656行代碼5小時搞定，Axiom AI自主完成兩項Erd?s猜想形式化證明

近日，AI 初創公司 Axiom 宣布其模型在沒有人類干預的情況下，自動完成了兩個數學猜想的證明——埃爾德什問題（Erd?s Problem）中的 481 號和 124 號。

據稱，481 號問題僅用時 5 小時，代碼量為 656 行；124 號問題則耗時超 24 小時。值得關注的是，這些證明均通過 Lean 驗證，Lean 的特點是其形式化證明過程無需人工干預，為數學正確性提供了保障。

（來源：X）

據悉，本次完成兩個數學猜想的證明的并不是 Axiom 推出的 API 或完整的產品，而是一個由多個模型組成的系統，包括 Axiom 的通過強化學習后訓練研發的模型。

該公司 CEO 洪樂潼（Carina Hong）對 DeepTech 表示：“六百多行代碼對于形式化的證明來說，算是比較簡潔和漂亮的證明?！?/p>

（來源：X）

該證明在社交媒體發布后，有用戶評價稱“埃爾德什問題的精簡形式化令人耳目一新”，也有用戶評價本次證明是一個“好的起點”，還有用戶這樣評價：“幾周前 OpenAI 曾稱聲稱用 GPT-5 解決了埃爾德什問題，但社區指出它只檢索了現有文獻。而 Axiom 實際上證明了這個問題。”

圖丨X 上用戶評論（來源：X）

埃爾德什問題是匈牙利數學家保羅·埃爾德什（Paul Erd?s）提出的一系列懸而未決的數學猜想，長期被視為檢驗推理能力的試金石。

圖丨埃爾德什問題 481 號（來源：Erd?s Problem）

481 號問題是一個社區近 45 年未被解決的問題，即某種迭代算術過程是否必然在某一步產生重復，從而進入循環或重復狀態。

圖丨Axiom 模型證明的 481 號問題（來源：洪樂潼）

而 124 號問題是：考慮若干整數基數 (d_1 < d_2 < \cdots < d_r)（且每個 (d_i \ge 3)），構造由這些基數的不同比例冪構成的序列。這是一個近 30 年未被解決的問題，也是最近比較火熱的話題之一。

幾天前，我們對 Harmonic 公司開發的 Aristotle 模型自主解決埃爾德什問題 124 號進行了報道，該公司由 Robinhood 的 CEO 弗拉德·特涅夫（Vlad Tenev）創立。

圖丨埃爾德什問題 124 號（來源：Erd?s Problem）

“關于 124 號問題，我們跑了超過一天的時間，中途一定是走到某個‘死胡同’里了。盡管目前跑出來的證明比較長，不如我們期望的簡練，但至少它跑出來了。”洪樂潼說。

圖丨Axiom 模型證明的 124 號問題（來源：洪樂潼）

Axiom 是一家成立不到 4 個月的公司，據公開資料其目前已融資 6,400 萬美元的種子輪融資，成員不到 20 人。該公司 CEO 洪樂潼是 00 后，她在美國麻省理工學院獲得數學和物理雙學士學位，并在英國牛津大學獲得神經科學碩士學位。此前，她曾在美國斯坦福大學攻讀數學和法學博士學位，后輟學。

Axiom 官網稱，其創新性體現在通過融合 AI、編程語言和數學，開發能夠解決復雜數學問題的人工智能系統，其初始模型是 AI 數學家。一方面，其可啟發人類數學家的科研靈感，另一方面可成為人類數學家的合作者，而非替代者。最新公開消息顯示，著名數學家小野健（Ken Ono）剛從美國弗吉尼亞大學離職加入 Axiom 擔任創始數學家，他曾在 2020 年擔任洪樂潼研究項目的導師。

該公司官網提到，我們現在處于一個“數學發現”的時代。其在博客中曾提到過一個想法：人類在自然語言中進行推理，而該公司的模型在進行形式化推理時，會把自然語言的推理過程轉化為形式化代碼。在這個過程中，形式化代碼的運行結果會反饋回來，進而影響人類在自然語言推理上的直覺和思考方式。

實際上，這個過程可以拓展到更廣泛的應用領域，比如金融、量化交易、芯片、硬件和軟件的形式驗證、物理定律的形式化推導等。

自動形式化是近年來被關注新的方向，其把自然語言的證明轉換到 Lean 語言中，這個過程與證明和形式化證明同樣重要，且在一個系統中同時訓練，而不是分開訓練。

洪樂潼對 DeepTech 解釋道：“我們對數據主要依賴自動生成，無論是從自然語言到形式化的自動轉換，還是在形式化的基礎上自動生成 100 到 1,000 倍的變體，甚至可以借鑒類似編譯器中的想法和手段。”

據了解，Axiom 目前正在設計內部的基準數據集，旨在用更難的數據集來挑戰其模型能否進一步突破極限。此外，他們還希望讓猜想和證明可以做持續的非對稱自我博弈以及事后重演。

洪樂潼認為，AI for Maths 是 AI for Science 的理論層和算法層，她表示：“大家可能覺得解決了埃爾德什問題很了不起，但我認為這只能說明模型具備了一定的能力，但我們也必須清醒地看到，它距離成為真正的 AI 數學家還有一定的距離，比如在數論、代數幾何、代數拓撲、微分拓撲等方向上我們還有很大的進步空間?！?/p>

從融資規模與公司體量來看，Axiom 當前進展已引發行業關注。后續能否進一步與競爭對手拉開差距并形成落地產品，還需多一些的耐心與觀察。

參考資料：

https://x.com/carinalhong/status/1995905801719066763?s=46

https://b.capital/why-we-invested/toward-mathematical-superintelligence-why-we-invested-in-axiom/

https://axiommath.ai/

https://www.erdosproblems.com/

https://techfundingnews.com/axiom-math-ai-mathematician-64m-seed/

https://www.wsj.com/tech/ai/math-ken-ono-carina-hong-axiom-startup-649bc417

運營/排版：何晨龍