Researchers gathered in London this week to accelerate the formalization of Fermat's Last Theorem using advanced AI models. The workshop focuses on converting Andrew Wiles's 1993 proof into Lean code for computer verification. Progress has been rapid, with code lines doubling after the first day.
Twenty-five mathematicians, computer scientists and AI experts met in a central London hotel to work on the project led by Kevin Buzzard of Imperial College London. The five-year effort, funded in 2024, aims to add the theorem to the Mathlib repository of formalized mathematics.
Before the workshop there were 20,000 lines of code in the project. After the first day the total had reached 40,000. Buzzard noted that AI capabilities improved sharply from December last year, allowing the team to tackle more of the underlying mathematics than originally planned.
Hang Lu Su, also at Imperial College London, described the process as an industrialization of intellectual work. Participants are using models including Claude to generate and refine code, though concerns remain about verbosity and long-term maintainability of AI-produced output.
Buzzard expressed confidence that the original goals will be met by the end of the project. How far the team advances on the full pyramid of supporting theorems will depend on further AI developments.