文章圖片
文章圖片
文章圖片
魚羊 發自 凹非寺
量子位 | 公眾號 QbitAI
5天時間 ， AI就搞定了原本需要6個月完成的菲爾茲獎級數學成果的形式化證明 。
這一最新成果一經公布 ， 立即在x上引發了討論熱潮 ， 甚至有數學家稱之為“自動形式化領域的ImageNet時刻” 。
AI是來自Math這家公司名為Gauss的AI 。 具體完成的工作 ， 是形式化驗證了讓Maryna Viazovska在2022年獲得數學最高獎——菲爾茲獎的成果：關于8維和24維最優球體堆積問題的定理 。
這是本世紀以來首次有菲爾茲獎成果被完全形式化 。
而單一項目20萬行Lean代碼 ， 也使得“硅基高斯”的這項最新工作 ， 成為歷史上最大規模的單一目的Lean形式化項目 。
還有一個引起大家關注的重點是 ， “硅基高斯”在推理驗證過程中 ， 還自主檢測并糾正了原論文中的錯誤 。
本世紀首次完成菲爾茲獎成果形式化2022年 ， Maryna Viazovska拿下菲爾茲獎的獲獎理由是：證明了E8晶格在8維空間中提供了最密堆積的相同球體 ， 以及對相對極值問題和傅里葉分析問題的進一步貢獻 。
其中提到的這個球體堆積問題 ， 就是這次“硅基高斯”所關注的 。
簡單來說 ， 就是要證明 ， 在n維空間中 ， 相同的球體最多能以多高的密度進行堆積 。
在一維情形下 ， 這個問題并不復雜 ， 二維情形也早有證明 。 但當n的數字來到3 ， 也就是在三維情形下 ， 盡管開普勒在1611年就提出了相關猜想 ， 但直到1998年 ， 數學家Thomas Hales才在計算機的輔助下完成了證明；而三維情形的形式化驗證 ， 則又耗費了十余年的時間 。
【AI Agent搞定世紀首次菲爾茲獎成果形式化！一周時間獨立完成】在更高維度上 ， 這個問題就更加復雜、難以攻克 。 直到Maryna Viazovska找出了該問題與模形式理論之間的聯系——
她利用一種創新的方法 ， 將傅里葉分析與模形式結合起來 ， 構造了一個優化的輔助函數來嚴格驗證E8晶格在8維空間中的最優性 。
基于同樣的方法 ， 她還和合作者們一起 ， 進一步證明Leech晶格提供了24維空間中最密的球體堆積 。
2024年 ， Maryna Viazovska開始和合作者們一起推動對這一成果的形式化項目 。
形式化是指將數學證明嚴格地表達為符合形式邏輯規則的形式語言 。 這種過程可以被計算機驗證 ， 以確保證明的每一步都完全符合邏輯規則 ， 主要目的是提高數學的嚴謹性、可靠性和透明性 。
2025年11月 ， “硅基高斯”開始參與到這個項目之中 。 在證明了若干關于模形式、徑向施瓦茨函數和基礎球體堆積理論的問題之后 ， 這個AI的目標變成了：自動完成該項目的全部剩余工作 。
于是事情的發展開始超乎人們的想象：
在前兩年 ， 人類專家團隊共編寫了約2萬行Lean代碼 。 而Gauss僅用5天的時間 ， 就新增約5萬行代碼 ， 在沒有借助額外輔助框架的情況下 ， 完成了該問題的8維情形驗證 。
團隊原本估計 ， 用現有工具 ， 要完成這一項目還需6個月時間 。
又花了一周時間 ， Gauss在研究了Viazovska原論文和20+篇額外參考文獻后 ， 生成45萬行代碼 ， 把24維情形的形式化證明也給搞定了 。
“硅基高斯”背后團隊強調 ， Gauss是“獨立推演了全部證明過程” 。
在完成證明的過程中 ， 它還發現并修正了原論文的細節錯誤：在Prop 7中 ， 函數b(t)的計算缺了一個負號 ， 另外還有某處定義存在缺陷 。
該研究團隊認為：
對菲爾茲獎級別數學成果的驗證表明 ， 以Gauss為代表的AI智能體 ， 已經具備加速數學前沿研究發展的能力 。
擴大自動形式化的規模 ， 將通過使全部已知數學成果變得可檢索 ， 徹底變革數學知識體系和數學發現方式 。
p.s. 為了讓這些形式化知識更加可維護 ， 研究人員們還利用Gauss自動重構、優化改進了代碼 ， 把代碼行數從峰值的50萬行 ， 壓縮到了約20萬行 。
代碼均已在GitHub上發布 。
關于GaussGauss背后公司Math Inc.的創始人 ， 是xAI聯合創始人、BatchNorm作者Christian Szegedy 。
他在2025年創辦Math ， 致力于用AI“解決數學 ， 解決一切” 。
此前 ， Gauss就因為用3周時間 ， 完成陶哲軒和Alex Kontorovich提出的數學挑戰——在Lean中形式化強素數定理（Prime Number Theorem ， PNT） ， 而一炮成名 。
而陶哲軒本人也和Math有所合作 ， 將解析數論中的顯式估計形式化 ， 把依賴大量計算的論證轉化為經過驗證、可復用的構建模塊 。
在當時 ， 外界對于Gauss這樣的AI Agent ， 還有許多質疑 ， 包括自動化的程度、對數學問題隱含目標的忽略……但現在 ， 正如Christian Szegedy自己所說：
（不到兩年前）數學家們還認為 ， 人工智能要達到能夠協助完成此類數學形式化工作（菲爾茲獎級數學成果形式化）的水平 ， 尚需多年 。
但“硅基高斯” ， 在今天已經帶來最新突破 。
參考鏈接：[1
https://x.com/mathematics_inc/status/2028542388717986135[2
https://www.math.inc/sphere-packing
— 完 —
量子位 QbitAI · 頭
關注我們 ， 第一時間獲知前沿科技動態條號
推薦閱讀
- 釘釘首創智能表格“透視表視圖”，AI表格Agent接入釘釘群
- 英偉達護城河被AI攻破，字節清華CUDA Agent，讓人人能搓CUDA內核
- \uD83E\uDD9E別在 OpenClaw 上花冤枉錢了，這份小白指南手把手教你 1 分鐘搞定
- 從經驗驅動到 AI 驅動：AI Agent 重構決策閉環｜友盟 + 深圳閉門會
- 上海語音Agent團隊融資近億，浙大校友創辦
- AI智能體不是越多越強：信息冗余構成了LLM Agent Scaling的瓶頸
- 訓練獎勵太稀疏？港中文聯合美團給Agent加上「過程分」
- AdaResoner實現Agentic Vision的主動「視覺工具思考」
- 技術門檻降為零，Manus反擊OpenClaw，推出傻瓜版Agents
- 超6萬GitHub項目實測：AI Agent寫代碼效率暴漲，通過率仍落后人類