![\"\"](\"https:\/\/www.europesays.com\/uk\/wp-content\/uploads\/2026\/07\/SEI_304535668.jpg\")
<\/p>\n<\/p>\n
Pierre de Fermat was a 17th-century mathematician<\/p>\n
Lebrecht Music& Arts, YAY Media AS\/Alamy<\/p>\n<\/p>\n
In the lobby of a central London hotel, tourists are bracing themselves for a day of sightseeing in a heatwave. Meanwhile, staff are resetting the dining room after breakfast. And in a windowless meeting room, assembled academics are contemplating whether humans have a role to play in the future of mathematics, now that AI can prove theorems by itself.<\/p>\n
The general mood in the room is one of bewilderment at the recent jump in computer intelligence and excitement about the potential it unlocks \u2013 and perhaps a slight unease about what the future holds for them personally.<\/p>\n
Twenty-five researchers from diverse fields and countries are here to spend a week working on formalising Fermat\u2019s last theorem with cutting-edge AI models.<\/p>\n
Fermat\u2019s last theorem puzzled mathematicians for centuries until it was proven in 1993 by Andrew Wiles<\/a>. It states that there are no whole numbers a, b, and c that satisfy the equation a\u207f + b\u207f = c\u207f, where n is a whole number greater than 2. It is extremely easy to state, but fiendishly difficult to prove.<\/p>\n Now, Kevin Buzzard<\/a> at Imperial College London is working on a five-year project<\/a> to turn Wiles\u2019s 100 pages of mathematics into computer code called Lean, so that it can be formally checked for correctness and used as a foundation for further research.<\/p>\n Formalising mathematical theorems takes them out of the realm of pen and paper, and puts them into a configuration that allows computers to grapple with them, methodically working through the logic and exposing any flaws. Already, there are 2 million lines of formalised mathematics stored in a central repository called Mathlib<\/a>.<\/p>\n This workshop has brought together mathematicians, computer scientists and AI experts in the hope that they can advance Buzzard\u2019s project to add Fermat\u2019s last theorem to this corpus by getting the very latest AI models to do some of the heavy lifting.<\/p>\n Groups are huddled around laptops, each displaying slightly different interfaces for one of the AI industry\u2019s leading models. The atmosphere is buzzing. A second room was booked so that people could work in silence if they preferred, but it is empty.<\/p>\n Problems and sub-problems are split up, distributed and chipped away at by human brains prompting and steering AI. There were a total of 20,000 lines of code in the project before the workshop, says Buzzard. After just the first day, that had doubled.<\/p>\n The Formalising Fermat project<\/a> was funded in 2024 and began slowly as Buzzard laboriously coded by hand. The pace picked up dramatically around December last year, he says, when the power of AI models to work with advanced mathematics seemed to grow rapidly. Then, in May, an 80-year old problem posed by Paul Erd\u0151s<\/a> was solved by machine<\/a>, taking the field totally by surprise. The whole affair has forced Buzzard to rethink things.<\/p>\n \u201cI was always quietly confident that we were going to succeed.\u2029But now we\u2019re two years in and AI has got so good that now my instinct is, this is ridiculous \u2013 what I said I\u2019d do is ridiculous. Let\u2019s just do something 10 times better,\u201d he says.<\/p>\n Wiles\u2019s proof may have stretched to around 100 pages, but it relied on another 2000 or so pages of mathematics from the 1960s, 70s and 80s. Buzzard\u2019s original project was to formalise only the final paper \u2013 or more recent improvements of it, at least \u2013 but assume that everything it rested on was correct.<\/p>\n If the whole set of theorems were a pyramid, Buzzard had intended to start climbing from only 90 per cent of the way up, where the really interesting problems lived. But now he thinks it is possible to tackle the whole thing from top to bottom for the sake of completeness.<\/p>\n He is extremely confident that, by the end of his five-year project, he will have done what he originally set out to do. How AI progresses in the coming years, how expensive it is to access and how this workshop goes will determine how far he gets on the rest of the pyramid.<\/p>\n