[devit]

This seems pointless, i.e. they might formalize the machine learning models (actually, the Lean code seems an AI-generated mix of Lean 3 and 4, probably doesn't compile), but the actual hard part is of course the proofs themselves, which they don't seem to solve.

Theorems of the kind "model X always does this desirable thing" are almost always false (because it's an imprecise model), and theorems of the kind "model X always does this desirable thing Y% of the time" seem incredibly hard to prove, probably impossible unless it's feasible to try the model on all possible inputs.

Even formulating the theorem itself is often extremely hard or impossible, e.g. consider things like "this LLM does not output false statements".

[mentalgear]

At least the author[0] seems to have some clout behind him. However, given that his code doesn't even compile and the premise seems massively over-stated, I wonder how his credentials (Stanford, etc) can even be genuine.

[0] https://mateopetel.xyz/

[Onavo]

How do they deal with models with a stochastic element (most of generative AI)? Not sure how you intend to prove sampling. Are they going to perform (mathematical) analysis on every single normal distribution in the model?

[Tainnor]

Indeed it doesn't compile.