Meta 與紐約大學的研究人員打造了一套極簡的人工智慧系統來證明數學定理，其表現追平甚至超越精心設計的 Lean 證明工作流程——而且成本更低。

這套名為 h1 的系統提出一個簡單的主張：在自動化定理證明中，只要模型能獲得良好的回饋，簡單可以戰勝複雜。

極簡的代理迴圈

這項研究來自 Meta 的 FAIR 研究團隊與紐約大學。在 2026 年 10 月 25 日發表、題為「h1: A Taste of the Bitter Lesson in Automated Theorem Proving」的論文中，研究人員將 h1 描述為一個極簡的代理迴圈，將前沿大型語言模型連接至 Lean 4，並即時向模型提供驗證器結果。

Lean 4 是一套開源證明輔助工具，數學論證在其中以程式碼形式撰寫，因此檢查每一步驟的是編譯器而非人類審閱者。這種設定讓驗證器擁有最終決定權：證明必須通過編譯才算成立。

大多數自動化證明系統會將語言模型包覆在複雜的框架中，使用預先定義的工作流程將問題拆分、分派子任務，並協調眾多環節。h1 框架跳過了這些機制，改而依賴幾個簡單的機制：

• 持續性檔案編輯，模型在保存步驟間狀態的證明檔案上工作
• 每次編輯後立即獲得編譯器回饋，錯誤能即時浮現
• 反思，運用語言模型自身推理問題所在的能力

論文指出，h1 的表現主要來自與 Lean 之間的高效介接，而非複雜的編排。

基準測試結果

研究報告指出，h1 在多個形式化定理證明基準上達到最先進的表現。在 PutnamBench——一個以 William Lowell Putnam 數學競賽（北美大學生的年度數學競賽）題目為基礎的基準測試——上，h1 使用 GPT-5.5 取得 672 分中的 670 分。在 FATE-X 評測中，h1 取得 100 分中的 90 分。

該系統也解決了 FormalConjectures 集合中的八個未解問題，其中包括以多產數學家 Paul Erdős 為名的 Erdős 問題的多個變體。由於這類問題以 Lean 的形式語言表述，解決它們意味著產出經機器驗證的證明，而非文字論證。

最直接的比較對象是 DeepMind 的 AlphaProof Nexus。在 Erdős 問題解答上，h1 錄得 82.5% 的成功率，AlphaProof Nexus 則為 76%。成本差距比準確度差距更大：h1 每個成功證明花費 121 美元，AlphaProof Nexus 則為 317 美元。

「苦澀的教訓」應用於數學

論文標題指向「苦澀的教訓」——這是 AI 研究者 Rich Sutton 在 2019 年一篇文章中提出的術語，意指由大量運算驅動的可擴展通用方法，隨時間推移往往勝過專門的手工技術。

這並非 Meta 首次嘗試這一課題。這項研究建立在 Meta 早期的工作之上，包括 2022 年推出的 HTPS 神經定理證明器，並反映了方法的轉變。早期系統專注於在模型周圍建立更聰明的搜尋機制，而 h1 則專注於讓模型直接與驗證器互動。

時機也很重要。h1 的結果依賴於 GPT-5.5 等前沿模型，而亮眼的 PutnamBench 成績正是以該模型達成。

這代表什麼

成本數據是這項研究最實用的部分。每個成功證明的成本從 317 美元降至 121 美元，改變了哪些問題值得嘗試。當每次嘗試的成本更低時，團隊就能對更困難或更具投機性的猜想進行更多嘗試。結果經機器驗證的特性也是其吸引力的一部分：形式化證明的進展吸引著數學領域之外的關注，因為證明輔助工具也被用於驗證軟體與硬體設計。

不過仍有一些注意事項。基準分數反映的是在特定測試集上的表現，而 PutnamBench 在 670/672 的成績下已接近飽和，因此系統在 FormalConjectures 等未解問題集合上的表現，將是接下來最值得關注的指標。h1 的方法也在很大程度上依賴其底層的前沿模型。

論文更廣泛的訊息是：強大的基礎模型搭配乾淨的驗證器回饋，可能比複雜的框架更重要——而這項押注在這些基準測試上得到了回報。

來源：CryptoBriefing