2 ms·

AI models and in particular LLMs are not capable of logic reasoning. See for example this paper: https://arxiv.org/abs/2506.06941 https://arxiv.org/abs/2506.06

AI models and in particular LLMs are not capable of logic reasoning. See for example this paper: https://arxiv.org/abs/2506.06941 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 17d ago
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 17d ago
  Has Lean itself been proved?
  - dekhn 17d ago
    I think pretty much every major mathematician has accepted that the ideas and implementation behind lean is solid.