형식화의 이정표: 8차원에서 구 채움 문제

A Milestone in Formalization: The Sphere Packing Problem in Dimension 8

2016년, 비아조프스카는 8차원 구 채움 문제를 해결했는데, 이는 2003년에 콘과 엘키즈가 결정한 최적성 조건을 만족하는 '마법' 함수를 모듈러 형태로 구성하는 방식으로 이루어졌다. 2024년 3월, 하리하라와 비아조프스카는 이 해결책과 관련된 수학적 사실들을 Lean Theorem Prover를 사용하여 형식화하는 프로젝트를 시작했다. 2026년 2월, 중요한 이정표가 달성되었는데, 바로 결과가 공식적으로 검증된 것이다. 검증의 최종 단계는 Math, Inc.의 자동 형식화 모델 'Gauss'에 의해 수행되었다. 본 논문에서는 이 이정표를 달성하기 위해 사용된 기술들을 논하고, 인간과 Gauss 간의 독특한 협업에 대해 성찰하며, 남아 있는 프로젝트 목표에 대해 논의한다.

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.