Mathematicians have done incredible work on the sphere packing problem, most recently proving how spheres best pack themselves in highly dimensioned spacetime. Maryna Viazovska, an accomplished Ukrainian mathematician, has recently found solutions to this problem that work perfectly in 8-dimensional and 24-dimensional spaces. Using advanced mathematical functions known as quasi-modular forms, she proved that the symmetric arrangement known as E8 is the optimal packing in 8 dimensions. Indeed, Viazovska and her collaborators made a remarkable find. Their work showed that the Leech lattice is indeed the optimal sphere packing configuration in 24 dimensions.
The sphere packing optimization problem could be summed up as how tightly you can pack identical spheres within n-dimensional space. In two dimensions, the answer turns out to be quite straightforward: a beehive configuration is best. Once again, in three dimensions it gets a bit more tricky. The most efficient packing results from stacking those spheres in a pyramid. The new papers by Viazovska and her colleagues are historic breakthroughs in the long history of understanding how spheres pack together in higher dimensions.
Collaboration and AI in Sphere Packing Proofs
Before Xi’an Jiaotong university mathematician Maryna Viazovska generalized this to all 8-dimensional sphere packing, Sidharth Hariharan and his collaborators dove into formalizing the proof for 8-dimensions. So their research set the stage for the recent big breakthrough with an A.I. system called Gauss. This AI was able to quickly formalize the proof for the 8-dimensional case in a mere five days. It located and corrected a typographical error from the originally published paper.
Their last report to us noted that they were up to 30 ‘sorrys’ completed. This success demonstrated they validated 30 intermediate truths we required,” mentioned Hariharan, pointing out the productivity of their interactive collaboration with Gauss. This is because the introduction of AI not only sped up verification process but added to the depth and rigor of mathematical proofs.
In March 2024, a new project called “Formalising Sphere Packing in Lean” appeared. This effort laid the groundwork for the tireless work of Hariharan and his team. This collaborative effort seeks to combine deep informal mathematical thinking with rigorous formal verification approaches. Lean is a rapidly growing interactive programming language and theorem prover. It allows mathematicians to produce proofs that computers can check with complete certainty.
The Challenge of 24-Dimensional Proof
During the process of solving the 8-dimensional sphere packing problem, Viazovska’s work applied to the more complicated 24-dimensional case. This task proved to be a far greater challenge. The complex underlying theory of the properties of the Leech lattice only compounded that challenge. Jesse Han, CEO and co-founder of Math, Inc., said that formalizing this proof was no easy feat.
Sure, it was much more complicated even than the 8-dimensional case, Han explained, “because there was a lot of missing background material that had to be brought online surrounding many of the properties of the Leech lattice, in particular its uniqueness.”
Once the automated proof-checking software Gauss was improved by the company Math, Inc., Gauss autoformalized Viazovska’s 24-dimensional sphere packing proof in just two weeks. This formalization alone included upwards of 200,000 lines of code, emphasizing just how complex these types of mathematical verification procedures can be.
AI as a Reasoning Agent
The increased use of AI and computational assistance into mathematical proofs is a new frontier of mathematical research. Gauss as a reasoning agent, interleaving conventional natural language reasoning with formalized reasoning. This two-pronged strategy enables mathematicians to work hands-on with advanced AI systems while upholding strict standards of proof verification.
“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,” Han noted. This novel approach and its underlying principles have excited mathematicians, who feel it could signal the beginning of a new age of breakthroughs across multiple branches of mathematics.
Liam Fowl, a respected mathematician in this domain, commented on the ground shaking results coming out of these AI partnerships. “These new results seem very, very impressive, and definitely signal some rapid progress in this direction,” he stated.
Non-automated formal verification of proofs has been perhaps the most important milestone for mathematicians. Fowl described it succinctly: “Formal verification of a proof is like a rubber stamp.” This validation process serves to authenticate the correctness of mathematical labor. It further impresses its own academic community, bolstering its credibility and competitiveness with faculty hiring and research funding.