E8 sphere-packing Lean 形式化报告发布：Gauss 在最后阶段完成约 4 万行 autoformalization

Hariharan、Birkbeck、Lee、Ma、Mehta、Poiroux 与 Viazovska 发布维数 8 sphere-packing proof 的 Lean 形式化进展报告。项目在 2026 年 2 月已达到 formally verified milestone；论文详细说明最后阶段由 Math, Inc. 的 autoformalization model Gauss 协助完成，并讨论人类与模型如何分工。公开材料报告整个 development 约 60,000 行 Lean，其中最后约 40,000 行在数天内由 Gauss 协助完成。