On: How An AI math breakthrough ignited a controversy

[jeanmichelselli]

AI models and in particular LLMs are not capable of logic reasoning. See for example this paper:

https://arxiv.org/abs/2506.06941

Ergo, they can't prove any theorem whatsoever. How do people at OpenAI expect that we believe in claims like that? This is yet another before-the-IPO stunt in my opinion..

Personally, I won't believe any of these claims until the community of mathematicians says otherwise.

[ctenb → jeanmichelselli]

They didn't write a traditional proof, but a lean program, which can be used to validate proofs formally, using a computer. It's still up to humans to check wether the formalization is sensible, but the proof is correct.

[prmph → ctenb]

Has Lean itself been proved?

[dekhn → prmph]

I think pretty much every major mathematician has accepted that the ideas and implementation behind lean is solid.