Comment by mswphd
8 hours ago
as mentioned elsewhere, there was a bug in the lean kernel exploited by AI to prove a false statement roughly a month ago
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
8 hours ago
as mentioned elsewhere, there was a bug in the lean kernel exploited by AI to prove a false statement roughly a month ago
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
Got it. Thanks. I feel people are using this single story to downplay this feat. There's definitely a chance but I don't see any indication of similar bugs in here or the openai's proofs that were created a month ago as i think these companies might've vetted it enough and the other team who's working on similar lean proof for this also seems to have acknowledged this feat
I also doubt this is leveraging a lean4 kernel bug, but I also do not think that a 13m LoC proof that has not been human reviewed closes the book on our understanding of Fermat's Last Theorem, in part because of the decided possibility of a kernel bug being used somewhere in those 13m lines.
How about all of these bugs from last week?
https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...
...I'm not saying this FLT result is compromised. I suppose things depend on your perspective where we are on the spectrum of "finding more bugs means there are fewer left to discover" vs. "finding more bugs probably means there are still unexplored corners out there".
[dead]