In July 2022, Viazovska became an overnight international sensation. She was awarded the prestigious Fields Medal for her pioneering work on the problem of sphere packing. Sometimes called the Nobel Prize of Mathematics, this award represents one of the highest honors bestowed in the profession. Viazovska’s research focused on solving two complex versions of the sphere-packing problem, which examines the densest arrangement of identical circles or spheres within n-dimensional space.
Her resolutions of 8-dimensional and 24-dimensional sphere packing extended the frontiers of what mankind knew mathematically. In a surprising development, researchers have since been able to autoformalize these proofs. The accomplishment is the result of joint work between AI and human mathematicians and has the potential to change how we verify mathematical proofs.
The Sphere-Packing Problem and Its Significance
The sphere-packing problem has long vexed mathematicians, who seek to understand how tightly they can fit the same-size spheres together in different dimensions. The Viazovska solutions for the 8-dimensional case and the 24-dimensional case each stand as historic milestones in this continued mathematical pursuit.
Sidharth Hariharan first put this proof in formal language for 8-dimensional sphere-packing. His goal was to use those proof techniques to develop a deeper understanding of mathematical concepts. His first meeting with Viazovska in Lausanne, Switzerland, paved the way for exciting new creative collaboration.
“When they reached out to us in late January saying that they finished it, to put it very mildly, we were very surprised,” – Sidharth Hariharan
Hariharan and his collaborators created a plan to visualize the elements within the 8-dimensional proof. This ambitious work paves the way for deeper and broader advancements across the field.
AI’s Impact on Proof Formalization
One of the most influential actors in this space is Gauss, a reasoning agent created by Math, Inc. This readily available AI model has already proven outstanding abilities in formalizing mathematical proofs. Beautifully enough, it autoformalized the proof of 8-dimensional sphere-packing in under five days. It even caught an errant “the” typo that slipped through in our original!
Riding this success, Math, Inc. put out an improved version of Gauss, which took on the tougher 24-dimensional proof. That initial version, it’s worth noting, took two weeks to build and was more than 200,000 code lines long!
“And it was actually significantly more involved than the 8-dimensional case, because there was a lot of missing background material that had to be brought on line surrounding many of the properties of the Leech lattice, in particular its uniqueness,” – Jesse Han
This advanced reasoning agent can conduct literature searches, generate Lean code, and run verification tooling, showcasing its versatility and utility in mathematical research.
Collaboration Between AI and Humans
The teamwork of AI and human mathematicians has helped reach a historic milestone for sphere-packing proofs. It represents a historic victory for the success of the entire discipline of mathematics. Hariharan and CEO Jesse Han of Math, Inc. understand the importance of replacing open-ended human contribution with technology. These ongoing efforts have enabled these groundbreaking achievements to be commemorated.
“I think the end result of technology like this will be to free mathematicians to do what they do best, which is to dream of new mathematical worlds,” – Jesse Han
The autoformalization process detailed here represents an extraordinary breakthrough in the field of proof verification. Even experts as wide-ranging as planning guru Liam Fowl understand that the power of such collaboration.
“These new results seem very, very impressive, and definitely signal some rapid progress in this direction,” – Liam Fowl
Beyond being simply, or maybe not so simply, an endorsement of the underlying mathematical proofs, formal verification is like a rubber stamp certifying those proofs are correct.
The Future of Mathematical Proofs
As Math, Inc. continues to refine its technology and enhance Gauss’s capabilities, the potential for applying AI in mathematics is expanding. The path from early stage research discoveries to public availability illustrates the dedication to playing a leading role in unlocking new mathematical knowledge through innovative approaches.
“We had been building the project’s repository for about 15 months when we enabled public access in June 2025,” – Sidharth Hariharan
With the aid of AI, thanks to these developments, mathematicians can have machines automate typically manual verification tasks. This gives them the bandwidth to concentrate their efforts on addressing bigger challenges and thinking through innovative approaches.