About the formalization of Fermat's Last Theorem in Lean and AI's role in proofs.
Has this happened?
Yes 21 (19%)Not sure 46 (41%)No 44 (40%)
Votes cast 1–2 October 2026: 100,590 votes from 9,694 people.
Hacker News has set AI a lot of challenges over the years. Which ones has it met?
About the formalization of Fermat's Last Theorem in Lean and AI's role in proofs.
Votes cast 1–2 October 2026: 100,590 votes from 9,694 people.
Much of the value of proof is in the development of math definitions and intermediate theorems needed to get you there, Grothendiek-style. This ability seems still to be beyond AI (at least, I haven’t heard of any fundamentally new and useful definitions such as “scheme” or “modular form” emerging from the latest blizzard of AI proofs). BUT, I wonder if AI could develop this skill too through a process of efficiently refactoring a big Lean proof into Lean pieces, then interpreting the pieces back into new, human-grokable definitions with evocative names?