+- MKLab (https://mklab.gr)
+-- Forum: [INDEX] (https://mklab.gr/forumdisplay.php?fid=1)
+--- Forum: ARTFICIAL INTELLIGENCE (AI) (https://mklab.gr/forumdisplay.php?fid=5)
+---- Forum: ARTICLES (https://mklab.gr/forumdisplay.php?fid=33)
+---- Thread: Anthropic AI ‘formalizes’ proof of Fermat’s last theorem (/showthread.php?tid=2029)
Anthropic AI ‘formalizes’ proof of Fermat’s last theorem - mklabgr - 09-16-2026
The article reports a major AI-mathematics milestone: an advanced version of Anthropic’s Claude has formalized Andrew Wiles and Richard Taylor’s proof of Fermat’s Last Theorem in Lean, producing roughly 13 million lines of computer-checkable code in only 11 days. Fermat’s Last Theorem states that there are no positive integers satisfying $x^n+y^n=z^n$ for $n>2$.
The original proof was completed by Wiles in 1994 after centuries of attempts. Researchers quoted by Nature describe the AI achievement as extraordinarily difficult because formalization requires translating the mathematical argument—and thousands of supporting results—into a language that a computer can verify with complete logical precision.
The bigger significance is that AI could increasingly become a verification tool for mathematics, rather than merely a system that generates plausible-looking solutions. Claude’s result reportedly contains about 29,500 intermediate theorems, but there is an important limitation: its code is not yet easily reusable because it is separate from the carefully maintained Mathlib library. Integrating it would require substantial human work, and mathematicians worry about incompatible formal libraries developing in parallel.
Nevertheless, the achievement strengthens the possibility of automatically checking enormous mathematical papers, identifying errors that peer review misses, and eventually certifying large parts of mathematical knowledge. Nature notes that mathematicians now see AI-assisted formal verification as potentially transformative for the reliability and scalability of mathematical research.
ARTICLE