Mathematicians continue to use technology to prove an astounding breakthrough in Landau’s proof of sphere-packing, representing revolutionary progress made through technology in the mathematical field. This strange region has confounded experts for decades. Maryna Viazovska made waves in 2016 by providing a solution to the sphere-packing problem in both two and three dimensions. She presented the best known packings of equal spheres in a variety of dimensions. Her contributions provided a foundation for future investigations into higher-dimensional packing. This unprecedented endeavor resulted in historic outcomes accomplished by an extraordinary, cross-disciplinary team that included innovators Sidharth Hariharan.
The sphere-packing problem investigates how densely identical circles, spheres, or their higher-dimensional counterparts can be packed within a given space. When you apply this problem to two dimensions, the structure that results is a honeycomb, it’s the most optimized structure. In three dimensions, spheres stacked in a pyramid get the densest packing. Viazovska’s work extended to eight-dimensional and twenty-four-dimensional spheres. She established that the E8 configuration is indeed the best possible in eight dimensions, just as the so-called Leech lattice has this honor in twenty-four dimensions.
Collaborative Efforts and Innovations
Sidharth Hariharan, now at Carnegie Mellon University, has been in the thick of proof verification of sphere-packing. He has worked with Jesse Han and others to formalize these proofs. Collectively, they used innovative computational approaches to make this essential discovery possible. This time, the team was able to autoformalize Viazovska’s 24-dimensional proof, over 200,000 lines of code, in a mere two weeks.
That’s one of the many goals of this collaboration — to emphasize the need to build on existing mathematical frameworks. They are quick to highlight the role of past researchers, which set the stage for reaching these historic outcomes.
“They told us that they had finished 30 ‘sorrys,’ which meant that they proved 30 intermediate facts that we wanted proved.” – Sidharth Hariharan
The Formalising Sphere Packing in Lean project started in March 2024. This new endeavor is a critical opportunity to move the needle on modernizing proof-verify processes. This new initiative is meant to take advantage of emerging computational tools to make proofs more efficient and accurate.
Math, Inc. had a pretty outstanding coup for an announcement. For example, their reasoning agent, Gauss, autoformalized Maryna Viazovska’s 24-D sphere-packing proof in an hour. They accomplished this monumental task in just two weeks. Furthermore, Gauss efficiently handled the 8-dimensional case in just five days, during which it identified and corrected a typo in the original publication.
Technological Advances and Impact on Mathematics
As Jesse Han pointed out, there’s a lot of complexity that goes into validating these proofs.
Human mathematicians and automated reasoning agents are working together in creative and powerful new ways. This kind of synergy has the potential to significantly improve the future of mathematical research.
“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
We’re living through tremendous technological change! Those in the field are optimistic that this improvement will free mathematicians to focus on creative and original problem-solving rather than becoming bogged down by the verification process. Han said he remains hopeful that technology can play a big role in what math looks like.
The Future of Mathematical Exploration
Beyond the profound assistance promised by devices of automated reasoning agents, they might replace long-established traditional roles in mathematical research. As the language of programming progresses, so will the way mathematicians engage with computational tools.
“But at the end of the day, this is technology that we’re very excited about, because it has the capability to do great things and to assist mathematicians in remarkable ways.” – Sidharth Hariharan
The potential for automated reasoning agents extends beyond mere assistance; they could redefine traditional roles within mathematical research. As programming evolves, so too will the interaction between mathematicians and computational tools.
“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. 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