In 1637, French mathematician Pierre de Fermat left a note in the margin of a book. He claimed to have discovered a remarkable proof but wrote that "the margin is too narrow to contain it." It took humanity 358 years to fill that gap. The 'Fermat's Last Theorem' was finally solved when British mathematician Andrew Wiles published his 129-page proof in December 1995.
Thirty-one years later, AI stands before the same problem once more. This time, it rewrote Wiles' 129-page human-authored proof line by line so that computers could verify its logical completeness—a 'verification.' Anthropic announced on the 4th (local time) that its AI Claude completed this task in just 11 days. Dozens of AI agents wrote 13 million lines of code for the proof-checking program 'Lean' and proved 33,000 intermediate lemmas; ultimately, 29,500 of those were incorporated into the final proof.
Mathematical papers often omit steps. Mathematicians understand that writing just a few lines stating "the next result follows from the previous theorem" is sufficient. Computers do not work this way: if even one step is skipped, they ask "why?" Lean starts from basic mathematical rules and checks whether logic flows continuously from the first step to the conclusion. 'Formalization'—translating human papers into Lean's language—requires writing out every detail, even those humans consider "obvious," making it extremely labor-intensive. This explains why Professor Kevin Buzzard's team at Imperial College London, which began the project in 2024, initially estimated it would take several years.
Anthropic deployed multiple AIs like a research team. Large proofs were broken into smaller problems and distributed among them; one AI proved a lemma that another AI then used to tackle more difficult questions. The final judgment was made not by an AI but by Lean itself: the AI rewrote the solution in meticulous detail, and a rule-following computer graded it. Professor Buzzard described this as a "major advance" toward automatic formalization of modern mathematical literature.
Verification in mathematics is harder than it appears. Wiles himself first presented his proof in 1993 but had to revise it for another year after a critical gap was discovered during verification, finally releasing the definitive version in 1995. Thomas Hales' proof of the 'Kepler Conjecture' was deemed impossible to fully verify even by a panel of 12 referees over four years; Hales then assembled a team of 20 to create a computer-verifiable proof instead. As multiple AIs tirelessly generate proofs around the clock, their production speed begins to outpace human reading and verification capabilities. What becomes essential is a mechanism to determine "whether we can trust answers produced by AI."
Roles are increasingly divided: humans select which problems matter and set directions; AI rapidly handles intermediate calculations and proofs; programs like Lean re-verify results from scratch to ensure correctness. There are limits, however. Claude did not solve the theorem using a new method but built upon centuries of accumulated theory and existing proofs. The research team also emphasized that computer-generated proofs should never replace papers written for human understanding.
The number 11 carries significance. While it took humans 358 years to find the answer, converting it into a form verifiable by computers was expected to take several years—yet this expectation was shattered. The shift marks a transformation in science: from an era where humans both discovered and verified, to one where AI organizes human discoveries and computers complete the final verification.
in TECH
