Maryna Viazovska made a significant breakthrough in the realm of mathematics in 2016 by solving the sphere-packing problem in two distinct cases. Mathematicians and researchers have become ever more fascinated by this multi-faceted and difficult problem. It’s about figuring out the best packing of spheres in multiple dimensions. In two dimensions, Viazovska had previously found the solution corresponding to the honeycomb lattice as the densest sphere packing. At the same time, she decided that balls placed in a pyramid structure are the best arrangement in three dimensions.
Viazovska is applying her work to an entirely higher level! As a result, she showed that the symmetric arrangement known as E8 gives the most efficient packing in eight dimensions. Her groundbreaking contributions didn’t stop there, as illustrated in this powerful, unmissable collaboration. Together with her fellow researchers, she established the Leech lattice as the best packing answer in 24 dimensions. The formalization of the eight-dimensional sphere-packing proof announced this past February 23 made that day a watershed moment for mathematical research.
The Role of AI in Formalizing Mathematical Proofs
Fortunately, new artificial intelligence tools have been developed to help us all formalize its intricate, mathematical concepts. This breakthrough has provided further impetus to the sphere-packing proofs. Even more excitingly, a project called “Formalising Sphere Packing in Lean” started in March 2024, bringing AI even further into the fold of mathematical research. This project seeks to leverage Lean, an increasingly popular programming language and proof assistant, to formalize and clarify these mathematical proofs.
Notably, a significant development occurred when a researcher known as Gauss autoformalized Viazovska’s eight-dimensional case, relying on a preexisting blueprint. As legend has it, Gauss spotted a typographical error in the published paper. His correction serves as a good reminder about the dangers of slapdash work in mathematics.
Gauss’s accomplishments did not end there. In a span of just two weeks, he autoformalized the initial 24-dimensional sphere-packing proof. Remarkably, that’s what he teed up—without any manual or playbook to follow. “These new results seem very, very impressive, and definitely signal some rapid progress in this direction,” remarked Liam Fowl, a prominent figure in the field.
Challenges and Breakthroughs in Sphere Packing Research
The meticulous and delicate formalization process for the high dimensional 24 sphere-packing case was a test of will and focus. According to Jesse Han, one of the researchers involved, “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.” This only emphasizes the need for deep foundational theory and comprehension to solve these multidimensional, cross-cutting mega-issues.
Fostering honest collaboration between the parties was key Collaboration was key in tackling these challenges. Sidharth Hariharan and his team were just closing the loop on laying down formal proofs to really deepen their insights behind various mathematical ideas. It was their collaboration with AI tools that led to the real success. “They told us that they had finished 30 ‘sorrys,’ which meant that they proved 30 intermediate facts that we wanted proved,” explained Hariharan.
The teamwork and collaboration of human researchers plus AI has been a productive combination. “So it was a pretty fruitful collaboration,” Hariharan noted about their experience working with the AI-powered tools.
The Future of AI in Mathematical Research
As promising developments keep pouring in, one thing is certain AI’s role in mathematical research is growing exponentially. The autoformalization of sphere-packing proofs is a case in point. It shows AI’s role in accelerating the verification of complex mathematical ideas. The introduction of these reasoning agents has paved the way for new exploratory paths. These new, large AI models combine more informal, natural-language reasoning with fully formalized reasoning in fascinating ways.
Jesse Han emphasized this development by stating, “A programmer used to be someone who punched holes into cards, but then the act of programming became separated from whatever material substrate was used for recording programs.” This evolution is a part of a larger change within mathematics, as mathematicians use AI technologies more and more to help formalize proofs.
