Watershed Moment for AI–Human Collaboration in Math
IEEE Spectrum reports that Ukrainian mathematician Maryna Viazovska’s Fields Medal-winning proofs on sphere packing have been formally verified with significant assistance from AI, marking a major advance in human-AI collaboration for mathematical research.
The formalization of Viazovska’s 8-dimensional sphere-packing proof was announced on February 23, according to the IEEE Spectrum article. The work, carried out through the Formalising Sphere Packing in Lean project, combines human mathematicians with Gauss, an AI reasoning agent developed by startup Math, Inc. The achievement signals rapid progress in AI-assisted formal proof verification, a process that provides computer-checked certification of mathematical reasoning.
Viazovska received the Fields Medal in July 2022 for solving the sphere-packing problem in 8 and 24 dimensions. The problem asks how densely identical spheres can be packed in n-dimensional space. While solutions are known in two and three dimensions, higher dimensions present extreme mathematical challenges. Viazovska proved that the E8 lattice provides the optimal packing in 8 dimensions using powerful mathematical functions known as (quasi-)modular forms. She later collaborated on a similar proof for the Leech lattice in 24 dimensions. These results have practical applications in error-correcting codes used by smartphones and space probes.
Although the proofs were accepted by the mathematical community and earned Viazovska the Fields Medal, formal verification—where a computer rigorously checks every step—remains a separate and difficult task. Progress in AI-assisted formalization has accelerated since 2022, particularly with tools like Lean, a programming language and proof assistant that allows mathematicians to write proofs verifiable by computer.
The project originated from a chance meeting in Lausanne, Switzerland, between Viazovska and then-undergraduate Sidharth Hariharan, who was already skilled in formalizing proofs. Hariharan explained to Viazovska how formalization deepened his understanding of mathematical concepts. This conversation led to the launch of the Formalising Sphere Packing in Lean project in March 2024. The team created a human-readable “blueprint” to map out the proof’s components, identify gaps, and formalize missing elements in Lean.
Hariharan, now a first-year Ph.D. student at Carnegie Mellon University, recalled that the project’s repository was made public in June 2025 after 15 months of development. In late October, Math, Inc. reached out, offering the capabilities of its AI system Gauss.
Gauss is a specialized reasoning agent that interleaves natural-language reasoning with formal Lean code. According to Jesse Han, Math, Inc. CEO and cofounder, the system can conduct literature searches, call tools, write Lean code, take notes, run verification tooling, and execute the Lean compiler. The company previously gained attention for using Gauss to formalize the strong prime number theorem in three weeks—a task that Fields Medalist Terence Tao and Alex Kontorovich had been pursuing.
Math, Inc. informed the sphere-packing team that Gauss had resolved 30 “sorrys”—intermediate facts the human team needed proved. Some of these were integrated into the project. One AI contribution even helped identify and correct a typo in the human work, according to Hariharan, who described the collaboration as fruitful.
The IEEE Spectrum article describes the formalization of the 8-dimensional proof as a watershed moment for autoformalization. AI expert Liam Fowl, a Princeton University postdoc not involved in the project, called the results “very, very impressive” and indicative of rapid progress in the field. Fowl compared formal verification to a “rubber stamp” that certifies the correctness of mathematical reasoning.
The project also aims to tackle the more complex 24-dimensional proof, though the article notes a period of reduced communication from Math, Inc. after initial contributions.
Impact
This development carries significant implications for both mathematicians and the broader AI industry. Formal verification provides an unprecedented level of certainty in mathematical proofs, potentially accelerating discovery in complex fields. For developers working on AI reasoning systems, the success of Gauss demonstrates the value of specialized agents that combine language understanding with formal verification tools.
Users and researchers in mathematics stand to benefit from more reliable, computer-checked proofs that reduce human error. The collaboration model—humans creating blueprints and high-level strategy while AI handles tedious intermediate steps—could become a standard workflow in mathematical research.
In the competitive landscape, Math, Inc.’s progress with Gauss positions the startup as a notable player in AI for science. The company’s ability to contribute meaningfully to a Fields Medal-level proof highlights how AI tools are moving beyond simple assistance into substantive research partnership.
What's Next
The article indicates ongoing work toward formalizing the 24-dimensional proof, which is substantially more complex. While specific timelines were not detailed, the rapid progress seen in the 8-dimensional case suggests continued advancements in AI formalization capabilities.
As tools like Gauss mature, experts anticipate broader application across mathematical domains. The integration of AI reasoning agents with proof assistants such as Lean may eventually support larger-scale formalization projects that would be impractical for humans alone.
Further collaboration between human mathematicians and AI systems is expected to yield additional breakthroughs, potentially transforming how mathematical knowledge is established and verified in the coming years.