--- 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 · 0 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's Claude has completed the first fully formalized proof of Fermat's Last Theorem - a project experts expected would take years, finished in 11 days. The result: over 13 million lines of Lean 4 code and 29,500 intermediate theorems proved along the way. It's the largest Lean proof ever written. ## What actually happened Fermat's Last Theorem was first proved by Andrew Wiles in 1995, more than 350 years after Fermat scribbled his conjecture in a margin. Wiles's proof is notoriously complex, spanning hundreds of pages and drawing on deep results from algebraic geometry and number theory. Formalizing a proof means converting that mathematical reasoning into a form that a computer proof assistant - in this case, Lean - can check line by line. It's painstaking work. For a proof as sprawling as Wiles's, the conventional estimate was that formalization would take a team of mathematicians many years. Instead, dozens of Claude agents worked through the existing Wiles-based proof, filling in the logical gaps and translating everything into Lean code. Lean then verified the finished proof. Eleven days, start to finish. ## Why the 29,500 intermediate theorems matter The headline number is 13 million lines, but the more interesting figure might be the 29,500 supporting theorems. Wiles's proof touches many areas of mathematics - elliptic curves, modular forms, Galois representations - that had never been formally verified before. Claude had to prove all of those pieces too, not just the final result. That's a meaningful chunk of mathematical infrastructure that now has machine-checkable proofs behind it. ## The broader point Mathematics has a refereeing problem. More proofs are being published than the community can carefully check, and even proofs that pass peer review sometimes contain errors that go undetected for years. Formalization is one solution, but it's been too slow and labor-intensive to scale. If AI can handle the bulk of that conversion work - turning human mathematical reasoning into something a computer can verify - that changes the calculus considerably. This project suggests the timeline for AI-assisted formalization is much shorter than most people assumed. The complete proof is on GitHub, and Anthropic has a writeup of the process on their science blog. ## Questions this post answers ### Has an AI model formalized Fermat's Last Theorem in Lean 4? Yes, Claude produced a complete Lean 4 formalization of Fermat's Last Theorem that Anthropic uploaded to GitHub. The proof spans over 13 million lines of code, making it the largest Lean proof ever written, and it required proving more than 29,000 supporting theorems across areas of mathematics that had never been formalized before. Experts had expected the project to take years. _daily.dev tracks milestones like this for developers following AI progress in formal reasoning and code generation._ ## Community take How the wider developer community reacted, aggregated from 4 discussions and 468 comments across x (as of 2026-09-04). **TL;DR:** Reaction is split between genuine excitement that a Wiles-scale proof was formalized in Lean and reusable side-theorems were produced, and skepticism that this is mostly brute-force compute re-verifying an already-accepted result rather than a novel mathematical breakthrough. **Sentiment:** 30% positive · 35% mixed · 35% skeptical **The case for** - Formalizing the proof in Lean gives increased trust/confidence beyond human peer review, since Wiles's original proof did contain an error that was later fixed. - The ~29,500 intermediate theorems and formalized machinery (elliptic curves, modular forms, Galois representations) are seen as reusable infrastructure for future formalization work. - Some view it as evidence of rapid capability growth in AI reasoning over the past couple of years. - Checking prior proofs is seen as validating model capability and correctness for future formalization efforts. **The pushback** - Many argue this just translates an already-accepted 1995 proof into machine-checkable code rather than solving anything new, so the headline framing is misleading. - Concern that the result is bloated/inelegant "brute-forced" with massive compute rather than a clean, minimal formalization, and that a human-crafted version could cut the intermediate theorems substantially. - Skepticism that formal verification itself is trustworthy or meaningful, questioning who verifies the verifier. - Some feel it's a lot of compute spent to double-check a centuries-old, already-verified claim, with limited new information produced. - Frustration that frontier labs do this kind of one-off, non-followed-through work ("shoot and scoot") rather than integrating with ongoing academic formalization efforts like Kevin Buzzard's project. **By community** - x (heated): Replies swing between calling this a genuinely useful trust-building milestone with reusable formalized math and dismissing it as an expensive, inelegant re-verification stunt, with several sharp back-and-forth arguments over what formal verification actually proves. **Hottest debate:** Whether formalizing an already-accepted proof provides genuinely new mathematical value and trust, or is just a costly, oversized restatement of existing work. **Open questions** - Could a more elegant, much shorter Lean proof be constructed instead of the current 13-million-line version? - How does this affect the ongoing human-led effort (led by Kevin Buzzard) to formalize the same proof? - Will the reusable intermediate theorems and formalized machinery meaningfully accelerate future formalization work? **Highlights** > @ivanich22893 @scaling01 The humans can make mistakes. Wiles *did* make a mistake when he first published it, and only a handful of people have seriously looked at the proof. The new information is increased trust that the proof is correct. > — [boris\_brave on x](https://x.com/boris_brave/status/2095963899149345004) > @AnthropicAI AI solves maths by giving you a solution so complicated that to proof that the solution is wrong will be harder than solving the actual problem so you just give up and accept that it’s solved. Mathematical gaslighting > — [repojournal on x · 13 points, 3 comments](https://x.com/repojournal/status/2095957302570287316) > @AnthropicAI ngl this headline is doing a lot of lifting. wiles proved FLT in 95, this is just translating an ALREADY accepted proof into lean so a computer can double check it. useful yeah, but its not “ai solves 350 yr old problem” its “ai (with a huge human team) transcribes existing proof > — [AndAIyou on x · 14 points, 5 comments](https://x.com/AndAIyou/status/2095959719261172187) > @lajoiedeslutins @AnthropicAI technically it is way more than 13 million lines of code you need mathlib, a Lean compiler, a C compiler, a linker, etc. > — [Victor414733137 on x · 4 points](https://x.com/Victor414733137/status/2095970831570526408) > @MaleManlpulator @bleakflowerz @shiri_shh @AnthropicAI I wonder how they feel about this. Excited because it’s done, or having an existential crisis about their years long work being succeeded by a few trillion matrix multiplications on NVIDIA cards? > — [twq\_df on x · 1 points, 1 comments](https://x.com/twq_df/status/2095995629931487442) **Source threads** - [x](https://x.com/scaling01/status/2095953401460768990) · 0 points · 12 comments - [x](https://x.com/scaling01/status/2095941610651455822) · 0 points · 82 comments - [x](https://x.com/AnthropicAI/status/2095947707605266436) · 0 points · 371 comments - [x](https://x.com/rohanpaul_ai/status/2095965328669053054) · 0 points · 3 comments ## Similar posts on daily.dev - [Claude Can \(Sometimes\) Prove It](https://daily.dev/posts/claude-can-sometimes-prove-it-wshuhsu5p) · Hacker News · 2 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-04T23:02:19.605Z","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":0},{"@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":"Has an AI model formalized Fermat's Last Theorem in Lean 4?","acceptedAnswer":{"@type":"Answer","text":"Yes, Claude produced a complete Lean 4 formalization of Fermat's Last Theorem that Anthropic uploaded to GitHub. The proof spans over 13 million lines of code, making it the largest Lean proof ever written, and it required proving more than 29,000 supporting theorems across areas of mathematics that had never been formalized before. Experts had expected the project to take years. daily.dev tracks milestones like this for developers following AI progress in formal reasoning and code generation."}}]} ```