AI compressed a years-long proof formalization into 11 days
Anthropic says dozens of Claude agents completed the first end-to-end computer-checked formalization of Fermat's Last Theorem in 11 days. The system wrote 13 million lines of Lean, proved 30,300 intermediate theorems, and used 29,500 of them in the final result. This is not a new proof of the theorem. It formalizes a simplified route through the established proof, translating every logical step into a language that a proof assistant can check. That distinction makes the result more important, not less. AI can already generate more mathematical arguments than human reviewers can examine manually. Formalization turns the model's output into an artifact that can be replayed against explicit axioms and a public theorem statement. The orchestration mattered. Anthropic reports that early attempts failed when agents lost track of project state and stopped collaborating. The successful run used a directed graph of theorem statements, separate files for statements and proofs, search and reuse, dozens of agents, and roughly six billion output tokens. The public repository includes the proof, proof path, verification checks, and reproduction instructions. Full checking requires substantial computing resources, and the claim comes from the company that ran the project, so independent replication and mathematical review still matter. Even with those limits, the project demonstrates a productive model for AI-assisted research: do not ask people to trust a fluent answer. Make the system produce a result that another system and the public can inspect.
