Re:Formalizing Fermat's Last Theorem
by bobmarleybiceps on Friday September 04, 2026 @04:10PM
(#49569635)
guaranteed, up to lean itself having bugs that are exploited by the LLM :shrug:
[ Parent
| on HN ]
Do you have proof of this bug or something? Is this just envy against computers now ?
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.
Re:Formalizing Fermat's Last Theorem
by CaptWorld on Saturday September 05, 2026 @03:37AM
(#49574090)
Of course, there's a possibility but it exists everywhere but there's no sign till now that it has. Same with openai's proofs.
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".
Re:Formalizing Fermat's Last Theorem
by CaptWorld on Saturday September 05, 2026 @03:38AM
(#49574096)
Sure. But experts seem to be aware of the direction of those solutions so it seems unlikely there could be some hidden bug which disproves it. But it could be possible.
Well considering the proof is pretty much accepted by mathematicians to be correct (I'll be happy with that!), it would be sort of unnecessary to cheat. Maybe if some aspect is really tricky to formalize it could have done something there? If I had to search for it, I would go for parts of the original proof that are "outsourced" to other mathematical works.
Imagine one of the agents struggling to download a paper due to a paywall or whatever and just deciding to cheat lol