Comment by nicce
5 hours ago
Can’t wait to see the human verifying the results and then figure out that the AI model actually cheated and the results are not correct.
5 hours ago
Can’t wait to see the human verifying the results and then figure out that the AI model actually cheated and the results are not correct.
the proofs were verified in Lean, so unlikely.
As long as the proofs itself are correct. How long they were this time?
Edit: at least ~600,000 lines
https://stanfordtechreview.com/articles/openai-buckmaster-na...
To claim something verified in Lean is wrong, you need to either argue that the theorem was stated incorrectly, or that there is a bug in Lean (assuming no `sorry` etc, which is checked by comparator). The number of lines needed to prove it is irrelevant (other than checking for a bug in Lean gets harder).
3 replies →
But still possible [1].
[1] https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...