Earlier this month, an artificial intelligence (AI) startup announced that its AI agents had seen evidence of two cases of the devilishly difficult “high-dimensional sphere filling problem.” In 2022, this proof earned Ukrainian mathematician Marina Vyazovska the Fields Medal, one of the most prestigious awards in mathematics.
This is a huge step forward and signals a quiet revolution taking place in this field.
On the surface, it might not seem all that special. After all, mathematicians have long used tools that extend their abilities: abacuses, slide rules, calculators, and eventually computers. But none of these tools replaced mathematicians. They just allowed us to refocus our attention on more interesting issues. The arrival of AI in mathematics may feel like another step in the same process. However, there is a crucial difference. This tool does more than just assist with calculations. They help us reason, or at least perform many routines that are beneath human reasoning.
Article continues below
you may like
Kit Yates is Professor of Mathematical Biology and Public Engagement at the University of Bath, UK.
Change has been going on for a while. For many years, our greatest proofs were not due to the efforts of a single mathematician. Many modern research papers in pure mathematics now rely on large conceptual frameworks, long chains of dependencies, and catalogs of results that cannot be fully understood by a single person. Computers have previously played a role in large-scale proofs such as the four-color theorem and the Kepler conjecture. What is changing now, however, is the level of autonomy and trustworthiness we can expect from AI systems working in conjunction with formal proof assistants (programs designed to check mathematical arguments).
But until recently, converting state-of-the-art proofs into a machine-checkable format required experts to spend months or years.
These formal verification languages express mathematical arguments in a way that computers can check step by step, ensuring that all parts of the proof are logically sound. For example, consider Lean language. Unlike regular mathematical descriptions, Lean requires all definitions and inferences to be made explicitly, and each step is checked mechanically and systematically. It’s brutal, but it’s productive. If an argument is passed by Lean, it theoretically means that there are no hidden assumptions or leaps of faith in the proof. In recent years, Lean has become a testing ground for research-level mathematics, with mathematicians building “libraries” to support increasingly complex problems.
These libraries are vast collections of carefully programmed definitions and already verified theorems that allow researchers to prove new results in this language. But until recently, converting state-of-the-art proofs into a machine-checkable format required experts to spend months or years.
This is the context in which the recent formal validation of Viazovska’s high-dimensional sphere packing results should be understood. The sphere packing problem asks how closely identical spheres can be packed together in any dimension of space, not just the 3D world we live in. Prior to Wiazowska’s breakthrough, the sphere packing problem had only been fully solved in one, two, and three dimensions, leaving all higher-dimensional cases unsolved. Wiazowska’s proof of the 8- and 24-dimensional sphere packing problem is a profound piece of mathematical insight that solves a problem that was previously considered inaccessible.
Field medal level promotion
An important recent step forward is that human-AI collaboration has translated these arguments into fully validated lean code, checking every step. The scale of the results is astonishing. These are recent Fields Medal-level results, proven with a level of detail and certainty that would be impossible for individual judges or even large teams of human experts to reproduce without assistance.
A key element was Math, Inc.’s AI reasoning agent Gauss, which played a key role in turning human mathematical arguments into lean proofs. AI systems did not function entirely on their own. Mathematicians still had to create the blueprint, form the overall structure, and ensure that the right concepts were introduced. But once that scaffolding existed, the system was able to fill in the gaps with incredible speed. For 8D, we completed work in days that human contributors estimated would take months. More complicated 24th dimension events soon followed.
What to read next
The sphere stuffing project is perhaps the clearest demonstration of what is becoming possible.
This is not just a technical achievement. It signals a change in the way mathematicians organize their research. When I spoke with UCLA mathematician and Fields Medalist Terrence Tao, he suggested that the immediate value of AI may lie not in completely solving the most difficult problems, but in freeing us from the tedious work of thousands of small cases that are conceptually simple but too time-consuming for one person to tackle by hand.
Some AI systems are already surprisingly good at handling these tasks, he argued, allowing mathematicians to focus on strategy rather than bookkeeping. Tools like Lean are important because they provide a way to differentiate between the creativity that generates ideas and the rigor that checks them.
Kevin Buzzard, an AI certification expert at Imperial College London, also offered a complementary view. He is rightly concerned about the dangers of relying on large language models that sound authoritative without guaranteeing their correctness. But he also claims that formalization provides a way to solve this. In Lean, if a program accepts all steps, it is a valid proof. This does not mean that the computer necessarily did anything “intelligent”, but rather that formal verification languages leave no room for hidden steps or suggestive but incomplete arguments. The challenge, he sees, is that much of modern mathematics has not yet been translated into formal libraries, so the systems do not yet have the necessary concepts.
This latest advance suggests that gap is starting to close. The sphere stuffing project is perhaps the clearest demonstration of what is becoming possible.
This does not mean that mathematicians are on the verge of extinction. In fact, I suspect the opposite is true. As the realm of testable mathematics expands, so does the need for people who can ask the right questions, create new definitions, and recognize when an argument is truly insightful. But we have to adapt. We may find ourselves acting more like scientific instrument makers than lone theorists, interweaving human intuition with the tenacity of AI to create machine-tested certainty.
Mathematics has always advanced in conjunction with supporting tools. AI won’t change those habits. Just take it to the next level. Proving mathematical concepts is never easy, but your ability to test, validate, and build on them certainly improves.
Opinion on Live Science provides insight into the most important issues in science that affect you and the world around you today, written by experts in the field and leading scientists.
Source link
