Maryna Viazovska is a mathematician best known for her remarkable feats in the world of sphere packing. Thanks to the support and application of artificial intelligence, she has since made groundbreaking strides in her research. In 2016, Viazovska showed a remarkable new approach to the sphere packing problem. She determined the best packing for like spheres in 2D and 3D. Her work has not only earned her significant accolades, including the prestigious Fields Medal in July 2022, but has sparked a collaboration between AI technology and mathematical proof verification.
The sphere packing problem is the mathematical inquiry into how closely the same circles or spheres can be packed into ndimensional space. In two dimensions, the honeycomb structure squeezes circles closer together than any other form. In three dimensions, packing spheres into a pyramid produces the most efficient packing layout. In one of those discoveries, however, Viazovska proved something remarkable. Providing the final piece of evidence that the symmetric arrangement known as E8 delivers the most efficient packing in eight dimensions. She collaborated with other mathematicians to validate a thrilling find. Jointly, they determined that the Leech lattice is the optimal configuration for sphere packing in 24 dimensions.
A Meeting of Minds
In Lausanne, Switzerland, Viazovska met with Sidharth Hariharan, which re-fueled her interest in sphere packing proofs. Their joint efforts resulted in the creation of a project called “Formalising Sphere Packing in Lean” in March 2024. Lean is an expressive functional programming language and proof assistant. It provides a language for mathematicians to write proofs in, which a computer can then check for correctness.
In fact, this project is a truly impressive advance at the intersection between artificial intelligence and cutting-edge mathematical research. These works come together in the hope that human ingenuity plus AI will increase the rigor and reliability of mathematical proofs.
“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
Retrospectively, our project Formalising Sphere Packing in Lean is a perfect example of this synergy. Math, Inc. has developed a dynamic, new electronic version of Gauss. This powerful novel reasoning agent is now capable of performing literature searches, using external tools like GPS systems, and producing Lean code effortlessly. This innovation has advanced the entire discipline of mathematics by automating proof verification processes that may otherwise be intractably complex.
Impressive Achievements
Gauss accomplished an impressive feat by autoformalizing Viazovska’s proof regarding 24-dimensional sphere packing, comprising over 200,000 lines of code, within just two weeks. These developments have led to autoformalization’s most exciting and transformative moment, as well as for AI-human collaboration in mathematics more broadly.
On February 23, the news summary for formal proof of the 8D sphere packing finally was released. This milestone reveals the exciting capability of AI-driven tools to help mathematicians reach truly revolutionary discoveries.
“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 insights and expertise shared by our human collaborators proved instrumental in helping lay the groundwork for these milestones. Jesse Han pointed out the need for collecting a large amount of background material on the Leech lattice. This knowledge was critical for pushing this work forward.
“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
The Future of Mathematics and AI
This recent re-surfacing of proofs of sphere packing may very well be a glimpse into the new world of mathematical research combined with AI. Liam Fowl noted how striking these results are and that this underlines a fast-moving field.
“These new results seem very, very impressive, and definitely signal some rapid progress in this direction.” – Liam Fowl
Researchers are just beginning to explore AI’s capabilities when it comes to mathematics. It is an exciting exploration with tremendous potential for these technologies to help the field of mathematicians. Hariharan was excited about technology’s potential, saying that it will help make amazing progress in mathematical research possible.
“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 partnership between AI tools such as Gauss and human mathematicians is an encouraging sign of how technology can sharpen and deepen proof verification processes. Further evidence of this shift is seen in the changing role of programmers. As Han said, there’s been a huge shift in the nature of programming.
“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.” – Jesse Han