On September 4, 2026, Anthropic announced that its internal research model had produced a complete Lean-formalized proof of Fermat's Last Theorem (FLT) in 11 days: 13 million lines of code, 30,300 intermediate theorems (29,500 of which made it into the final proof), and roughly 6 billion output tokens. It is the first proof of Fermat's Last Theorem in history to be fully verified by a computer. Anthropic's official blog called it "the largest Lean proof file ever created," with a size more than five times that of the mathematical proof library Mathlib.
Before dissecting this properly, a frequently confused concept needs to be clarified: what happened here is not "AI discovering new mathematics," but "AI converting an existing human proof into a formal language that a machine can verify step by step." In 1995, British mathematician Andrew Wiles proved Fermat's Last Theorem in a 129-page paper—that was the mathematical discovery that genuinely cracked a mystery unresolved for 350 years. What Claude did was formalization: translating the complex chains of reasoning in Wiles's proof—spanning algebraic number theory, arithmetic geometry, Galois representation theory, and more—into code whose correctness can be automatically checked by the Lean proof assistant. To use a rough analogy: this is not writing a new novel, but translating an existing novel word by word into another language, while ensuring that the logic of every sentence still holds in the new language.
Technical Mechanics: It Wasn't a Single Agent Running for 11 Days
The platform Anthropic used was Prove2Me—an open-source collaborative formalization platform whose core uses a directed acyclic graph (DAG) to track dependencies between theorems. This structure allows dozens of Claude Agents to work in parallel: if a sub-proof depends on Theorem A and Theorem B, it can be assigned to different Agents advancing simultaneously without blocking one another. Anthropic disclosed that this task enlisted "dozens of" Claude Agents for concurrent collaboration, consuming approximately 6 billion output tokens in total.
The "11 days" refers to wall-clock time, not a single Agent working sequentially for 11 days. This distinction means two things: first, the difficulty of the task was substantially diluted through parallelization; and second, the coordination capacity of the overall system—task decomposition, dependency management, and assembly of sub-proofs—was the core variable behind this success, not merely the quality of any individual act of reasoning.
The model that carried out the task was described by Anthropic as an internal research version "roughly equivalent to Fable 5.1," with its specific parameter scale undisclosed. Human researcher Tianyi Peng (Columbia University) provided only a minimal amount of high-level guidance during the process—such as a note reading "Jacobian as a scheme sounds high priority"—while the remainder was left to the system's autonomous decision-making.
Kevin Buzzard's Dual Role
The reaction of Imperial College London mathematician Kevin Buzzard deserves close attention, because he is not merely an outside commentator. In 2024, Buzzard launched the mathematical community's collective formalization project, attempting to complete the Lean formalization of FLT step by step through human effort—a task widely expected to require several years.
After reviewing the proof submitted by Anthropic, Buzzard said publicly:
"This extraordinary automatic formalization achievement proves Fermat's Last Theorem without requiring any assumptions beyond mathematical axioms. It involved the automatic formalization of algebra, harmonic analysis, geometry, and number theory. The output of AI automatic formalization is robust enough to serve as the foundation for future work; this proof is multi-layered."But he also indirectly acknowledged the other side: among the files in Anthropic's GitHub repository, 106 upstream files came from the Imperial College FLT project led by Buzzard himself and from Mathlib. In other words, Claude did not start from zero—it stood on the shoulders of the mathematical community's years of accumulated work, then used AI methods to fill in the remaining gaps.
Where Are the Boundaries of "Autonomy"?
"Largely autonomously" in Anthropic's announcement is the phrase in this entire story that most requires careful reading. According to reports from SiliconAngle and other outlets, Claude's first formalization attempt failed—success was achieved only after incorporating Prove2Me, a third-party tool. This shows that the so-called "autonomy" is autonomy within the framework of a specific toolchain and pre-existing mathematical assets, not autonomy starting from a blank slate.
This does not diminish the value of the achievement itself, but it reminds us that when AI executes long-horizon tasks within a "well-documented body of human knowledge," its reliability differs dramatically from when it explores open domains. The correct assembly of the 29,500 intermediate theorems rested on the formal verification mechanism inherent in the Lean language—every inference step is checked in real time by the Lean kernel, making it impossible for errors to propagate. This was a "marathon with guardrails," not an unbounded free gallop across open terrain.
The Current Landscape of the AI Mathematics Race
Only by placing this event in the broader picture of AI mathematics in 2026 can its position be clearly seen. Earlier this year, OpenAI's internal model Astra announced a set of mathematical results, including solving the Erdős unit distance problem that had confounded the field for 80 years. Anthropic has also previously disclosed that another unreleased model made progress on the Riemann hypothesis, pushing the proportion of verified zeros further beyond the 41.6% mark. These three directions—the Erdős combinatorial problem, the Riemann hypothesis, and the formalization of FLT—belong to three distinct task types: "discovering new mathematics," "advancing known frontiers," and "verifying existing mathematics." Their technical difficulty and significance are entirely different.
FLT formalization belongs to the third category: it is the closest to engineering verification and the farthest from mathematical creation, yet it most directly demonstrates AI's execution capability on long-horizon, high-precision, verifiable tasks. Currently, a key question in the mathematical community is: how many of the 29,500 intermediate theorems will be incorporated into Mathlib as reusable modules for future research? If most are merely one-off products of this single exercise, then the pipeline connecting AI outputs with humanity's accumulated mathematics remains missing.
What Is the Real Milestone?
The deeper significance of this event lies not in AI having "proved" Fermat's Last Theorem—that was accomplished by Wiles in 1995—but in its demonstration of a new combination of AI capabilities: across 29,500 interdependent logical derivations, the coordination of multi-Agent parallel scheduling, DAG dependency tracking, and real-time Lean kernel verification held the cumulative error rate of a long-horizon task at zero.
This capability boundary deserves attention, and it also deserves caution. Formalization tasks have a critical property that tasks expressed in human natural language lack: every step has a right-or-wrong answer that a machine can judge. This is both the basis of its success and its limitation—most tasks in the real world have no verification mechanism like the Lean kernel standing by to catch mistakes. When the same multi-Agent architecture is applied to tasks without a real-time verification layer, whether error-free performance across 29,500 steps can be replicated is a question that no public data currently answers.
Anthropic's open stance this time is commendable: the proof code has been made public on GitHub under the Apache 2.0 license, and both the Lean kernel and the independent nanoda kernel have passed verification, allowing third parties to check it themselves. This is a rare case of "walking the talk"—not merely issuing a press release, but putting the raw output on display for anyone to scrutinize. The academic community's true examination will unfold over the coming months, as mathematicians conduct in-depth reviews of these 13 million lines of code. Until then, "AI has crossed the milestone threshold of formalized mathematics" is a judgment supported by evidence, while "AI autonomously completed one of the greatest proofs in human mathematics" is a claim that can only stand with a footnote attached.
© 2026 Winzheng.com 赢政天下 | 转载请注明来源并附原文链接