Mathematicians have spent over a century trying to understand the intricacies of sphere packing. This fascinating problem has applications that range from coding theory to crystallography. A few months ago, Maryna Viazovska took a huge step to shape the field of mathematics. She discovered extremely optimal solutions to sphere packing in both 8 and 24 dimensions. Her contributions to mathematics were rewarded with the esteemed Fields Medal this past July 2022. She adopted revolutionary new mathematical structures called (quasi-)modular forms. Together, these discoveries have dramatically deepened the world’s understanding of mathematics. They are at least partially responsible for opening the door to integrating artificial intelligence and machine learning into formal proof verification as well.
Viazovska’s exploration into sphere packing culminated in proving that the symmetric arrangement known as E8 is the optimal configuration for 8-dimensional packing. Together with other mathematicians, she proved that the Leech lattice is indeed the optimal sphere packing in 24 dimensions. That pioneering study has inspired an equally exciting, new joint undertaking. Sidharth Hariharan and his colleagues have been at the forefront of the effort to codify these proofs.
The Role of AI in Proof Verification
AI has recently made its mark as a most precious collaborator in the formal verification of mathematical proofs. One such exemplary case is Gauss, an AI developed by Math, Inc. Most notably, it autoformalized Viazovska’s 8-dimensional sphere-packing proof in five days flat. This remarkable achievement included identifying and rectifying a typo in the published paper, showcasing the potential of AI to augment traditional mathematical practices.
To Jesse Han, the CEO and cofounder of Math, Inc., Gauss is what he describes as a new “reasoning agent.” This new and groundbreaking tool combines natural-language reasoning with formalized reasoning. This combination allows it to handle even the most complicated mathematical ideas with much greater precision than traditional strategies.
“It’s a particular kind of language model called a reasoning agent that’s meant to interleave both traditional natural-language reasoning and fully formalized reasoning,” – Jesse Han
The progress didn’t end with 8 dimensions. Math, Inc. eventually released a successor to Gauss called Gauss 3. Today’s most powerful such tool autoformalized Viazovska’s 24-dimensional proof in less than two weeks. This theorem contains over 200k lines of code. This makes it all the more impressive and important to work that is getting done.
Formalizing Sphere Packing: A Collaborative Effort
Indian scientist Sidharth Hariharan did some of the most critical work to formalize Viazovska’s proofs. We were impressed that his pursuit of formal verification deepened his understanding of underlying mathematical concepts. He noted that making these proofs rigorous only added to what we already knew. While this process was certainly tedious, it opened up new frontiers of research.
To address these concerns, in March 2024 the FSPP — the initiative formally called the Formalising Sphere Packing in Lean — project — got started. The project’s goal is to build on Lean, a language and proof assistant that allows mathematicians to develop machine-checkable proofs. This process began by producing a human-readable “blueprint” for the 8-dimensional sphere-packing proof.
“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
The cooperative work capturing the parallel tracks taken by Hariharan’s team and AI tools has resulted in considerable martialization in methods for formal verification. Their study serves as an important reminder of the value of producing rich contextual material around arcane mathematical objects such as the Leech lattice.
“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
Future Implications of AI in Mathematics
AI’s introduction into the field of mathematics has the potential to greatly improve the process of developing and verifying proofs. Liam Fowl, a young mathematician watching these developments added that “recent results in this discipline have been truly from the extraordinary.” He noted that they represent a pace of change that’s unusually fast and might fundamentally change the way mathematicians go about solving problems.
“Formal verification of a proof is like a rubber stamp,” – Liam Fowl
As works such as Formalising Sphere Packing develop, they can produce profound advances in mathematics. Han expresses optimism about the potential future impact:
“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