AI helps formally verify the proofs of a Fields Medal winner for the first time

In mathematics there is a kind of recognition that ranks above any award: a computer confirming that your proof is flawless. The proofs by Ukrainian mathematician Maryna Viazovska, which earned her the Fields Medal in 2022, have just passed exactly that test, with an unprecedented degree of help from artificial intelligence.

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

In three dimensions, the best arrangement is the pyramid of balls familiar to anyone who has seen a stack of oranges at a market stall. But as the number of dimensions grows, the problem becomes monstrously hard. In 2016, Viazovska proved that the symmetric E8 structure is the best packing in eight-dimensional space, and soon afterward, together with colleagues, she established that the Leech lattice is optimal in 24 dimensions.

Abstract as they seem, these results bear directly on error-correcting codes used by smartphones and space probes.

The mathematical community checked the proofs and accepted them as correct, hence the Fields Medal. But formal verification, in which a computer program checks every logical step of a proof, is a task of a fundamentally different scale. A human referee can miss a subtle error; a computer will not. That is why formalizing complex proofs is considered the "gold standard" of reliability in modern mathematics.

It all started with a chance meeting. In Lausanne, third-year student Sidharth Hariharan told Viazovska how he used formalization of proofs in the Lean language to understand mathematical concepts deeply. Lean is both a programming language and a so-called "proof assistant" that lets users write mathematical reasoning in a form a computer can check for absolute correctness.

Viazovska was interested, and in March 2024 the project Formalising Sphere Packing in Lean was born. Experts from Imperial College London, the University of East Anglia and the University of California, Berkeley joined it. The team built a "blueprint," a human-readable map of all the elements of the eight-dimensional proof, marking which were already formalized and which remained to be translated into Lean.

Two years of painstaking work followed, and then came a turning point. 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" that can alternate natural-language reasoning with fully formalized mathematical derivation. In effect, it is an AI that can automatically translate mathematical proofs into a language a computer verifier understands. Gauss radically sped up formalization, allowing the team to finish what would otherwise have taken years more of manual work.

The result drew a strong response in the scientific community. "These new results look very, very impressive and definitely signal rapid progress in this direction," said Liam Fowl, a postdoc at Princeton University and an expert on AI reasoning who was not involved in the project. In his words, formal verification is a kind of "seal of quality," an absolute guarantee that every step of the logical reasoning is correct.

The significance of this breakthrough extends far beyond a single proof. Until recently, formalizing serious mathematical results was so labor-intensive that only a handful of projects took it on. If AI systems like Gauss can systematically speed up this work, mathematics gains something unprecedented: the ability to verify at scale proofs accumulated over decades. This does not replace mathematicians: Viazovska still achieved an intellectual feat that a machine cannot repeat. But AI proves indispensable in the most routine and high-stakes part of the work: checking that brilliant intuition did not lead to an error in one of thousands of logical steps.

We are watching the birth of a new model of collaboration: humans formulate ideas and build proofs, and the machine guarantees they are flawless. For a field where one unnoticed error can cast doubt on decades of later research, this is more than a convenience; it changes how the discipline works.