Maryna Viazovska’s landmark achievement in solving the 24-dimensional sphere packing problem has recently received a burst of visibility after global developments intriguing artificial intelligence. In 2016, Viazovska proved two significant iterations of a highly abstract mathematical problem. She proved solutions exist in eight and 24 dimensions as well. Her achievements have now inspired a project that utilizes AI to formalize these proofs, showcasing how technology can enhance mathematical understanding and exploration.
The sphere packing problem is the question of how closely the same sized circles or spheres can be packed in a space of n-dimensions. In two dimensions, the most optimal packing is a honeycomb lattice. In three dimensions, packing spheres in a pyramid maximizes the packing efficiency. Viazovska’s explosive work won her the top prize in mathematics, the Fields Medal. She proved that the E8 symmetric packing is the best possible packing solution in eight dimensions. Additionally, she, with her co-authors, proved that the Leech lattice is the densest possible packing arrangement in 24 dimensions.
The Role of AI in Mathematical Proofs
Gauss demonstrated its might by autoformalizing Viazovska’s 24-dimensional proof. It did this complex and remarkable accomplishment, which included more than 200,000 lines of code, in only two weeks! This magnificent accomplishment was itself a tremendous milestone because it needed no prior plan. In a letter to a colleague, Hariharan shared his surprise at the pace and goal-oriented nature of Gauss’s work.
“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
Gauss formally proved the eight-dimensional case, in addition to the 24-dimensional case. Astoundingly, he even found a typo in the published paper within five days of its appearance. This foundational ability highlights the revolutionary impact that AI can bring to the field of mathematics, equipping mathematicians with a powerful resource to verify intricate proofs.
The Complexity of Sphere Packing Proofs
The mathematics behind formalizing proofs is complicated and any attempt must start with a solid command of the basic ideas involved. Jesse Han, CEO and co-founder of Math, Inc., the creator of Gauss, calls Gauss a super reasoning agent. It does very well on traditional natural language reasoning and formalized logic. He emphasized that Gauss had to navigate substantial missing background information regarding the properties of the Leech lattice to accomplish its task effectively.
“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 online surrounding many of the properties of the Leech lattice, in particular its uniqueness,” – Jesse Han
Han noted that the accelerating research breakthrough occurred around mid-January. This resulted in a supercharged version of Gauss, capable of handling multi-part complex proofs with great ease. Human mathematicians plus AI math buddies. As demonstrated by this collaboration, the best synergy is with humans plus AI, not AIs replacing humans.
The Future of Mathematics and AI
Whatever concerns mathematicians have about AI, the mathematics profession will have to grapple with the reality of AI’s strong advance. As Fowl explained, he believes that given their potential impact, these developments are significant. He added that they demonstrate rapid advances in formal verification techniques. He compared the formal verification of a proof to a rubber stamp. This visualization serves to underscore its importance in the practice of accuracy and consistency in establishing mathematical truth.
“These new results seem very, very impressive, and definitely signal some rapid progress in this direction,” – Liam Fowl
The integration of AI into mathematics may ultimately free mathematicians to focus on imaginative pursuits rather than labor-intensive proof verification tasks. Han expressed optimism about this potential outcome:
“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