h1在5題共同測試中單次成功率達82.5%，納入第6題後為68.75%

AI定理證明系統 h1 在5道共同評測的埃爾德什（Erdős）問題中，單次執行成功率為82.5%，每項成功證明的平均API換算成本為121美元（約16萬韓元）。同一組題目中，AlphaProof Nexus的成功率為76%，每項成功證明平均成本為317美元；若納入第6題，h1的成功率則會降低。

Meta（META）的FAIR研究組織與紐約大學（NYU）研究人員等組成的團隊，於10月25日公開論文《h1：自動定理證明中的「苦澀教訓」一隅》（h1: A Taste of the Bitter Lesson in Automated Theorem Proving）。研究團隊比較h1與其他定理證明系統的表現和成本，並在多項基準測試中評估語言模型的證明能力。

h1與AlphaProof Nexus的比較，採用三套系統都至少解出一次的5道埃爾德什問題。研究人員讓h1和AlphaProof Nexus使用相同的Gemini 3.1 Pro模型，以比較系統配置帶來的差異。

在這5題中，h1的單次執行成功率為82.5%，高於AlphaProof Nexus的76%。只計算成功證明時，h1平均成本為121美元，AlphaProof Nexus則為317美元。

h1的運作方式，是由語言模型撰寫並修改Lean 4證明檔。驗證器回傳錯誤訊息與尚待證明的目標後，模型會參考這些資訊再次嘗試。

Lean 4是一種用來以特定格式表達數學命題與證明，並進行機器檢查的工具。因此，驗證結果顯示的是：輸入的形式化命題，其證明是否獲得接受。

研究團隊沒有要求系統預先把問題拆成多個步驟，也沒有規定要依固定順序調用專用證明器。模型可以持續維護工作檔案，並依據驗證回饋和自我檢查決定下一步。

在其他基準測試中，搭配GPT-5.5的h1解出PutnamBench 672題中的670題。不過，PutnamBench官方排行榜也列有解出全部672題的系統，因此不能把670題視為最高紀錄。

在採用GPT-5.6 Sol的實驗中，系統解出FATE-X 100題中的90題，以及FormalConjectures100-Solved 100題中的78題。這些基準測試的每道題目都只執行一次。

論文列出的美元成本，是將記錄到的Token用量套用價格表後換算出的API成本，並不代表實際支出。121美元和317美元只以成功證明計算，未納入未成功的任務。

若把失敗成本也計入h1的內部比較，單次長時間執行達到82.5%成功率時，平均成本為138美元（約18萬韓元）；採用三次執行方式達到相同成功率，則需202美元（約27萬韓元）。這組數據的計算方式與h1對比AlphaProof Nexus時不同。

未納入比較的埃爾德什125題，h1嘗試16次都因Lean執行逾時而未能完成。在這題上，AlphaProof Nexus表現較佳。

若計入全部6題，h1的單次執行成功率為68.75%，低於AlphaProof Nexus的71.67%。因此，不能把h1在5題測試中呈現的成功率與成本優勢，直接套用到所有定理證明任務。

研究團隊表示，他們在FormalConjectures中證明了8個原先標記為未解的命題。論文附錄說明，其中「Written on the Wall II」的兩道題目，是修改命題本身後才完成證明。

已合併至儲存庫的相關變更請求，將其中5題標記為已解，並附上Lean證明。論文提到的8題與該變更請求標記的5題，涵蓋範圍不同。

機器驗證是否接受一項證明，與輸入命題是否準確表達原本想處理的數學問題，是兩件不同的事。論文附錄也指出，形式化後的命題可能存在問題。

這篇論文探討的是數學定理證明實驗，並未評估區塊鏈或智慧合約的驗證能力。