Mathematicians put AI to work on Fermat’s last theorem

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.

The general mood in the room is one of bewilderment at the recent jump in computer intelligence and excitement about the potential it unlocks – and perhaps a slight unease about what the future holds for them personally.

Twenty-five researchers from diverse fields and countries are here to spend a week working on formalising Fermat’s last theorem with cutting-edge AI models.

Fermat’s last theorem puzzled mathematicians for centuries until it was proven in 1993 by Andrew Wiles. It states that there are no whole numbers a, b, and c that satisfy the equation aⁿ + bⁿ = cⁿ, where n is a whole number greater than 2. It is extremely easy to state, but fiendishly difficult to prove.

Now, Kevin Buzzard at Imperial College London is working on a five-year project to turn Wiles’s 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.

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.

This workshop has brought together mathematicians, computer scientists and AI experts in the hope that they can advance Buzzard’s project to add Fermat’s last theorem to this corpus by getting the very latest AI models to do some of the heavy lifting.

Groups are huddled around laptops, each displaying slightly different interfaces for one of the AI industry’s 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.

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.

The Formalising Fermat project 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ős was solved by machine, taking the field totally by surprise. The whole affair has forced Buzzard to rethink things.

“I was always quietly confident that we were going to succeed.
But now we’re two years in and AI has got so good that now my instinct is, this is ridiculous – what I said I’d do is ridiculous. Let’s just do something 10 times better,” he says.

Wiles’s 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’s original project was to formalise only the final paper – or more recent improvements of it, at least – but assume that everything it rested on was correct.

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.

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.

Hang Lu Su at Imperial College London is one of the researchers taking part in the workshop. She used ChatGPT to teach herself Lean just six months ago and is now working here at the cutting edge.

Most mathematicians she knows still use pen and paper, so the use of AI and formalisation on display here is in no way representative of the field today, but she believes it could be a glimpse of its future. “I feel like there’s an industrialisation of the intellectual process [occurring],” says Su. “If anything, the AI tools are working so well that it’s a bit like: ‘OK, we just let [the AI model] Claude work, and then what do we do?’”

A variety of tools are in use here, from the free and open source to the latest and most expensive models from US start-ups. Nobody at the event can say precisely how much money is being spent on tokens, the units of AI intelligence by which access is charged, but most agree that it will easily run into thousands of pounds a day. “I’m burning tokens like I’m not paying the bill, definitely,” says Su.

But to solve these knotty mathematical problems, the group will need quality as well as quantity. Su explains that she and a colleague were both trying to formalise the same bit of maths on the first day of the workshop. She arrived at an 800-word solution, while her colleague found a 400-word one. Both could equally be said to have proved the theorem in question. But the shorter version, compiled faster, would be easier for AI to work on going forward and was also more easily comprehended by a human.

The code created by AI can be verbose, clunky and take a long time to run, says Buzzard. It sometimes relies on using obscure features within Lean in unintended ways, which won’t compile properly when updated versions are released.

Many of the curators of the Mathlib library are cautious about adding lots of this AI-generated Lean code, even if it proves theorems, for this very reason, says Buzzard. Currently, the code in that library is expertly and carefully written by human mathematicians, who ensure it is efficient, concise and readable to humans. It is a solid foundation for future work. The code being created at this workshop is rather different.

“We’re building a layer of slop on top – let’s just call it slop – and now the question is, what happens when we try to move the next layer? Can we build the next layer on top or does it just grind to a halt?” asks Buzzard.

These advances are also throwing up philosophical and existential questions for mathematicians. At the very least, the tools available to researchers are changing, and therefore so will their job – but at the most techno-optimist end of the spectrum, AI may end up taking over and expanding the borders of known mathematics on its own, outpacing and replacing human thought.

“We’re all doing [maths] because we love it, and we think it’s important. But now AI is coming along, and suddenly the question is, actually, why are we doing this? What’s the point of it?” says Buzzard. “If a machine proves a theorem but no human can understand it, then what have we achieved?”

Those questions are even more pointed when the maths in question is abstract in the extreme, sitting in the sort of world that includes 38-dimensional spheres or complex problems without obvious immediate application. “There’s this abstract world, but does that abstract world exist if humans aren’t there to appreciate it?” asks Buzzard.