AI just verified a proof that earned one of math’s most prestigious prizes. Math will never be the same | Kit Yates
Earlier this month an artificial intelligence (AI) startup announced that their AI agent had confirmed a proof of two cases of the devilishly challenging “higher dimensional sphere-packing problem.” In 2022, the proofs earned Ukrainian mathematician Maryna Viazovska a Fields Medal, one of the most prestigious prizes in math.
This was a giant step forward, and speaks to the emergence of a quiet revolution in the field.
On the surface, it may not seem so extraordinary. After all, mathematicians have long used tools to extend their abilities — abacuses, slide rules, calculators and, eventually, computers. Yet none of these tools ever replaced mathematicians; they just allowed us to refocus our attention on more interesting problems. The arrival of AI in mathematics might feel like another step in that same process. But there’s a crucial difference: This time, the tools aren’t just helping us calculate; they’re helping us reason, or at least perform many of the routines that sit underneath human reasoning.
Article continues below
Kit Yates is a professor of mathematical biology and public engagement at the University of Bath in the U.K.
The change has been coming for a while. For years, our biggest proofs have not been the endeavours of single mathematicians. Many modern research articles in pure mathematics now rely on huge conceptual frameworks, long dependency chains, and catalogs of results that no single person can fully internalize. Computers have played a role in large proofs before, like the four-color theorem and the Kepler conjecture. But what’s changing now is the level of autonomy and reliability we can expect from AI systems working alongside formal proof assistants — programs designed to check mathematical arguments.
But until recently, turning cutting‑edge proofs into machine‑checkable form required specialists to devote months or years to the work.
These formal verification languages express mathematical arguments in a way a computer can check step by step, guaranteeing that every part of the proof is logically sound. Take the language Lean, for example. Unlike ordinary mathematical writing, Lean requires every definition and inference to be made explicit, and it checks each step mechanically and methodically. It’s unforgiving, but in a productive way: If the argument is passed by Lean, that, in theory, means the proof doesn’t have hidden assumptions or leaps of faith. Over the past few years, Lean has become a proving ground for research‑level mathematics, and mathematicians have been building “libraries” to support increasingly complex problems.
These libraries are huge collections of definitions and already‑verified theorems that have been painstakingly programmed, allowing researchers to prove new results in the language. But until recently, turning cutting‑edge proofs into machine‑checkable form required specialists to devote months or years to the work.
That’s the context in which the recent formal verification of Viazovska’s higher-dimensional sphere‑packing results should be understood. The sphere‑packing problem asks how tightly identical spheres can be packed together in spaces of any dimension, not just the 3D world we live in. Before Viazovska’s breakthrough, the sphere‑packing problem had only been fully solved in dimensions one, two and three, with all higher‑dimensional cases remaining open. Viazovska’s proofs of the eight- and 24‑dimensional sphere-packing problem, are profound pieces of mathematical insight that solve problems previously thought out of reach.
Fields Medal-level advancements
The recent important step forward is that a human-AI collaboration has now translated those arguments into fully verified Lean code, which then checked every step. The sheer scale of that achievement is astonishing; these are recent Fields Medal‑level results, and they have now been certified at a level of detail and certainty that would be impossible for individual referees, or even large human specialist teams, to reproduce unaided.
A key ingredient was Math, Inc.‘s AI reasoning agent Gauss which had played a vital role in helping to turn human mathematical arguments into Lean proofs. The AI system wasn’t working entirely unaided; mathematicians still had to set out the blueprint, shape the overall structure, and ensure the right concepts were in place. But once that scaffolding existed, the system could fill in the missing pieces at extraordinary speed. In the eight‑dimensional case, it completed work that the human contributors had estimated would take them months, and it did so in days. The 24‑dimensional case, which is even more intricate, followed soon after.
The sphere‑packing project is probably the clearest demonstration yet of what is becoming possible.
This is more than a technical accomplishment. It points toward a shift in the way mathematicians might organize their work. When I talked to UCLA mathematician and Fields Medalist Terence Tao, he suggested that the immediate value of AI might come not from cracking our hardest problems outright but from relieving us of the drudgery — the thousand small cases that are conceptually straightforward but too time‑consuming for any one person to tackle by hand.
Some AI systems, he argued, are already surprisingly good at handling these tasks, letting mathematicians devote their attention to strategy rather than bookkeeping. Tools like Lean matter because they give us a way to separate the creativity of generating ideas from the rigor of checking them.
AI proof expert Kevin Buzzard, of Imperial College London, expressed a complementary view. He worries, rightly, about the dangers of relying on large language models that sound authoritative without guaranteeing correctness. But he also argues that formalization offers a way through this. In Lean, if the program accepts all the steps, then it’s a valid proof. This doesn’t mean the computer has necessarily done something “intelligent” but rather that the formal verification language leaves no room for hidden steps or suggestive-but-incomplete arguments. The challenge, as he sees it, is that most of modern mathematics still hasn’t been translated into formal libraries, so the systems don’t yet have the concepts they need.
This latest step forward suggests the gap is beginning to close. The sphere‑packing project is probably the clearest demonstration yet of what is becoming possible.
None of this means mathematicians are on the brink of extinction. In fact, I suspect the opposite is true. As the space of verifiable mathematics expands, so too does the need for people who can pose good questions, create new definitions, and recognize when an argument is genuinely insightful. But we are going to have to adapt. We may find ourselves acting more like scientific-instrument builders and less like lone theorists, weaving together human intuition and AI tenacity to produce machine‑verified certainty.
Mathematics has always moved forward by partnering with assistive tools. AI doesn’t change that practice; it just takes it to the next level. Mathematical concepts won’t get easier to prove, but our capacity to test, verify and build upon them will surely increase.
Opinion on Live Science gives you insight on the most important issues in science that affect you and the world around you today, written by experts and leading scientists in their field.
