| ▲ | imjonse 2 hours ago |
| the proofs were verified in Lean, so unlikely. |
|
| ▲ | thesz 2 hours ago | parent | next [-] |
| But still possible [1]. [1] https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke... |
|
| ▲ | nicce 2 hours ago | parent | prev [-] |
| 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... |
| |
| ▲ | latent-person an hour ago | parent [-] | | 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). | | |
| ▲ | nicce an hour ago | parent [-] | | That is the point. Someone must verify that the Lean matches the actual theorem, precisely as it should be interpreted. | | |
|
|
