--- title: Claude formalized a Lean 4 proof of Fermat's Last... description: Anthropic released a complete Lean 4 formalization of Fermat's Last Theorem, produced by Claude and uploaded to GitHub. At over 13 million lines of code, it is... canonical: https://daily.dev/posts/claude-formalized-a-lean-4-proof-of-fermat-s-last-theorem-in-13-million-lines-of-code-wmzgr4slc twitter:card: summary_large_image twitter:site: @dailydotdev og:type: website og:site_name: daily.dev og:title: Claude formalized a Lean 4 proof of Fermat's Last Theorem in 13 million lines of code | daily.dev og:description: Anthropic released a complete Lean 4 formalization of Fermat's Last Theorem, produced by Claude and uploaded to GitHub. At over 13 million lines of code, it is... og:url: https://daily.dev/posts/claude-formalized-a-lean-4-proof-of-fermat-s-last-theorem-in-13-million-lines-of-code-wmzgr4slc og:image: https://api.daily.dev/og/posts/wMzGR4SLC.png og:image:alt: Claude formalized a Lean 4 proof of Fermat's Last Theorem in 13 million lines of code og:image:width: 1200 og:image:height: 630 og:locale: en --- > ## Documentation Index > Fetch the complete documentation index at: https://daily.dev/llms.txt > Use this file to discover all available pages before exploring further. # Claude formalized a Lean 4 proof of Fermat's Last Theorem in 13 million lines of code **[Collections](https://daily.dev/sources/collections)** · 2 min read · 4 upvotes · 0 comments ## Summary Anthropic released a complete Lean 4 formalization of Fermat's Last Theorem, produced by Claude and uploaded to GitHub. At over 13 million lines of code, it is the largest Lean proof ever written, and it also proves more than 29,000 supporting theorems across areas of mathematics never before formalized. Experts had expected such an effort to take years; the project was completed in a month. Anthropic frames this as a step toward reducing the mathematical refereeing burden as the volume of new proofs grows. The full proof and a writeup of the process are publicly available. ## Content Anthropic announced last month that Claude completed a formal, machine-verified proof of Fermat's Last Theorem — a project experts expected would take years. It took eleven days. The result is the largest Lean proof ever written: over 13 million lines of code, roughly 6 billion output tokens, and 29,500 intermediate theorems spanning areas of mathematics that had never been formalized before. The proof follows the 1995 Darmon-Diamond-Taylor exposition of the Wiles-Taylor-Wiles argument, not the more modern approach currently being pursued by Kevin Buzzard of Imperial College London under a five-year EPSRC grant. Buzzard, who is essentially being paid to do by hand what Claude just did in under two weeks, verified the proof himself using Lean's comparator tool. He confirmed no soundness exploits or shortcuts were used. He also noted, somewhat pointedly, that the mathematical content adds nothing new — the mathematical community already treats Wiles's 1995 proof as essentially certain. What's significant is the speed of formalization itself. ## How it was done The first attempt failed. The agents lost coherence as the proof grew larger and dependencies multiplied. Success came after adopting Prove2Me, an open coordination platform that tracks theorem dependencies and splits work into reusable files, combined with a multi-agent harness built on Claude Code. Dozens of Claude agents worked in parallel, converting the logical gaps in the existing Wiles-based proof into Lean code that a computer could check line by line. The codebase compiles nearly 20 times slower than Lean's mathlib on a 96-core machine, which gives some sense of its scale. It also completes Freek Wiedijk's 20-year-old list of 100 formalization challenges. ## What it actually means The proof can't enter Mathlib yet. Mathlib maintainers currently won't accept AI-authored contributions, and reviewing 13 million lines of machine-generated Lean is its own enormous problem. The bottleneck has shifted from writing proofs to reviewing them. But the broader implication is real: formalizing advanced mathematics has historically been so labor-intensive that it rarely happened at all. If AI can now do it at something close to the pace of publication, that changes the economics of mathematical verification entirely. Catching gaps in published proofs, easing the burden on referees, building a machine-checkable foundation for modern mathematics — these have been aspirations for decades. Eleven days is a different kind of answer than anyone expected. ## Questions this post answers ### How long did it take Claude to formalize a proof of Fermat's Last Theorem in Lean 4? It took eleven days, producing over 13 million lines of Lean code, roughly 6 billion output tokens, and 29,500 intermediate theorems, making it the largest Lean proof ever written. The proof follows the 1995 Darmon-Diamond-Taylor exposition of the Wiles-Taylor-Wiles argument and was independently verified by mathematician Kevin Buzzard using Lean's comparator tool. _Anyone tracking how fast AI can tackle formal verification work follows milestones like this on daily.dev._ ### What made the multi-agent Lean proof effort succeed after an initial attempt failed? The first attempt failed because agents lost coherence as the proof grew and dependencies multiplied. Success followed after adopting Prove2Me, an open coordination platform that tracks theorem dependencies and splits work into reusable files, combined with a multi-agent harness built on Claude Code, letting dozens of agents work in parallel converting proof gaps into checkable Lean code. _Developers experimenting with multi-agent coding harnesses can follow approaches like this one on daily.dev._ ### Why can't Claude's Lean proof of Fermat's Last Theorem be added to Mathlib? Mathlib maintainers currently do not accept AI-authored contributions, and reviewing 13 million lines of machine-generated Lean code is itself an enormous unsolved problem. The bottleneck in formal mathematics has shifted from writing proofs to reviewing them, even though the codebase compiles about 20 times slower than mathlib on a 96-core machine. _Teams weighing how to review large AI-generated codebases can track this debate on daily.dev._ ## Community take How the wider developer community reacted, aggregated from 2 discussions and 10 comments across lobsters, hackernews (as of 2026-09-13). **TL;DR:** Discussion centers less on the achievement itself and more on whether an AI-generated, hard-to-read mechanization undermines funding and motivation for producing an idiomatic, human-legible formalization. **Sentiment:** 20% positive · 60% mixed · 20% skeptical **The case for** - Some see value in the AI's work contributing to 'building the commons' if it feeds into Lean's mathlib over time. **The pushback** - Concern that an existing (even sloppy) AI-generated proof could undercut the case for funding future idiomatic formalization work. - Debate over whether the funding body actually required idiomatic proof/library contributions or just verified results, leaving the practical impact on the author's grant unclear. **By community** - lobsters (mixed): A back-and-forth about whether AI-generated proofs threaten funding for idiomatic formalization work, without clear resolution. - hackernews (mixed): Mostly meta-commentary pointing to a larger related thread rather than substantive discussion here. **Hottest debate:** Whether the AI-produced mechanization jeopardizes funding/motivation for the author's ongoing idiomatic Lean formalization work. **Open questions** - Was the EPSRC funding specifically tied to producing an idiomatic proof, or just a verified result? - Has anyone tried forcing more idiomatic translations from AI models, and is the current messiness a limitation of model capability or of the approach taken? **Highlights** > > An existing mechanization, even if barely-comprehensible slopped-out code, destroys the possibility for funding future work Has anyone before funded specifically idiomatic proof, or just a proof verification and the mathematicians cared about the format? (Feels similar to companies paying developers for results and developers potentially caring about the readable code) Has anyone done attempts at forcing an idiomatic translation? Basically, is the issue with the current model capabilities, or with approach taken? > — [viraptor on lobsters · 1 points, 1 comments](https://lobste.rs/s/5iacaa/flt_anthropic_has_beaten_me_it#c_xjzq3e) > Yes, per the OP: > I am currently being funded by the EPSRC to formalize a proof of Fermat’s Last Theorem, and a naive reaction to the news above is that I no longer have any work to do. This is not the case. The work certainly achieves some of the aims of the EPSRC project [...]. But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. > — [tuxes on lobsters · 1 points, 1 comments](https://lobste.rs/s/5iacaa/flt_anthropic_has_beaten_me_it#c_u57ojz) > The process for science funding, in many cases including EPSRC programs, is basically the applicants saying «if you fund this project to this amount, that's what we'll do» and some of the applications being approved. So without further clarifications, «I promised XYZ and ZXC when getting the funding» and «my group was funded to do XYZ and ZXC» are not fully distinguishable in this context. The relative importance of parts of the application is often an interesting question, and typically a hard-to-answer one. (And it depends on the prevailing attitudes in the community, too, as there is «review by experts» part to all this) > — [k749gtnc9l3w on lobsters · 1 points](https://lobste.rs/s/5iacaa/flt_anthropic_has_beaten_me_it#c_b9utlh) > That only says what the author promised, not what was requested from the author / funded. > — [viraptor on lobsters · 1 points, 1 comments](https://lobste.rs/s/5iacaa/flt_anthropic_has_beaten_me_it#c_3fjun3) **Source threads** - [lobsters](https://lobste.rs/s/5iacaa/flt_anthropic_has_beaten_me_it) · 34 points · 6 comments - [hackernews](https://news.ycombinator.com/item?id=49570133) · 34 points · 4 comments ## Similar posts on daily.dev - [Fermat Left a Note in a Margin. Other People Spent 358 Years Finishing It.](https://daily.dev/posts/fermat-left-a-note-in-a-margin-other-people-spent-358-years-finishing-it--y4pafjmyt) · SQL Authority · 2 upvotes · 0 comments - [Human mathematicians are being outcounterexampled](https://daily.dev/posts/human-mathematicians-are-being-outcounterexampled-ocacgpf22) · Hacker News · 3 upvotes · 0 comments - [How I Vibed a Proof of Conway’s Conjecture — overreacted](https://daily.dev/posts/how-i-vibed-a-proof-of-conway-s-conjecture-overreacted-onrulhfhq) · Overreacted · 5 upvotes · 0 comments - [Creator of Lean: Handwritten Math Will Change Dramatically](https://daily.dev/posts/creator-of-lean-handwritten-math-will-change-dramatically-ssexcp90l) · The Developing Dev · 0 upvotes · 0 comments --- Tags: [#claude](https://daily.dev/tags/claude), [#anthropic](https://daily.dev/tags/anthropic), [#math](https://daily.dev/tags/math) [View this post on daily.dev](https://daily.dev/posts/claude-formalized-a-lean-4-proof-of-fermat-s-last-theorem-in-13-million-lines-of-code-wmzgr4slc) ```json {"@context":"https://schema.org","@graph":[{"@type":"Organization","@id":"https://daily.dev/#organization","name":"daily.dev","url":"https://daily.dev","logo":{"@type":"ImageObject","url":"https://daily.dev/apple-touch-icon.png","width":180,"height":180},"sameAs":["https://twitter.com/dailydotdev","https://github.com/dailydotdev","https://www.linkedin.com/company/daily-dev-ltd"]},{"@type":"WebSite","@id":"https://daily.dev/#website","url":"https://daily.dev","name":"daily.dev","publisher":{"@id":"https://daily.dev/#organization"},"potentialAction":{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https://daily.dev/search?q={search_term_string}"},"query-input":"required name=search_term_string"}}]} {"@context":"https://schema.org","@type":"TechArticle","headline":"Claude formalized a Lean 4 proof of Fermat's Last Theorem in 13 million lines of code","url":"https://daily.dev/posts/claude-formalized-a-lean-4-proof-of-fermat-s-last-theorem-in-13-million-lines-of-code-wmzgr4slc","mainEntityOfPage":{"@type":"WebPage","@id":"https://daily.dev/posts/claude-formalized-a-lean-4-proof-of-fermat-s-last-theorem-in-13-million-lines-of-code-wmzgr4slc"},"datePublished":"2026-09-04T18:51:11.264Z","dateModified":"2026-09-13T19:34:16.822Z","description":"Anthropic released a complete Lean 4 formalization of Fermat's Last Theorem, produced by Claude and uploaded to GitHub. At over 13 million lines of code, it is...","isAccessibleForFree":true,"articleSection":"Collections","inLanguage":"en","publisher":{"@type":"Organization","name":"daily.dev","url":"https://daily.dev","logo":{"@type":"ImageObject","url":"https://daily.dev/apple-touch-icon.png","width":180,"height":180}},"author":{"@type":"Organization","name":"Collections","logo":"https://media.daily.dev/image/upload/s--fk_6ycEi--/f_auto,q_auto/v1780996001/logos/collections?_a=BAMAMiWQ0","url":"https://daily.dev/sources/collections"},"commentCount":0,"discussionUrl":"https://daily.dev/posts/claude-formalized-a-lean-4-proof-of-fermat-s-last-theorem-in-13-million-lines-of-code-wmzgr4slc","interactionStatistic":[{"@type":"InteractionCounter","interactionType":{"@type":"LikeAction"},"userInteractionCount":4},{"@type":"InteractionCounter","interactionType":{"@type":"CommentAction"},"userInteractionCount":0}],"keywords":"claude,anthropic,math","timeRequired":"PT2M"} {"@context":"https://schema.org","@type":"BreadcrumbList","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https://daily.dev"},{"@type":"ListItem","position":2,"name":"Collections","item":"https://daily.dev/sources/collections"},{"@type":"ListItem","position":3,"name":"Claude formalized a Lean 4 proof of Fermat's Last Theorem in 13 million lines of code"}]} {"@context":"https://schema.org","@type":"FAQPage","@id":"https://daily.dev/posts/claude-formalized-a-lean-4-proof-of-fermat-s-last-theorem-in-13-million-lines-of-code-wmzgr4slc#faq","mainEntity":[{"@type":"Question","name":"How long did it take Claude to formalize a proof of Fermat's Last Theorem in Lean 4?","acceptedAnswer":{"@type":"Answer","text":"It took eleven days, producing over 13 million lines of Lean code, roughly 6 billion output tokens, and 29,500 intermediate theorems, making it the largest Lean proof ever written. The proof follows the 1995 Darmon-Diamond-Taylor exposition of the Wiles-Taylor-Wiles argument and was independently verified by mathematician Kevin Buzzard using Lean's comparator tool. Anyone tracking how fast AI can tackle formal verification work follows milestones like this on daily.dev."}},{"@type":"Question","name":"What made the multi-agent Lean proof effort succeed after an initial attempt failed?","acceptedAnswer":{"@type":"Answer","text":"The first attempt failed because agents lost coherence as the proof grew and dependencies multiplied. Success followed after adopting Prove2Me, an open coordination platform that tracks theorem dependencies and splits work into reusable files, combined with a multi-agent harness built on Claude Code, letting dozens of agents work in parallel converting proof gaps into checkable Lean code. Developers experimenting with multi-agent coding harnesses can follow approaches like this one on daily.dev."}},{"@type":"Question","name":"Why can't Claude's Lean proof of Fermat's Last Theorem be added to Mathlib?","acceptedAnswer":{"@type":"Answer","text":"Mathlib maintainers currently do not accept AI-authored contributions, and reviewing 13 million lines of machine-generated Lean code is itself an enormous unsolved problem. The bottleneck in formal mathematics has shifted from writing proofs to reviewing them, even though the codebase compiles about 20 times slower than mathlib on a 96-core machine. Teams weighing how to review large AI-generated codebases can track this debate on daily.dev."}}]} ```