IXThinker·2026-03-05 09:40

AI五天形式化菲爾茲獎級數學證明

AI 公司 Math 的 Gauss 模型僅用五天，完成對 2022 年菲爾茲獎得主 Viazovska 八維與二十四維球體堆積定理的形式化驗證，傳統需時約六個月，屬本世紀首次有菲爾茲獎成果被完全形式化。

成果內容

球體堆積定理研究高維空間中最密集的球體排列方式，是 Viazovska 獲菲爾茲獎的代表性工作。Gauss 用 Lean 語言將整個證明完全形式化，單一項目達 20 萬行代碼，是史上最大規模的單一目的 Lean 形式化項目。