AI helped formally verify a Fields Medal laureate’s proofs for the first time

In mathematics, there exists a special kind of recognition that stands above any award: when a computer confirms that your proof is absolutely flawless. The proofs of Ukrainian mathematician Marina Viazovska, which earned her the Fields Medal in 2022, have just undergone exactly such a verification — and did so with unprecedented participation from artificial intelligence.

Viazovska received her medal for solving one of the most elegant and treacherous problems in mathematics — the sphere packing problem. It sounds simple: how do you arrange identical balls in space as densely as possible? In two dimensions, every beekeeper knows the answer — honeycombs.

In three dimensions, a pyramid of spheres is optimal, familiar to anyone who has seen a stack of oranges on a shelf. But as the number of dimensions grows, the problem becomes fiendishly complex. In 2016, Viazovska proved that the symmetric E8 structure is the optimal packing in eight-dimensional space, and soon afterward, together with colleagues, established that the Leech lattice is optimal in 24 dimensions.

Despite their seeming abstraction, these results have direct relevance to error-correcting codes used by smartphones and space probes.

The mathematical community checked and recognized the proofs as correct — hence the Fields Medal. However, formal verification — a process in which every logical step of the proof is checked by a computer program — is a task of fundamentally different scale. A human reviewer can overlook a subtle error, a computer cannot. This is why the formalization of complex proofs is considered the "gold standard" of certainty in modern mathematics.

It all began with a chance encounter. In Lausanne, a third-year student Siddharth Hariharan told Viazovska how he used proof formalization in the Lean language for deeper understanding of mathematical concepts. Lean is simultaneously a programming language and a so-called "proof assistant," enabling the recording of mathematical reasoning in a form that a computer can verify for absolute correctness.

Viazovska became interested, and in March 2024, the project Formalising Sphere Packing in Lean was born. It was joined by experts from Imperial College London, University of East Anglia, and University of California, Berkeley. The team created a "blueprint" — a human-readable map of all elements of the eight-dimensional proof, marking which ones had already been formalized and which still needed to be translated into Lean.

Two years of painstaking work — and then a breakthrough occurred. In October 2025, the startup Math, Inc., which developed the AI system Gauss, joined the project. This is not an ordinary language model: Gauss is a "reasoning agent," capable of alternating between natural language reasoning and fully formalized mathematical inference. Essentially, it is an AI that can automatically translate mathematical proofs into a language comprehensible to a computer verifier. Connecting Gauss dramatically accelerated the formalization process, allowing completion of what would otherwise have taken years of manual work.

The result resonated significantly in the scientific community. "These new results look very and very impressive and certainly signal rapid progress in this direction," noted Liam Foul, a postdoc at Princeton University and expert in AI reasoning, who did not participate in the project. According to him, formal verification is a kind of "quality seal," an absolute guarantee that every step of logical reasoning is correct.

The significance of this breakthrough extends far beyond a single proof. Until recently, the formalization of serious mathematical results was such a labor-intensive process that only isolated projects undertook it. If AI systems like Gauss can systematically accelerate this work, mathematics will gain something unprecedented: the ability to mass-verify proofs accumulated over decades. This is not a replacement for mathematicians — Viazovska still accomplished an intellectual feat that machines cannot replicate. But AI proves indispensable in the most routine and crucial part of the work — verifying that brilliant intuition did not lead to an error in one of thousands of logical steps.

We are witnessing the birth of a new model of collaboration: humans formulate ideas and construct proofs, while machines guarantee their flawlessness. For mathematics, where one overlooked error can cast doubt on decades of subsequent research, this is not merely convenient — it is a paradigm shift.