Watershed Moment for AI–Human Collaboration in Math

The formal verification of Ukrainian mathematician Maryna Viazovska's Fields Medal-winning proofs concerning optimal sphere packing in 8 and 24 dimensions has been achieved through a human-AI collaboration, signaling rapid progress in AI's role in mathematical research.

Viazovska's original work, which solved the sphere-packing problem for 8 dimensions (using the E8 arrangement) and 24 dimensions (using the Leech lattice), was already verified by the mathematical community. However, formal verification—ensuring proofs can be checked by a computer using a proof assistant like Lean—is a separate challenge. This project, "Formalising Sphere Packing in Lean," began after undergraduate Sidharth Hariharan connected with Viazovska, aiming to formalize her proofs.

The collaboration accelerated significantly when the startup Math, Inc., using its AI reasoning agent named Gauss, contributed automated formalizations. Gauss first proved 30 intermediate facts ("sorrys") for the 8-dimensional case. Later, an improved version of Gauss autoformalized the entire 8-dimensional proof in five days, even finding and fixing a typo in the published paper. Subsequently, Gauss autoformalized the much more complex 24-dimensional proof, involving over 200,000 lines of code, in just two weeks, building upon the foundational theory established in the 8-dimensional case. Both human collaborators and the AI developers view this as a revolutionary step, suggesting that such technology will free mathematicians to focus on conceptual discovery.

(Source：ieeespectrum)