Maryna Viazovska’s proofs of sphere packing formalized with AI

Maryna Viazovska. Credit: EPFL 2026.

The proofs that earned EPFL professor Maryna Viazovska the Fields Medal in 2022 have reached a new milestone: their complete formalization by computer, achieved through a collaboration between mathematicians and artificial intelligence tools.

In 2016, Maryna Viazovska solved the sphere packing problem in dimension 8, proving that the E₈ lattice constitutes the densest possible arrangement. Shortly after, together with collaborators, she established an analogous result in dimension 24 using the Leech lattice. Her method provided an elegant solution to a problem studied for centuries, with close ties to applied fields such as error-correcting codes.

For this major contribution, Viazovska was awarded the Fields Medal in 2022, the highest distinction in mathematics. Her proof was swiftly accepted by the scientific community, but formally verifying it by computer represents a challenge of a different kind: it requires translating every step of the reasoning into a logical language that software can check automatically.

The project Formalising Sphere Packing in Lean, launched in 2024 following a meeting in Lausanne between Viazovska and young mathematician Sidharth Hariharan, took on this task. Working with several international researchers, the team constructed a detailed blueprint of the dimension-8 proof and progressively translated it into Lean, a proof assistant widely used in mathematics. A specialized AI, Gauss, developed by startup Math, Inc., then played a decisive role in the formalization. By helping to complete certain intermediate steps, it accelerated the process and enabled the dimension-8 case to be wrapped up in five days, followed by the considerably larger dimension-24 case — over 200,000 lines of code — in two weeks.

This international project illustrates the rapid progress of formal verification and could mark a turning point in the collaboration between mathematicians and AI systems for verifying and constructing complex mathematical proofs.

Find out more

Watershed Moment for AI–Human Collaboration in Math – Twenty-first-century Fields Medal proof formalized for the first time, IEEE Spectrum.

EPFL

EPFL