Anthropic says Claude has produced what the company describes as the first complete computer-checked proof of Fermat’s Last Theorem, formalized in the Lean programming language. The claim comes from an Anthropic research post surfaced on Hacker News; no independent source in the provided cluster verifies the result. According to Anthropic, Claude worked largely autonomously for 11 days and generated an end-to-end formalization of the theorem. The company says the effort produced 13 million lines of Lean and proved 29,500 intermediate theorems on the way to a computer-checkable version of the result. Fermat’s Last Theorem states that there are no positive integers a, b, and c satisfying aⁿ + bⁿ = cⁿ for any n greater than 2. Anthropic’s post recounts the theorem’s long history, from Pierre de Fermat’s 17th-century margin note to Andrew Wiles’s 1995 proof, which the company says ran to 129 pages and required extensive human verification. The reported advance is not a new proof of Fermat’s Last Theorem in the mathematical sense. Anthropic explicitly frames the novelty as verification: translating an existing body of mathematical reasoning into a form that a proof assistant can check mechanically, much as a computation can be checked by a calculator. Anthropic says the project began when Tianyi Peng, an Anthropic researcher whose Columbia University group works on AI formalization tools, tested whether Claude could make progress on formalizing the theorem. The result, according to the company, went beyond that initial goal by producing a complete Lean-checked version. The post also places the work in the context of earlier formalization efforts. Anthropic cites a proposal by Dutch computer scientist Jan Bergstra to formalize Wiles’s proof and a multi-year community effort begun in 2024 by Kevin Buzzard at Imperial College London to complete a Lean formalization. The central caveat is sourcing. The provided material contains Anthropic’s own account, but not an independent review of the Lean development, the “first complete” claim, or the exact line and theorem counts. For now, the strongest version of the story is that Anthropic says Claude has completed a major formalization milestone, not that the broader mathematics and proof-assistant communities have independently validated every claim. Who benefits: Proof-assistant researchers, mathematicians working on formalization, and AI labs building reasoning systems stand to benefit if the reported workflow proves reproducible. Lean users may also gain from the intermediate formal material if Anthropic makes it usable to the community. Who's exposed: The claim raises the verification burden for Anthropic: the result depends on whether external experts can inspect and validate the formalization. Existing community formalization efforts may also face new pressure to compare methods and outputs against AI-generated work.