FrontierMath Erdős Benchmark

資料來源#

• After Math
• Announcing FrontierMath Erdős
• FLT: Anthropic has beaten me to it
• FrontierMath Erdős
• Long-horizon autoformalization of a core theorem underlying MIP* = RE
• OEIS Open: How many conjectures can language models turn into theorems?
• On the Navier–Stokes Millennium Prize Problem
• ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization
• SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization

摘要#

FrontierMath Erdős 是 Epoch AI 建立的基準測試，涵蓋 截至 2026 年 8 月仍未解的 68 個 Erdős 問題，並以 Lean 形式化；AI 系統必須在固定預算內證明或推翻命題（Tom Adamczewski 與 Greg Burnham，2026-09-01 公告，empirical）。這是該語料中首個題目完全沒有已知答案的基準測試，也是首個把美元預算納入得分定義、而非只在揭露資訊的註腳中提及的基準測試。

這項工作的出發點是，Erdős 問題已成為「追蹤 AI 數學能力的核心基準之一，但這種地位相當非正式」——DeepMind 使用過（9/353），OpenAI 對單位距離問題的反證也使用過，卻沒有共用題目集合、共用預算或共用驗證標準。Epoch 在既有做法上加入三項規範：篩選（哪些問題既難又重要）、驗證（以 Lean 機器檢查解答），以及可重現性（公開測試框架、題目清單和每題預算）。

三項改進，以及它們實際帶來的價值#

篩選：把重要性作為選題標準#

「Erdős 問題」泛指 Paul Erdős 曾提出的問題，而他提出過數百個問題。Thomas Bloom 維護的 erdosproblems.com 收錄了 1,217 個問題，其中 652 個仍未解；Epoch 請 Bloom 從未解問題中選出他最看重的題目，也就是他認為既有數學意義又具挑戰性的問題。他選出 68 題，約占未解題目的 10%，截至 2026 年 8 月全都仍未解。

Epoch 自己也指出了明顯的弱點：「這種做法高度主觀」，並引用 Bloom 對姊妹基準的標準：「毫無疑問，每位數學家都會看到清單中的某些題目，心想『他們到底為什麼會選這題？』——但只要他們也看到其他題目，認為『這題理所當然該入選，這是個深刻而重要的問題』，我想我們就做得不錯。」讓門檻更具體的參照是：Bloom 粗略估計，截至 2026 年 8 月，AI 總共解出過 3 至 5 個這種水準的 Erdős 問題。因此，分母刻意選在歷來成果所及的邊緣，而不是目前可測量能力的邊緣。

驗證：「Lean 形式化」在此確切保證什麼#

解題必須提交通過驗證的 Lean 證明或反證，並由 Comparator 檢查。Comparator 是 Lean FRO 建立的證明檢查器，「設計上能抵抗刻意作弊的提交」。這是強而有力的一面。但 Epoch 也明確列出三項限定，每一項都很重要：

1. 可靠性取決於 Lean 本身。 公告唯一的註腳指出，保證成立的前提是「Lean 本身沒有錯誤——但它肯定有錯。實務上，我們預期誤判極為罕見，而且發生時不難辨認。」這是標準保留條件，公告明確說出，而非默認不提。
2. 可靠性也取決於形式化命題是否正確——這正是 AI-Driven Formal Proof Search 所指出、仍須由人類負責的部分。Epoch 的形式化來源不一：68 題中有 50 題已由 Google 的 Formal Conjectures 專案形式化；其餘 18 題由 AI 在 Epoch 指導下形式化。
3. 這 18 題尚未經專家審查。 Epoch 原話是，這 18 個命題「相當簡單，形式化版本目前已通過我們的初步審查。不過，我們不是 Lean 專家，因此可能仍有錯誤。我們正在尋求更多專家審查。」因此，對 26% 的題目而言，目前的保證僅表示有非專家審查過 AI 對未解問題所作的形式化。公告沒有說明已解題目是否有任何一題來自這個子集，因此這仍是待解問題，而不是單純的保留條件。

可重現性：$300／72 小時規則#

整個程式碼庫連同測試框架與 68 道題目清單均以開放原始碼形式公開。預設規則是：每題嘗試一次，每次嘗試有 $300 推論預算和 72 小時工作時間。 模型不連網執行——它們可使用離線數學論文集與電腦代數系統等工具。

這項做法的影響範圍遠超數學。Epoch 明確要處理實驗室內部結果的不透明性，例如「有多少人嘗試過……哪些問題……使用什麼支架……花了多少推論運算」；它的解法是把預算變成得分本身的屬性，而不只是披露資訊。參見 Compute-Controlled Benchmarking，了解為何這是更有力的做法；Expenditure Horizon 則是 2026 年另一項嘗試，將能力放到美元尺度上衡量。

結果：68 題解出 2 題，另外 3 題花了多少成本#

五個模型，每題各嘗試一次：

模型	得分
GPT-6 Astra（預發布）	3%
GPT-5.6 Sol	0%
GPT-5.5	0%
Claude Fable 5.1	0%
Claude Fable 5	0%

（兩個 Anthropic 項目分別是 Fable 5 與其小版本。）只有預發布的 GPT-6 Astra 解出題目：68 題中 2 題。它藉由找到反例推翻了問題 74，成本 $222、耗時 10 小時 (2026-09-29 經 FrontierMath Erdős 更新取代：$218、耗時 15 小時)；並在 $172、耗時 10 小時 (更新取代：$247、耗時 16 小時) 證明了問題 126。論文依據實際 token 價格重新計算 Astra 每次嘗試的成本（見下方「方法論論文補充了什麼」），可能因此造成數字變動；原公告刊出的數字沒有說明採用哪種價格計算方式。所有模型的其他嘗試都「在得到經驗證的證明前用盡預算」。

標題呈現的是兩個事件，應該直說。 在相同的 68 題上，2/68 對 0/68 相差兩次成功；以 2×2 列聯表計算，雙尾 Fisher 精確檢定的 p 值約為 0.50。因此，Astra 排名高於其他四個模型的排序，依據的是這個規則在每題只嘗試一次、n = 68 的情況下無法判定的差異——下方超出規則的重複測試才讓 Astra 的能力更可信，而且沒有其他模型做過超出規則的測試。Epoch 沒有提出這一點；但數據支持這樣的解讀。

成本階梯：$300 → >$220,000#

除了基準測試外，Epoch 也以同一款預發布 Astra，針對相同問題進行了較不系統化的嘗試，使用更高預算、不同的代理設定和不同的嘗試次數。Epoch 特別強調這些嘗試：「這些嘗試不計入 FrontierMath Erdős 得分。」 Astra 的得分仍為 3%。

在所有嘗試中，Astra 至少解出過 68 題中的 5 題——上面兩題，加上問題 1（反證）、548（證明）和 571（證明）：

問題	結果	解出次數	各次解答成本
1	反證	5 次中 2 次 4 次中 2 次	$405（27 小時）和 $1,384（84 小時）
74	反證	7 次中 7 次 6 次中 6 次	$47（5 小時）至 $271（19 小時）
126	證明	5 次中 5 次 4 次中 4 次	$154（8 小時）至 $249（17 小時）
548	證明	4 次中 1 次 3 次中 1 次	$363（20 小時）
571	證明	4 次中 1 次 3 次中 1 次	$617（41 小時）

其餘問題每題嘗試 兩到六次，共 269 次 (2026-09-29 經 FrontierMath Erdős 更新取代：63 題中有 56 題完成了兩到五次嘗試，合計 172 次；其餘七題不列入計算，未能得出判定便因基礎設施故障中止的嘗試也不計)——沒有解出任何一題。上表採用論文的次數，排除沒有判定結果的嘗試。解出五題的總花費：超過 $220,000；相比之下，基準測試本身約花費 $20,000（68 × 約 $294，也就是幾乎每次計分嘗試都花光 $300）。

公告留下了三種值得進一步解讀的方式：

• 在同一個模型內，邊際解題成本上升了兩個半數量級。 規則內解出的兩題成本為 $222 和 $172 $218 和 $247（論文數字）。另外三題合計多花約 $200,000——每多解一題約 $67,000——因為大部分花費都用在沒有解出任何問題的徒勞嘗試上（公告記為 269 次，論文則為 172 次）。
• 兩種限制都會影響結果，而且各自限制不同。 三題規則外解答的成本都超過 $300 上限（$363、$405/$1,384、$617），而且每次嘗試的成功率都偏低（論文數字為 2/5、1/4、1/4 2/4、1/3、1/3）。基準測試找到的兩題則成本低且可靠（74：7/7 6/6；126：5/5 4/4）。因此，固定規則不只是篩掉超出預算的解答——它也挑出單次抽樣下可靠可解的問題，而每題成功率呈雙峰分布。
• 在一定範圍內，增加嘗試次數比增加預算便宜。 問題 74 有些嘗試花 $47 就解出，另一些則花 $271：同一問題、同一模型的單次解答成本相差 5.8 倍；每題只嘗試一次，這種差異就被轉成二元結果。

Epoch 自己也點出尚缺的實驗：「未來工作可以更有系統地測試這種推論擴展，衡量每次嘗試預算和嘗試次數增加時，解答數量如何成長。」

形式化成本，量化呈現#

Epoch 提出的第一項保留條件，對 AI-Driven Formal Proof Search 影響最大：「將這類結果形式化，基本上等於另外進行一個完全獨立的專案，再把它接上來。」它舉出的例子，是該語料中最鮮明的數字；本維基也已用另一種描述追蹤這項結果——Erdős 問題 90 就是單位距離猜想，也是 OpenAI 模型推翻的命題（見 Latent Capability Overhang）：

自然語言證明有 18 頁；後續將結果形式化為 Lean 的工作則包含 120 萬行程式碼——「主要是因為必須引用一項『深層』結果，而該結果尚未在 Lean 標準函式庫中形式化。18 頁的論文可以直接引用該結果，Lean 形式化則需要從第一原理推導它。」

這約等於每頁文字要 67,000 行 Lean；明確指出的原因是 mathlib 覆蓋度，不是證明難度——AI-Driven Formal Proof Search 從 AutoGraphForge 記錄的同一個詞彙瓶頸，在這裡以實際完成形式化的結果呈現其成本。請留意，這 120 萬行並非模型輸出，而是由人主導的獨立工作（github.com/plby/Erdos90）；因此這量到的是形式化成本，不是 AI 支付這項成本的能力。Epoch 將其概括為：「這是所有要求 AI 系統解決未解問題的 Lean 基準測試都會遇到的限制」——反過來看，這也是該語料支持未形式化分支最有力的論據。

一週後，有供應商聲稱只花 17 小時就付清這筆成本。 [[navier-stokes-ai-claim|OpenAI 對 Navier–Stokes 的公告]]（On the Navier–Stokes Millennium Prize Problem，2026-09-08，vendor-claim）表示：「Lean 形式化與驗證透過 GPT‑6 Astra 額外花了 17 小時」——也就是說，在本頁規則下得分 2/68 的模型，不到一天就形式化了一個千禧年大獎級別的爆破解答。對照上段，可能有三種情況：不同結果的形式化成本差異極大；AI 現在能負擔一項過去需要人類主導、耗費 120 萬行的成本；或兩項產物並非同類（完整推導與證明骨架、不同的命題，或「驗證」的界定範圍不同）。公告沒有提供任何能區分這些情況的資訊——沒有行數、命題內容、公理規範、函式庫版本，而且它連結的儲存庫也不在此語料中。此處記錄這項說法，是因為本頁收錄了唯一經測量的數字；而「形式化成本便宜 1000 倍」的 vendor-claim，正是這個數字應該用來檢驗的主張。

這對本頁標題下的結果，還有一項更直接的影響。 本頁唯一非零得分屬於預發布的 GPT-6 Astra。同一份公告指出，Navier–Stokes 結果來自「能力明顯高於 GPT-6 Astra 的內部模型」，該模型於 8 月 28 日開始訓練——也就是本基準發布前一週。照供應商自己的說法，本頁測量的模型在 2/68 公布時，內部就已被更新的模型取代。因此，基準測試的 3% 描述的是外部評估者可取得的最強模型，而不是前沿能力。這不會削弱本頁所貢獻的測試規則，而是界定數字的意義；這也是潛在能力落差首次出現在計分基準測試中。

本節量化的 Mathlib 覆蓋不足，在 ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization（empirical）中有相應的實測：為了形式化隨機最佳化收斂證明，代理建立了 109,634 行的領域函式庫；在四項任務中移除該函式庫後，人類評分維持不變（平均 6.8），token 數則增加 7.7% 至 154%（Many-Agent Proof Harnesses）。重複使用能降低重建成本；但在那些任務上，它沒有改變最後達成的成果。

反對把這種結果列入評分的理由（2026-09-12）#

Navier–Stokes 公告發布三天後，De Toffoli 與 Duede 在 Terence Tao 的部落格發表了評論（After Math，practitioner-opinion），主張這類基準測試衡量的不是該衡量的事；值得在這個基準測試的頁面上記錄：

「如果數學上的成功逐漸與產出經認證的答案過度緊密地畫上等號，數學就可能調整自身，以迎合那些最容易被基準測試、並自動化取代的特徵。」

他們認為，經認證的答案還稱不上解答——解答還需要清晰易懂的論證，讓結果能進入實際數學研究（見 Logical vs Intelligible Proof）；而數學的目標也不只有解題，還包括建立理論、訓練、社群、累積知識和美學價值。他們指出，這不只是哲學上的憂慮，也是制度層面的問題：mathandai.org 上的一份聲明最初由 25 位菲爾茲獎得主連署，警告 AI 公司的目標與數學社群之間存在「嚴重錯位」。

這些論點有多少適用於此處。 古德哈特定律的風險確實存在，但尚未量化；它針對的是數學領域的規範，而非測試規則。本頁自己的貢獻——固定預算、經篩選的分母、核心檢查器的判定——就它宣稱衡量的內容而言，比該語料中的其他做法都更適切。有兩點削弱了這項反對意見對本基準測試的適用性：Epoch 的題目由人類專家按重要性篩選，且根據背景估算，這種水準的題目歷來只有 3 至 5 題曾由 AI 解出；這正好與挑選易於評分的題目相反。再者，2/68 說明的是題目難度，而非宣稱解出其餘 66 題就代表解決了數學。仍值得留意的是如何解讀：本頁數字上升，只代表經篩選的未解問題中，通過認證的答案增加；它沒有說明數學家是否能運用這些答案。這是由沒有提出測量、也沒有自身利益的作者所提出的論點；若涉及事實問題，權重應低於本頁其他所有內容。

依題目特性防止污染，但有明確期限#

Epoch 會將此基準當作「經典」公開測試——模型按發布時狀態評估，不設強力防護。它用來說明目前為何安全的論點相當特殊，也值得推廣：截至 2026 年 8 月，68 個問題都沒有已知解答，所以訓練資料截止時間早於該日期的模型不可能學到解答。這種污染免疫力來自題目本身尚未解出，而不是保留測試集、雜湊或沙箱（Benchmark Contamination and Decontamination）。

這種保護有明確期限，而且 Epoch 也承認：解答將會公開並受到討論，最後進入訓練資料。公告提出兩種強度不一的緩解方式：

• 事後篩除——「模型訓練截止日期前已解出的問題可以篩掉，所有模型都在剩餘題目上比較。」這確實可行，但基準測試每成功一次，分母就會縮小。
• 負面結果仍有參考價值——「如果後來的模型無法解出較早模型已解出的問題，那大概表示後來模型的數學能力較弱。」在目前這種得分下，這個說法不如聽起來那麼有力：計分測試只解出兩題，能提供參考的負面結果也只有一兩個事件。

第三項簡短的保留條件關於適用範圍：「Erdős 問題並不涵蓋全部數學。」Epoch 預期此處的進展與整體數學能力「至少有一定相關」，但也說明這種推論「並不嚴謹」。

方法論論文補充了什麼（2026-09-29）#

Adamczewski 與 Bloom 的論文（FrontierMath Erdős，arXiv 2609.25050，2026-09-06，12 頁，empirical；Bloom 是策展者，因此題目選擇由親自選題的人說明）是公告所指的配套論文。它沒有改變總結（Astra 3%，四個模型 0%），而是補上測試規則、來源脈絡，並重新計算成本。

重新計算成本是主要修正。 Astra 尚未發布，價格也未公開，因此測試框架用 GPT-5.6 Sol 的每 token 價格代替計費。Astra 真實價格約高一倍（視 token 組成而定，約 1.8 至 2.0 倍）：計量成本達到 $300 上限的嘗試，實際花費為 $545 至 $572。作者依 token 數重新計算每次嘗試，並且只將實際價格不超過 $300 的解答計入得分。由此造成一項影響：問題 1 在計分測試中以 $405 被推翻，因此不計入得分（它只列在額外嘗試中）——讓得分維持在 2/68 而非 3/68 的，是固定預算的修正，不是模型本身。一項承認的缺失是：代理的預算工具顯示計量美元，因此真正花到 $300 時，畫面顯示只花了約 $160、還剩 $140；模型因此按比實際寬鬆的預算安排進度。作者認為這比丟棄整次測試好。還有一個未釐清的數字：論文仍稱基準測試花費「約 $20,000」，這符合 68 × 名目 $300 的計算；但按本頁計算，66 次未成功嘗試若各花 $545 至 $572，Astra 實際支出應為約 $36,000 至 $38,000。應把 $20,000 視為名目預算，而非實際支出。

作者所估算的每題解答預期成本：約 $10,000（每次嘗試 $300、成功率 3%），他們稱這是「解出重要未解問題的合理成本」。對照上面的成本階梯，這是在測試規則下的成本；另外三題的邊際成本仍約為每題 $67,000。

逐題檢視題目來源。 68 個猜想涵蓋 65 個不同問題：Hadwiger-Nelson（#508）有三個猜想（平面的色數恰為 5、6 或 7——Formal Conjectures 的「數值是多少」命題不符合證明或反證格式），而 #713 的兩部分分別計算。這三個 HN 猜想按設計互斥（證明其中一個會推翻另外兩個；推翻其中一個則無法解決其他猜想），所以題目集合並非完全獨立：一項結果就能附帶解決另外兩題。其他多部分問題（#208、#812、#1206）只納入指定部分；對於表述不明確的問題（#138、#208、#812），Bloom 選出最能體現其「精神」的一個問題，通常也是最難的部分。**68 個猜想中有 50 個（涵蓋 48 個問題）來自 Formal Conjectures；另外 17 個問題沒有現成命題，因此經自動形式化，產生 18 個猜想；Bloom 逐一檢查每個自動形式化命題是否忠實呈現原問題。**這更精確地界定公告中「不是 Lean 專家」的保留條件：審查者是問題策展者兼數學家，而非 Lean 專家；論文也沒說明五個已解問題中哪些屬於自動形式化子集。論文另透露：7 個問題與 Sidon 集有關（這是 Bloom 個人最喜歡的主題），所以一個 Sidon 集相關的洞見理論上可能解決全部七題；有些問題（#172、#431、#500、#508、#952、#970）原本並非 Erdős 提出；選題標準是若由人類解出，足以在高水準期刊發表，沒有設定目標題數或難度上限。Bloom 提到，他過去曾批評 erdosproblems.com 不適合作為基準測試，因為難度差異極大，而且許多由 AI 解出的問題都很冷門；他認為例外的是 #90（單位距離）、#146 和 #183，這些著名問題累積了長期的部分成果。

Comparator 的實際運作方式。 每次嘗試會分在兩個 Docker 容器執行，兩者都無網路連線：代理容器（有完整 shell）與 Comparator 容器（採用乾淨的 Lean 工具鏈）。只有提交的 Lean 原始碼能離開代理容器。Comparator 在 Landlock OS 沙箱中編譯提交內容，並在沙箱外計算判定結果；只有當命題敘述與其依賴的每個宣告都和可信副本一致、只使用三個標準公理（sorry 會透過 sorryAx 被拒；native_decide 會透過 Lean.ofReduceBool 被拒），且整份提交從頭透過核心重新執行時，才會接受。這可防止 debug.skipKernelTC、插入宣告的中介程式，以及產生型別錯誤項目的有缺陷 tactic。仍須信任的是 Lean 核心、Comparator 與其沙箱。論文列出六種攻擊類別；參見 Kernel-Level Proof Auditing，了解這與 SafeVerify 和 #print axioms 的關係。

代理系統。 Inspect 的 deepagent（bash、文字編輯器、時間／token 預算工具，以及子代理委派、持續記憶和待辦清單）；Lean 4 + Mathlib 工具鏈，加上 SageMath 和 Python（sympy、mpmath、numpy、pantograph）；以及一份截至 2022 年的 476,000 篇純數學 arXiv 論文離線快照（proof-pile 的 arXiv 子集）。限制：$300 和 72 小時。在 OEIS Open Benchmark 上，deepagent 和論文快照對準確率的影響都不及簡易 ReAct 代理；仍保留它們，是「因為未來模型可能更善於運用這些資源」。

論文明列的其他限制。 FME 得分可能「大幅低估」數學能力（形式化成本、缺少 Mathlib 前置條件）；若猜想能推出 Collatz 這類著名未解問題，不給分；猜想可能獨立於公理，因此任務無解；已解猜想將外洩至訓練資料，而目前的免疫依據是截至 2026 年 8 月尚無已知證明。

五個解答簡述（附錄 B；論文提醒，這些證明尚未經數學專家「消化」，erdosproblems.com 上的非正式解說也只是佔位內容）：

• #1（不交集集合，最早可追溯到 1931 年）： 推翻 N >> 2^n；對任何 epsilon，都存在任意大的 n，使得 {1..N} 中有一個不交集集合，且 N <= epsilon * 2^n。此結果沒有給出有效界限（無法用 epsilon 表示 n 的上界），證明方法是對行列式趨近於 0 的有理數 n × n 矩陣使用線性代數；Bloom 以格點重新推導此結果。先前最佳結果為 0.22002 * 2^n（Bohman）。兩個反證基本上相同。
• #74： 存在 f(n) -> infinity，使得任何一個圖若其所有 n 頂點子圖都能藉由刪除至多 f(n) 條邊變成二分圖，則其色數至多為 3；證明初等且採歸納法，當 f(n) ~ log n / log log n 時似乎可行（Lean 命題只要求存在此函數）。六次反證，三種不同論證。
• #126： |S(A)| >> n^(1/2)，遠強於題目要求的 |S(A)|/log n -> infinity；四次嘗試中有三個不同的初等證明，指數分別為 1/8、1/3 和 1/2。
• #548（Erdos-Sos 樹猜想，1962）： 完整證明，「出奇地簡短優雅」，方法是對頂點排列方式進行雙重計數。
• #571： 每個 [1,2) 區間內的有理數 alpha 都是某個二分圖的極值數指數；Bloom 認為這五題中最難，且它與大量既有文獻的關係尚未評估。

論文也提醒，不要輕易把「已解」解讀為研究已完成：AI 證明雖通過機器驗證，卻尚未閱讀；「這些結果對數學的影響，取決於人類專家是否理解解答。」

本文其他比較的相關工作修正。 DeepMind 已解決的 9 個命題（Formal Conjectures 中形式化的 353 個 Erdős 命題）涵蓋 七個問題，其中四題明確解決（#152、#846、#125、#26）；#741 在 erdosproblems.com 上標為已解，但只適用於某種「密度」解釋；#12 只解決了三部分中的兩部分，#138 則只透過變體解決，兩者都仍未解。因此，「9/353」計算的是包含變體和子部分在內的命題數，不是 9 個問題。論文也將此基準與 HorizonMath（101 題）、FM:OP（50 題，估計 10–40% 無解，2026 年 7 月因驗證器忠實度移除兩題）、OEIS Open、LeanEval（Lean FRO 的排行榜，同樣由 Comparator 評分）以及 First Proof（由 30 位審查者評閱自然語言證明；第二輪中，四個 AI 系統在 10 題裡有 7 題至少獲得一項及格評分）相互比較；對這些比較的疑慮已記錄於 OEIS Open Benchmark。

與 DeepMind 的 9/353 數字對照#

維基已記錄一項 Erdős 解題數：由 AlphaProof Nexus 在 Formal Conjectures 儲存庫中嘗試的 353 題裡解出 9 題，每題成本「數百美元」。這個數字並未被取代：它使用不同題目集合、不同規則，也回答不同問題；兩個數字都仍有效。

	DeepMind（2026-05）	FrontierMath Erdős（2026-09）
題目集合	從 Formal Conjectures 嘗試 353 題，未按重要性篩選	Bloom 手動挑選 68 題，兼具重要性與難度
比率	9/353 = 2.5%	2/68 = 2.9%
預算	每題「數百美元」，不含在 353 題中尋找可解題目的成本	$300 和 72 小時，每題一次嘗試，所有題目都嘗試
驗證器	SafeVerify（編譯，不含 sorryAx）	Comparator（Lean FRO，抗作弊）
報告方式	列出已解題目	提供含分母的得分

兩個比率看起來相似，實際上並不相同。 有兩股相反力量。一方面，Epoch 的分母刻意選得更難——Bloom 的重要性篩選，對照的是 Epoch 描述為包含許多「從未受到太多關注……最後只花不多力氣就輕易解決」的問題集合。另一方面，Epoch 的規則在成本上也更嚴格：DeepMind 的每題成本沒有計入尋找可解題目的成本，而固定要求每題只嘗試一次，正好迫使人們支付這項成本——此處便可看出，68 題總花費約 $20,000，最後只解出兩題。較恰當的總結是，兩個數字在量級上相符（個位數百分比），但衡量的是難度與搜尋成本的不同組合；FrontierMath Erdős 則是兩者之中，第一個能直接與後續模型比較、而不必重新釐清哪些題目曾被嘗試的數字。

同一位評估者的另一個數字：492 個未解猜想中解出 30%（OEIS Open，2026-08）#

這份公告發布六週前，同一篇論文的第一作者發表了 OEIS OPEN（OEIS Open: How many conjectures can language models turn into theorems?，arXiv 2608.11941， 2026-08-12，empirical）：492 個已用 Lean 形式化的 OEIS 未解猜想，每個猜想預算 $50，每個模型都嘗試全部題目——Claude Opus 4.8 解出 492 題中的 147 題，得分 30%。 與本頁相比，解題率高十倍、預算只有六分之一；兩者出自同一機構、同一作者，採用相同的核心下證明或反證標準。

兩項結果並不衝突；一起看就能凸顯篩選的影響。 其他條件大致相同——Lean 形式化、證明或反證、得分定義納入固定美元上限、開放測試框架、2026 年前沿模型。差別在於如何挑選題目：

	FrontierMath Erdős	OEIS Open
題目	68 題，由 Bloom 手動挑選，兼具重要性與難度	492 題，根據 Gemini 提示挑選「非平凡、具數學趣味、不是著名未解問題」的題目
預算	$300／72 小時，每題一次嘗試	$50／72 小時，每題一次嘗試（100 題 LITE 子集中每題 $200）
最高得分	2/68 = 3%（預發布 GPT-6 Astra）	147/492 = 30%（Claude Opus 4.8）
檢查器	Comparator	SafeVerify，並由 Comparator 交叉檢查（→ 144/492）
題目受到的關注	有編目且經研究的 Erdős 問題	47% 的項目未列參考文獻；451/492 個序列在 OpenAlex 上沒有引用作品

因此，「AI 能解決多少未解問題」這個問題，若不說明題目如何挑選，就沒有答案；兩種選題方式讓解題率相差一個數量級，而花費只有六分之一。這是該語料支持本頁篩選步驟的最有力證據，同時也最有力地提醒人們：在有人說明由誰按什麼標準選題之前，未解問題的標題百分比毫無意義。這也重新界定前面的 Fisher 精確檢定保留條件：本頁無法判定的 2 對 0 差異不是測量失敗，而是採用高難度分母的結果；Epoch 自己的低難度分母則展示了同一套工具在題目不同時的表現。

兩者之間有三項可互相參照的結果。 OEIS Open 部分回答了本頁關於預算擴展的問題：花費曲線約按對數線性上升，每增加十倍預算，解題率提高約十個百分點，直到 $200 都沒有平台期——但其基準解題率為 30%，因此對 3% 區間幫助有限。它也直接提供成本階梯的對照：每解出一題平均花 $6 至 $10，最高 $47，而本頁每題解答成本為 $172 至 $1,384，邊際成本約 $67,000。它也讓錯誤形式化的疑慮更尖銳，而非降低疑慮：本頁 68 題中有 18 題由 AI 形式化，只有非專家審查；OEIS Open 的全部 492 題則由 Gemini 代理自動形式化，原樣採用，沒有進一步驗證，唯一辯護理由是：錯誤形式化可能不會偏袒某一個模型。

「形式化能力」另一面隱藏的問題：命題忠實度（2026-09-29）#

本頁的成本計算關注的是無法編譯的證明。SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization（empirical）衡量的是生成命題時相反方向的錯誤：在 178 道困難 Lean 問題中，表現最佳的代理有 61.8% 編譯成功，但只有 11.2% 符合原定理的意思。因此，非正式問題的形式化版本能編譯成功，並不表示原本的命題已獲證明。這項研究與此處間接相關。68 個命題都已提供（50 題出自 Formal Conjectures，18 題由 AI 產生、尚未經專家審查；這是下方第一個待解問題），因此這類錯誤涉及基準測試背後的形式化步驟，而非代理的證明；其方法是將生成命題與影子定理作正向和反向蘊涵檢查，正適合用來審查那 18 題。詳見 Kernel-Level Proof Auditing。

相關連結#

• Kernel-Level Proof Auditing — 說明上表中的 Comparator 並非形式上的差異：它取代了較弱的檢查方式（編譯後用 grep 搜尋原始碼中的 sorry）；對 PutnamBench 上某個已發布證明器測得，這種方式有 31–44% 機率放過依賴 sorryAx 的證明

• Logical vs Intelligible Proof — 說明為何已認證答案的計分數量衡量錯了性質，也記錄了針對此類分母「最容易被基準測試、並自動化取代」的警告。該頁還指出本頁 Erdős-90 數據實際代表什麼：同一結果以兩種產物存在，一份 18 頁、一份 120 萬行，只有前者可讀

• AI-Driven Formal Proof Search — 本基準測試評分的典範，也就是記錄 9/353 數字的頁面；此處是與它對照，而非取代它。形式化成本數據（18 頁 → 120 萬行 Lean，原因明確歸於 mathlib 覆蓋度）是該頁的詞彙瓶頸在已完成形式化後的實際成本

• AlphaProof Nexus — 9/353 背後的系統，以及規則上的對比：每題成本不含尋找可解題目的搜尋成本；另一方則在每一題上都花固定預算

• Compute-Controlled Benchmarking — 語料中最清楚實踐該頁主張的例子：預算不是伴隨得分披露，而是得分的定義；更高預算的規則外測試也公開，但明確不承認為得分

• Expenditure Horizon — 另一項以美元衡量能力的 2026 年指標，也是同一設計空間的另一端：METR 需要平滑的報酬和人類報酬曲線，而開放 Erdős 問題無法提供，因此此基準報告固定預算下的解題數與每題解答成本分布，METR 則報告跨越點

• Benchmark Contamination and Decontamination — 另一種依題目特性預防污染的方式：題目在解出前沒有答案可供外洩；解出後即失去免疫力，後續計畫是事後篩除分母

• Latent Capability Overhang — 在單一模型內量測該頁主張：每次嘗試 $300 時解出 2/68；預算不設上限且可重複嘗試時解出 5/68，花費超過 $220,000；本頁也為該頁的實例補上數字，因為單位距離猜想就是 Erdős 問題 90

• The Navier–Stokes AI Claim — 同月缺乏規範的對照案例：沒有分母、沒有預算上限、沒有公開驗證標準；供應商稱模型比本頁評分的模型新一代，並宣稱 Lean 形式化耗時 17 小時，而本頁實測案例有 120 萬行

• Many-Agent Proof Harnesses — 選擇不做形式化的分支；其最有力的論據正是本頁第一項保留條件：形式化是「接上的獨立專案」，一份 18 頁證明要花 120 萬行才完成

• Large-Scale Test-Time Compute — 將成本階梯解讀為開放研究問題上的推論擴展曲線；Epoch 表示目前尚無人系統性測量這條曲線

• OEIS Open Benchmark — 同一作者在 2026 年的另一項未解問題基準測試，也是本頁的校準對照：492 個 OEIS 猜想刻意排除著名問題，每題 $50，得分為 147/492 = 30%，對照本頁的 2/68 = 3%。它也提供本頁選用 Comparator 的檢查器數據：將 SafeVerify 接受的提交重新交給 Comparator 檢查，得分往兩個方向各變動三個猜想

• Epoch AI — 基準測試的發起者

• Lean — 形式化目標；Comparator 是在其上建構的抗作弊檢查器

• Statement Drift — 說明本頁 18 個自動形式化命題與 Bloom 忠實度審查的關係：Comparator 保證證明符合可信副本，只有策展者的閱讀能保證副本本身就是 Erdős 問題

尚待解答的問題#

• 18 個 AI 產生的形式化命題能否通過專家審查？五個已解問題中有沒有任何一題屬於這 18 題？ Epoch 表示這 18 題只通過由自稱非 Lean 專家的團隊進行的初步審查，專家審查「正在進行」，但從未說明哪些已解題目來自哪個子集。若已解題目中有錯誤形式化，標題上的成果就只是形式產物；若沒有，得分仍然成立，但分母的可靠性仍有疑慮。**2026-09-29 由 FLT: Anthropic has beaten me to it（case-study）補充：**此案例形成對照，命題經過專家審閱：Buzzard 表示自己檢查過 FLT 命題是否符合定理，並指出這是機器無法檢查的部分。此案例沒有提供 Epoch 那 18 題的資訊。**2026-09-29 由 Long-horizon autoformalization of a core theorem underlying MIP* = RE（case-study）補充：**第二個對照案例，也是首個專家審查改變形式化命題的案例：原論文的一位共同作者審查了頂層定理和缺口解決方式；25 項缺口註記促成修正已發表命題中的兩項錯誤，以及錯誤預算中的三項錯誤（最後界限不變）。此案例也說明未經審查的 AI 形式化為何有風險：代理產生了同義反覆的別名，以及把結論直接寫進前提的命題，而且都能編譯成功。仍沒有 Epoch 那 18 題的相關資訊。****2026-09-29 由 FrontierMath Erdős（empirical）部分解答：**這些命題並非完全沒有經過審查——Bloom 逐一檢查了 18 個自動形式化猜想（涵蓋 17 個問題）是否忠於原問題；但他是策展者，並非 Lean 形式化審查者，論文也沒說明五個已解問題中有沒有任何一題屬於這 18 題。仍有兩個問題：是否經過獨立的 Lean 專家審查，以及五題解答的來源。

• 解題數如何隨每次嘗試的預算及嘗試次數成長？ Epoch 將其列為未來研究，而自己的規則外資料只是未受控制的版本：解出 5 題、269 172 次無成果嘗試（論文重新計算）、花費超過 $220,000，對照約 $20,000。可檢驗的形式是：讓同一模型對相同的 68 題分別以 $300／$1,000／$3,000 預算各嘗試 k 次，查看解題覆蓋率是否像有驗證器的已封閉基準測試一樣按對數線性成長，或是受限於可觸及問題的數量而抵達上限。**2026-09-23 由 OEIS Open: How many conjectures can language models turn into theorems? 在不同題目集合上部分回答。**OEIS Open 正好進行這項測量——在八次執行、兩種預算上限和五個模型中，按解題當下每個樣本的花費比較解題率——發現解題率大致隨支出按對數線性成長，每增加十倍預算，解題率提高約十個百分點；在 $200 上限內看不到平台期。以同一模型為例，Claude Opus 4.8 的得分從 $50 時的 30% 升至 $200 時的 39%；Epoch 推估 $200 時約解出 492 題中的 216 題，高於 $50 時實測的 147 題。因此，在某些未解問題集合上，曲線會按對數線性成長，而非觸頂；這是目前最先出現的相關證據。不過此處的問題仍未解，有三個原因：基準解題率是 30% 而非 3%，所以斜率只在本基準從未涵蓋的區間測得；支出軸是根據固定預算執行期間何時解題回推，而非分別以不同上限執行獨立測試，論文也指出偏差本身（代理會收到預算資訊，可能因此改變行為）；此外，嘗試次數的影響尚未測試——OEIS Open 對每個模型與設定只執行一次，因此這個問題中 k 次嘗試的部分仍未測量。

• 事後污染修正能否維持分數可比性？可用分母縮小的速度會不會快過能力成長？ Epoch 的計畫是篩除在模型訓練截止日前已解出的問題，再以剩餘題目比較。觸發事件：此題組中部分問題公開解答後，首次以新模型進行測試。

• 五個 AI 證明能否經得起人類仔細理解？#1 和 #571 是否真的是新成果？ 論文指出，這些證明通過核心驗證，但「尚未消化」；#571 的證明與既有成果之間的關係「需要花些時間釐清」。作者承諾撰寫的人類可讀解說，或文獻比對，都能檢驗此事。觸發事件：五題中任一題首次出現經同儕審查的解說。

參考來源#

• On the Navier–Stokes Millennium Prize Problem — OpenAI（無署名），openai.com，2026-09-08 發布並於 2026-09-10 更新，約 1,900 字，vendor-claim。本文只引用其中兩項主張，兩者都直接引自公告文字：透過 GPT‑6 Astra 花 17 小時進行 Lean 形式化，以及截至 2026-08-28 開始訓練時，內部模型「能力明顯高於 GPT‑6 Astra」。兩項都無法驗證——未取得連結的證明 PDF 和 Lean 儲存庫，模型也尚未發布，而且結果受到質疑。此來源用來界定本頁數字的適用範圍，絕不據此調整數字。完整分析見 The Navier–Stokes AI Claim
• Announcing FrontierMath Erdős — Tom Adamczewski 和 Greg Burnham（Epoch AI），「Announcing FrontierMath Erdős」，epoch.ai，2026-09-01，約 2,250 字，empirical。這是網頁文章，不是從 PDF 擷取：文中兩張表格皆依原始 HTML 表格轉錄，並於上文完整引用。此項評估的依據與薄弱之處。 測量結果真實存在，測試框架和題目清單也已公開原始碼，但仍有三項限制：標題中的模型是預發布 GPT-6 Astra，因此外界無法重現的數字恰好是唯一非零得分；預發布存取權暗示公告未說明的實驗室關係；配套論文（epoch.ai/files/frontiermath-erdos.pdf）收錄每題解答摘要與完整方法，但不在此語料中——本文所有資訊都來自公告；計分測試每題只嘗試一次，因此 2/68 對 0/68 是兩個事件（雙尾 Fisher 精確檢定 p ≈ 0.50），公告沒有提出此統計保留條件。Epoch 是獨立評估者，而非模型供應商，並且用會使頭條數字降低的方式約束自己——它公開了花費超過 $220,000、解出 5/68 的規則外測試，並明確拒絕將其列為得分；這與追求漂亮基準數字的做法相反。Erdős 問題編號（1、74、90、126、548、571）採用 Bloom 在 erdosproblems.com 上的編號
• OEIS Open: How many conjectures can language models turn into theorems? — Tom Adamczewski（Epoch AI），「OEIS Open: How many conjectures can language models turn into theorems?」，arXiv 2608.11941，2026-08-12，27 頁，empirical。本頁主要來源的同一第一作者，早六週發表。本文引用它的 492 個猜想分母與選題提示、$50／$200 上限、147/492 與 144/492 得分、每題解答成本範圍、對數線性支出曲線，以及題目受到關注程度的中繼資料。內容取自 PDF；上文數字皆來自論文文字或圖表，單一表格則與 pdftotext -layout 交叉核對，但文中未引用該表。完整分析見 OEIS Open Benchmark
• After Math — De Toffoli 與 Duede，「After Math」，Terence Tao 部落格客座文章，2026-09-12，約 2,000 字，practitioner-opinion。本文引用其中對基準測試的警告、答案與解答之間的區別，以及 mathandai.org 聲明（25 位菲爾茲獎得主連署，「嚴重錯位」）。該文從未提及 FrontierMath、Epoch AI 或此基準測試——它針對的是 OpenAI 公告和數學領域規範；此處的連結是本維基提出的。文中沒有任何測量；聲明本身也未取得。完整分析見 Logical vs Intelligible Proof
• FLT: Anthropic has beaten me to it — Buzzard，2026-09-04，case-study。只用來對照尚待解答問題中的命題審查情形。
• Long-horizon autoformalization of a core theorem underlying MIP* = RE — Lu、Deng、Zhu 與 Ji，arXiv 2609.19814 v2，2026-09-17，case-study。只在專家審查待解問題中引用，用於對照經審查的命題。完整註記見 wiki/sources.md。
• FrontierMath Erdős — Tom Adamczewski（Epoch AI）與 Thomas F. Bloom（曼徹斯特大學），「FrontierMath Erdős」，arXiv 2609.25050，2026-09-06，12 頁，empirical（保留原分級）。內容取自 PDF；上文所有數字皆來自論文文字、圖說或對照文字閱讀表 1–3（表 3 的 #126 列在同一格包含四次嘗試成本，是實際清單；不是表格轉換造成錯誤合併，已用文字中的「四個 #126 證明」確認）。本文未逐列引用表 4（68 個單行命題）。Bloom 同時是共同作者、策展者，也是自動形式化命題的審查者，因此題目選擇與命題審查都非獨立於論文作者；同一測試的公告數字與論文不同，本文已用論文數字取代。完整編譯註記見 wiki/sources.md。
• SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization — Han 等人，arXiv 2608.29270，2026-08-29，empirical。本文只引用一段內容：178 道生成 Lean 命題中，61.8% 可編譯，11.2% 語意一致；並引用正向／反向影子檢查方法，說明它可用於審查 18 個 AI 產生的形式化版本。完整分析見 Kernel-Level Proof Auditing。
• ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization — Wang、Li 與 Yuan，arXiv 2609.34960，2026-09-28，empirical。本文只引用函式庫移除實驗相關段落。