FLT: Anthropic has beaten me to it | Xena
I guess technically it was revealed to the world by a coffee shop in Islington on Insta, but an hour later it was officially announced by Anthropic: one of their internal models, using the prove2.m…
I guess technically it was revealed to the world by a coffee shop in Islington on Insta, but an hour later it was officially announced by Anthropic: one of their internal models, using the prove2.me platform, has formalized a complete proof of Fermat’s Last Theorem (FLT) in Lean. This is the final theorem to be formalized in Freek Wiedijk’s famous list of 100 formalization challenges and thus wraps up this 20-year-old benchmark. Congratulations to Anthropic! Mathematical details The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but…
saved by
related reading
- Formalizing Fermat's Last Theoremanthropic.com
- Xena | Mathematicians learning Lean by doing.xenaproject.wordpress.com
- Announcing FrontierMath Erdősepoch.ai
- lf-lean: The frontier of verified software engineering | Theoremtheorem.dev
- A recent experience with ChatGPT 5.5 Pro | Gowers's Webloggowers.wordpress.com
- 2510.01346arxiv.org
- What's new | Updates on my research and expository papers, discussion of open problems, and other maths-related topics. By Terence Taoterrytao.wordpress.com
- Human mathematicians are being outcounterexampledxenaproject.wordpress.com
- my favorite proof of fermat's little theoremblog.kayleesk.com
- Mathematics in the Library of Babel - Daniel Littdaniellitt.com
- The fall of the theorem economydavidbessis.substack.com
- Lean Game Serveradam.math.hhu.de