Mathematicians and computer scientists have reported unexpectedly swift progress in formalising Fermat's Last Theorem, leveraging cutting-edge Artificial Intelligence (AI) models during a recent workshop in London. The initiative, spearheaded by Kevin Buzzard of Imperial College London, aims to translate Andrew Wiles's 1993 proof of the centuries-old theorem into computer code, known as Lean, for rigorous formal verification and as a basis for future mathematical exploration.
Fermat's Last Theorem, famously simple to state but notoriously difficult to prove, asserts that no three positive integers a, b, and c can satisfy the equation aⁿ + bⁿ = cⁿ for any integer value of n greater than 2. Wiles's original proof spanned approximately 100 pages, building upon thousands of pages of prior mathematical research.
The London workshop brought together 25 researchers from various fields and countries to collaborate on Buzzard's five-year project. Before the event, the project contained around 20,000 lines of code. Remarkably, this figure doubled after just the first day, demonstrating the profound impact of AI in accelerating the formalisation process. Researchers huddled around laptops, using leading AI models to tackle problems and sub-problems, with human insight guiding the AI's computations.
Buzzard's "Formalising Fermat" project commenced in 2024, initially progressing slowly with manual coding. However, the pace dramatically increased around December 2025 as AI models became significantly more adept at handling advanced mathematical concepts. This shift, coupled with an AI's unexpected solution to an 80-year-old problem posed by Paul Erdős in May, has prompted Buzzard to reassess the project's ambitions.
Originally, Buzzard intended to formalise only the final paper of Wiles's proof, or its more recent improvements, assuming the foundational mathematics were correct. However, given the rapid advancements in AI, he now believes it is feasible to formalise the entire body of work, from its most fundamental principles upwards, for complete verification. This expanded scope hinges on the continued progression of AI capabilities, the cost of access to these models, and the ongoing success of collaborative workshops.