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).
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).
That is the point. Someone must verify that the Lean matches the actual theorem, precisely as it should be interpreted.
2 replies →
But still possible [1].
[1] https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...