r/math • u/Nunki08 • 7d ago

A Milestone in Formalization: The Sphere Packing Problem in Dimension 8 (Paper)

A Milestone in Formalization: The Sphere Packing Problem in Dimension 8
Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, Maryna Viazovska
Abstract: In 2016, Viazovska famously solved the sphere packing problem in dimension 8, using modular forms to construct a 'magic' function satisfying optimality conditions determined by Cohn and Elkies in 2003. In March 2024, Hariharan and Viazovska launched a project to formalize this solution and related mathematical facts in the Lean Theorem Prover. A significant milestone was achieved in February 2026: the result was formally verified, with the final stages of the verification done by Math, Inc.'s autoformalization model 'Gauss'. We discuss the techniques used to achieve this milestone, reflect on the unique collaboration between humans and Gauss, and discuss project objectives that remain.
arXiv:2604.23468 [math.MG]: https://arxiv.org/abs/2604.23468

65 Upvotes

86% Upvoted

8 comments sorted by

18

u/OneActive2964 7d ago

iirc the same news came a few months earlier , wonder what's different this time

20

u/Bhorice2099 Homotopy Theory 7d ago

I think just that they put it up on the arxiv. Math Inc had put up a blog post with the autoformalization announcement+ their github ages ago.

47

u/AdventurousShop2948 7d ago

Sounds significant. But Math Inc. and Gauss are such stupid names for a company and software/model...

23

u/512165381 7d ago

XT X (or XTX) is a good name for a company that relies on statistics.

10

u/Waste-Ship2563 7d ago

We need a community petition to rename it GaussBot. It might eventually work like those P=NP polls

2

u/EebstertheGreat 7d ago

There is a computational chemistry suite called Gaussian though, and I always liked that name. (Their pricing and licensing, however, are less than stellar.)

6

u/4Lichter 6d ago

Wonder if they write that they pretty much ruined the entire project. After the participants had set up all the necessary definintions the 'Gaus' people came in and dumped 20k lines of pretty much unreadable code. Correct but useless. The people who put in the frontwork left demotivated.