Formal Verification of the Fields Medal via AI

An artificial intelligence has formally verified the mathematical proofs of Ukrainian mathematician Maryna Viazovska, winner of the Fields Medal in 2022. This result marks a significant advancement in AI's ability to assist in mathematical research.

The Fields Medal-winning research addressed the sphere packing problem, which asks how to arrange identical circles or spheres in n-dimensional space as densely as possible. Viazovska had solved the problem in 8 and 24 dimensions, demonstrating that specific configurations (E8 and Leech lattice) are the most efficient.

The Human-AI Collaboration

The "Formalising Sphere Packing in Lean" project came about thanks to the meeting between Sidharth Hariharan and Viazovska. Hariharan, an expert in formalizing proofs, collaborated with other experts to create a readable "blueprint" that mapped the various elements of the 8-dimensional proof.

Subsequently, Math, Inc., a startup developing the AI Gauss, accelerated the process. Gauss is a language model designed to automatically formalize proofs. After completing the Lean formalization of the prime number theorem, Gauss demonstrated several facts related to the sphere packing project.

Results and Implications

Gauss not only auto-formalized the 8-dimensional case, but also identified and corrected a typo in the published paper, all in just five days. Subsequently, it formalized the 24-dimensional proof in two weeks, without a pre-existing blueprint.

This result represents a watershed moment for auto-formalization and human-AI collaboration, paving the way for a revolutionary transformation in mathematics, where large-scale formalizations become commonplace. This allows mathematicians to focus on creating new mathematical theories.