AI doubles Fermat proof code in one day
Get the Health newsletter
Daily health & science — research, biotech, public health, the studies worth knowing. Free.
- Kevin Buzzard at Imperial College London is leading a five-year project to convert Andrew Wiles's roughly 100-page 1993 proof of Fermat's last theorem into Lean code, and a week-long London workshop of 25 researchers from maths, computer science and AI used leading models to push the codebase from 20,000 lines to 40,000 lines after just the first day.
- Buzzard said the project's pace shifted dramatically around December 2024 when AI models' ability to handle advanced mathematics jumped, and in May a machine solved an 80-year-old problem posed by Paul Erdős, prompting him to abandon his original plan of formalising only the final paper and instead attempt the whole ~2,000-page pyramid of supporting mathematics.
- Hang Lu Su at Imperial College London, who taught herself Lean via ChatGPT six months ago, said the workshop felt like an 'industrialisation of the intellectual process,' adding that token costs are running into thousands of pounds per day across a mix of free open-source tools and expensive US start-up models.
- Buzzard acknowledged the AI-generated Lean code is 'verbose, clunky' and sometimes uses obscure Lean features that break on updates, describing the workshop's output as 'a layer of slop' that Mathlib's human curators are wary of merging into the 2-million-line library.
- Buzzard raised philosophical questions about the field's future, asking: 'If a machine proves a theorem but no human can understand it, then what have we achieved?' and 'There's this abstract world, but does that abstract world exist if humans aren't there to appreciate it?'
Why it matters: Buzzard's project is a real-time test of whether frontier AI can absorb one of mathematics' most famous proofs, and the one-day doubling of the codebase suggests formalisation timelines that once took years may now collapse into months — but only if the resulting code is clean enough for the human-curated Mathlib library to accept, which Buzzard openly doubts.
