數學猜想難度矩陣

從單一難度等級到障礙向量、AI 可攀爬性與研究進展累積率

英文題名： Mathematical Conjecture Difficulty Matrix: From Scalar Difficulty Tiers to Obstruction Vectors, AI Climbability, and Progress Accumulability
縮寫： MCDM
版本： v0.1
日期： 2026-07-24
文件性質： 理論論文／數學研究基礎設施提案

摘要

現有數學與人工智慧評測體系，已普遍使用難度分級、專家工時、背景知識、創造性、執行成本、形式驗證成功率與專用 verifier 等指標。然而，這些體系主要用於評估已整理完成的封閉題目、競賽題、短期研究題或可由專用程式驗證的開放問題，尚不足以描述長期數學猜想的完整困難結構。

本文提出「數學猜想難度矩陣」（Mathematical Conjecture Difficulty Matrix, MCDM）。其核心主張是：

\boxed{\text{數學猜想的難度不是單一分數，而是一個障礙向量。}}

對猜想 (C)，本文定義基本難度向量：

\mathfrak D(C) = (B,I,E,F,V,R,G,U),

分別表示背景負載、核心洞見障礙、執行負載、形式化成熟度、可驗證性、研究阻力、全域耦合度與判定域不確定性。在此基礎上，再加入人類摘要難度 $L_0\!-\!L_9$ 、AI 可攀爬性 $A_0\!-\!A_5$ ，以及研究進展累積性 $P_0\!-\!P_5$ 。

本文反對以固定權重將所有維度壓縮成單一總分，主張以向量、偏序、瓶頸維度與方法相對狀態共同表示猜想難度。此框架可用於數學猜想資料庫、AI 自主數學平台、研究任務調度、形式化優先級、長期進展追蹤與跨模型能力比較。

1. 問題背景

數學題目的難度分級並不是新事物。競賽、資格考試、數學教育、定理證明基準與人工智慧評測，都需要判斷一道題目究竟屬於例行推導、創造性難題、研究級任務，還是當前不可完成的開放問題。

近年的 AI 數學基準已開始採用更精細的分類。FrontierMath 不是只以答案長度分級，而是使用三個主要維度：

Background：解題所需的背景知識；
Creativity：專家找到核心想法所需的時間；
Execution：將核心想法轉化為完整答案所需的工作量。

其最高難度 Tier 4 被設計為教授或博士後等級的短期研究專案，而非普通競賽題。[1]

FrontierMath: Open Problems 更進一步要求問題必須是未解、曾被至少兩位專業數學家認真嘗試、解決後具有可發表價值，而且候選答案能由專用程式高度可靠地驗證。[2] 這顯示現代評測已經開始重視：

\text{困難性} + \text{研究價值} + \text{候選答案可驗證性}.

另一方面，Formal Conjectures 將大量研究問題的命題陳述形式化為 Lean 4，並明確指出：形式化不只是為了建立題庫，也能澄清猜想的精確含義、暴露 Mathlib 中缺失的定義，並建立可供自動定理證明系統使用的研究級基準。[3][4]

TheoremBench 則指出，對形式證明系統而言，只計算最終定理是否完成並不足夠。還必須評估支撐子定理的覆蓋率、依賴結構、證明 token 效率，以及模型是否只會挑選容易的局部引理，而缺乏長程證明計畫。[5]

這些發展共同說明：數學難度已不再適合用「簡單、中等、困難」三個詞概括。

但仍有一個尚未被充分處理的缺口：

現有基準主要評估一個已經整理好的任務有多難；它們較少描述一個長期數學猜想為什麼會持續抵抗多代研究者、多種方法與大量局部進展。

本文的目標，就是建立適用於這類開放猜想的結構化難度框架。

2. 題目難度與猜想難度的差異

一道封閉題目通常具有以下特徵：

問題陳述相對穩定；
已知存在答案；
核心方法位於既有理論範圍內；
解答完成後可以立即判定正誤；
解題歷程通常不會改變問題本身。

長期數學猜想則可能具有完全不同的結構：

尚不確定應該證明還是尋找反例；
問題的最佳表示方式仍未知；
現有理論可能不足以承載解法；
不同方法只能控制猜想的不同投影；
局部進展可能被其他部分抵銷；
候選證明的驗證成本本身可能極高；
問題可能接近公理系統或可計算性的邊界。

因此，猜想難度不能只問：

\text{「一位專家需要多少小時完成？」}

而必須進一步問：

\text{「這個猜想由哪些障礙組成？」}

\text{「這些障礙能否分解？」}

\text{「局部進展是否能累積？」}

\text{「候選答案能否低成本地驗證？」}

\text{「現有方法的失敗是否能縮小剩餘判定域？」}

3. 核心主張：難度是一個障礙向量

令 (C) 為一個精確陳述的數學猜想。本文定義其基本難度向量為：

\mathfrak D(C) = (B,I,E,F,V,R,G,U).

每一個分量都表示一種相對獨立的障礙。

這個表示法並不主張八個維度已經窮盡所有數學困難，而是提供一個最小可用核心，使不同猜想可以在相同架構下描述。

3.1 背景負載 (B)

Background Load

背景負載衡量理解、操作與審查猜想所需的既有知識量。

建議分級：

等級	說明
B0	初等數學即可理解與操作
B1	大學基礎數學
B2	單一領域研究所知識
B3	單一領域研究前沿
B4	多個成熟領域的交叉知識
B5	多領域前沿與大量專門文獻
B6	需要尚未建立的新理論語言

背景負載不等於證明難度。一個命題可能需要極深背景，但一旦理解後證明相對直接；另一個命題可以用初等語言陳述，卻需要極難的新洞見。

3.2 核心洞見障礙 (I)

Insight Barrier

核心洞見障礙衡量現有工具與最終解法之間的概念距離。

等級	說明
I0	已知定理直接套用
I1	已知技巧的標準組合
I2	已知技巧的非典型組合
I3	需要重新表示問題
I4	需要新的關鍵引理族
I5	需要新的方法或不變量
I6	需要建立新理論
I7	可能需要改變問題的基礎框架

這一維比籠統的「創造力」更適合研究猜想，因為它描述的是解法必須跨越何種概念斷層。

3.3 執行負載 (E)

Execution Load

執行負載衡量已知核心方法之後，完成證明、反例或證書仍需多少工作。

它可能來自：

長篇符號推導；
大量情況分類；
高精度計算；
叢集搜尋；
數值誤差控制；
形式化程式碼；
多個軟體系統之間的證書轉換；
長期同行審查。

等級	說明
E0	幾步即可完成
E1	一般手算或短證明
E2	數小時至數天
E3	數週或需程式輔助
E4	大型計算或長篇形式證明
E5	多團隊、多系統、長期驗證
E6	當前算力或形式化能力不足

洞見障礙與執行負載必須分開。一個問題可以有極高的 (I) 而只有很低的 (E)，也可以核心想法簡單但執行規模極大。

3.4 形式化成熟度 (F)

Formalization Readiness

形式化成熟度衡量猜想及其前置理論是否已準備好進入證明助理。

此維度的方向與其他障礙不同：數值越高代表成熟度越高，而不是越困難。

等級	狀態
F0	自然語言陳述仍有歧義
F1	命題可被精確數學化
F2	核心對象已有形式定義
F3	部分前置引理已形式化
F4	可在證明助理中完整陳述
F5	有穩定的形式化依賴環境
F6	可端到端由核心檢查器驗證

Formal Conjectures 顯示，形式化開放問題本身就是研究基礎設施：它能暴露定義缺口、澄清自然語言陳述，並產生可供自動證明系統使用的標準介面。[3][4]

形式化成熟度不應與數學真實性混為一談。核心檢查器只能確認某個形式命題被證明，不能自動保證該命題忠實表達原本的自然語言問題。近期對 Lean 基準的審計也發現，錯誤形式化、缺少假設、空洞命題與評測漏洞，仍可能污染表面上的機器驗證結果。[6]

3.5 可驗證性 (V)

Verifiability

可驗證性衡量候選解出現後，確認其正確性需要多少成本。

建議將驗證型態區分為：

等級	驗證型態
V0	有限直接代入即可驗證
V1	短程式或專用 verifier
V2	可重播計算證書
V3	可由形式證明核心驗證
V4	需要跨多套形式與數值系統
V5	主要依賴專家長期審查
V6	候選解本身也難以明確判定

一個猜想可能很難求解，但很容易驗證。例如，找到一個有限反例或特定組合結構。另一個猜想則可能產生數百頁分析證明，其正確性需要多年審查。

FrontierMath: Open Problems 明確將「候選答案能否由普通電腦上的專用程式高度可靠地驗證」視為選題條件，說明可驗證性已成為 AI 研究評測的核心設計變數。[2]

3.6 研究阻力 (R)

Research Resistance

研究阻力是猜想對歷史研究投入所呈現的經驗性抗性。

可納入：

猜想存在時間；
認真嘗試的研究者數量；
參與者的專業程度；
已知失敗方法數量；
錯誤證明的頻率；
等價命題數量；
經歷重大理論進步後是否仍未解；
是否已有大規模計算驗證。

研究阻力不是猜想本體難度的純粹測量。知名猜想會得到更多嘗試，冷門猜想可能只是缺乏注意力。因此 (R) 應視為後驗證據，而不是單獨的難度判決。

3.7 全域耦合度 (G)

Global Coupling

全域耦合度衡量猜想能否被分解成相對獨立的子問題。

等級	耦合型態
G0	完全可分解，子問題完成即可合成
G1	弱依賴，可局部獨立推進
G2	有限交叉依賴
G3	多模組耦合，需要共享中間結構
G4	局部改進可能破壞其他條件
G5	多種主要方法最終回到共同瓶頸
G6	可能只有整體新框架才能閉合

這是 MCDM 相對於一般題目難度分級最重要的新增維度之一。

對低耦合問題，研究可以寫成：

C=C_1\land C_2\land\cdots\land C_n,

而且每完成一個 $C_i$ ，總進度就單調增加。

對高耦合問題，則可能出現：

\text{改善條件 }A \Longrightarrow \text{惡化條件 }B.

此時大量局部成果並不必然意味著接近最終解答。猜想可以產生上百個真實新引理，卻仍停留在相同的全域閉合障礙之前。

3.8 判定域不確定性 (U)

Decidability Uncertainty

此維度描述的不是「猜想現在還沒解」，而是我們是否知道它應以何種形式被解決。

等級	狀態
U0	已知可由普通證明或反例解決
U1	真或假均可由有限證書確認
U2	原理上可判定，但可能需要巨大資源
U3	目前方法族沒有可信閉合路徑
U4	懷疑需要更強公理或新基礎
U5	已形成正式獨立性候選
U6	已證明相對指定公理系統獨立

必須嚴格區分：

\text{目前沒有方法}

與：

\text{在某形式系統中不可判定}.

前者是方法相對不可達，後者是邏輯獨立性結果。兩者不能共用同一標籤。

4. 為何不應直接加總成單一分數

最直觀的做法是設定權重：

[ D(C)

w_BB+w_II+w_EE+w_FF+w_VV+w_RR+w_GG+w_UU. ]

本文不建議將其作為主要表示。

原因是不同障礙之間通常不可補償。

例如：

極高的形式化成熟度，不能抵銷缺乏核心洞見；
大量算力，不能自動抵銷高全域耦合；
容易驗證的反例，不能保證反例容易找到；
深厚背景知識，不能替代新的理論框架。

兩個猜想即使得到相同總分，也可能具有完全不同的研究性質：

[ (6,2,1,6,1,2,1,0) ]

和：

[ (2,6,3,1,5,5,6,4). ]

前者可能只是背景極深但結構清楚；後者則可能背景較低，卻高度耦合、難以驗證，且解決型態本身不確定。

因此，MCDM 的主要比較方式應是：

向量比較；
瓶頸維度比較；
Pareto 偏序；
方法相對投影；
時間序列變化。

4.1 Pareto 偏序

若猜想 $C_1$ 在所有障礙維度上都不高於 $C_2$ ，且至少一項更低，才可以說：

C_1 \prec C_2.

若兩者各有不同瓶頸，則應視為不可直接排序。

這比強迫所有猜想排成一條直線更忠實。

4.2 瓶頸表示

可定義主要瓶頸集合：

\operatorname{Bottleneck}(C) = \{d:\ d(C)\ge\tau_d\}.

例如某猜想可能被標記為：

Primary bottlenecks:
- I6: new theory required
- G5: global recoupling
- V5: long expert audit

這比「難度 92 分」更能指導研究。

5. 人類摘要難度層級 $L_0-L_9$

向量適合研究系統，但公共展示仍需要簡化標籤。本文提出十級摘要層級。

$L_0$ ：已解且可直接驗證

已知定理或測試命題；
證明短；
適合作為系統正確性檢查。

$L_1$ ：例行推導題

方法明確；
不需新洞見；
主要困難是基本執行。

$L_2$ ：高階既有方法題

需要大學高年級或研究所背景；
解法仍位於成熟理論範圍內。

$L_3$ ：極難競賽或資格考題

需要非顯然洞見；
通常可在數小時至數天內完成；
答案仍相對短而封閉。

$L_4$ ：專家短期研究題

需要數天至數週；
可能需要文獻、程式與高階計算；
核心理論已存在。

此級大致覆蓋 FrontierMath 高階封閉題與 Tier 4 類短期研究任務。[1]

$L_5$ ：局部開放研究問題

解決後具有論文價值；
已有專家嘗試；
預期數週至數年；
通常仍局限於一個領域；
成功或反例可清楚驗證。

$L_6$ ：理論擴充型猜想

現有理論不足；
需要建立新引理族、工具或形式化基礎；
可拆分成多個長期研究節點。

$L_7$ ：跨領域全域耦合猜想

涉及多個領域；
局部進展可能互相抵銷；
依賴圖龐大；
單一研究者或單一代理難以維持完整上下文。

$L_8$ ：世代級核心猜想

數十年至百年以上歷史；
大量頂尖研究者投入；
經歷多次理論進步仍未閉合；
解決可能需要新的研究綱領；
驗證本身也可能是大型工程。

$L_9$ ：基礎或判定邊界型猜想

不清楚應尋找證明、反例、新公理或獨立性結果；
問題的解決型態本身仍不確定；
可能接近形式系統強度或可計算性邊界。

需要強調：

L_9 \neq \text{比 }L_8\text{ 更困難的普通問題}.

它代表問題類型可能已經改變。

6. AI 相對難度：可攀爬性 $A_0-A_5$

數學難度不是完全獨立於求解者。

同一個猜想對人類與不同 AI 系統可能具有不同難度。因此應將人類難度與 AI 相對難度分開：

[ D_H(C) ]

表示人類研究難度，而：

D_A(C\mid M,T,S)

表示猜想 (C) 在模型 (M)、工具環境 (T) 與研究狀態 (S) 下的 AI 難度。

本文提出 AI 可攀爬性：

等級	說明
A0	現有模型可直接完成
A1	加入工具與少量多輪即可完成
A2	需要形式化、搜尋或大量計算
A3	能持續產生局部進展，但尚不能閉合
A4	需要新表示、新理論或長期研究記憶
A5	目前缺乏可信攻擊介面

AI 往往特別適合：

大量分支探索；
符號與程式生成；
有限反例搜尋；
文獻交叉比對；
形式證明嘗試；
可重播證書生產；
重複性計算與審計。

但目前仍較弱於：

長期維持統一研究意圖；
判斷真正有生產力的抽象；
在數百個局部結果中辨識共同瓶頸；
發明足以改變整個問題的新表示；
發現問題陳述或形式化本身錯誤；
管理跨年度理論版本與失敗知識。

FormalProofBench 顯示，即使題目已提供自然語言與 Lean 形式陳述，現有模型在研究所等級正式證明上的成功率仍明顯有限。[7] TheoremBench 也顯示，模型常偏向容易的支撐子定理，並以冗長 tactic 軌跡取代緊湊的全域證明計畫。[5]

因此，AI 可攀爬性不等於數學本體難度。它描述的是一個猜想是否已經具有適合當代 AI 攻擊的介面。

7. 研究進展累積性 $P_0-P_5$

僅知道一個猜想很難，仍不足以決定是否值得投入上百或上千輪 AI 研究。

更重要的變數是：

\boxed{\text{每一輪研究是否能使下一輪站在更高的位置。}}

本文定義研究進展累積性：

等級	說明
P0	失敗幾乎不留下可重用成果
P1	可保存少量技巧或反例
P2	可排除局部參數、特例或方法
P3	可建立系統性的失敗地圖
P4	可形成形式化依賴圖、證書庫與可重播工程
P5	每輪都能單調縮小剩餘判定域

可定義有效累積率：

\alpha_N = \frac{ \text{前 }N\text{ 輪新增且可重用的證書、排除域、依賴更新與形式引理} }{ N }.

也可以定義加權版本：

\alpha_N^{(w)} = \frac{ \sum_{k=1}^{N} w_k \cdot \Delta S_k }{ N },

其中 $\Delta S_k$ 是第 (k) 輪對研究狀態的有效更新量。

一千輪 (P0) 型研究，可能只是重複生成。

一千輪 (P4) 型研究，則可以建立：

完整方法依賴圖；
失敗原因分類；
形式化中間定理；
數值與符號證書；
可移交給未來模型的研究狀態。

因此，預測 AI 是否可能解決某猜想，不應只估計模型能力與研究輪數，而應估計：

\boxed{ \text{預期有效進展} \approx \text{模型能力} \times \text{研究輪數} \times \text{累積率} \times \text{驗證可靠度}. }

8. 難度不是靜態屬性

猜想難度會隨理論、工具與形式化環境改變。

因此應寫成：

\mathfrak D_t(C\mid \mathcal K_t,\mathcal T_t),

其中：

$\mathcal K_t$ 是時間 (t) 的可用數學知識；
$\mathcal T_t$ 是時間 (t) 的工具、算力與形式化基礎設施。

一項新定理可能降低 (B)、(I) 或 (G)；新的證明助理程式庫可能提高 (F)；新的 verifier 可能降低 (V)；大規模失敗研究則可能提高對 (R) 的認識，同時縮小方法空間。

因此，猜想資料庫不應只保存一張固定難度卡，而應保存難度版本歷史：

2026-07:
B5 I6 E4 F2 V5 R6 G5 U3

2028-03:
B5 I5 E4 F4 V3 R6 G4 U2

難度下降本身就是研究成果，即使猜想尚未被最終解決。

9. MCDM 猜想卡

每個猜想可由一張標準卡表示：

conjecture_id:
title:
formal_statement:
informal_statement:
status:
domains:

human_summary_level: L0-L9
ai_climbability: A0-A5
progress_accumulability: P0-P5

difficulty_vector:
  background_load: B0-B6
  insight_barrier: I0-I7
  execution_load: E0-E6
  formalization_readiness: F0-F6
  verifiability: V0-V6
  research_resistance: R0-R6
  global_coupling: G0-G6
  decidability_uncertainty: U0-U6

primary_bottlenecks:
secondary_bottlenecks:

known_partial_results:
known_equivalences:
known_counterexample_ranges:
known_failed_approaches:
formal_dependencies:
computational_dependencies:

candidate_resolution_modes:
  - proof
  - disproof
  - finite_counterexample
  - conditional_theorem
  - method_relative_impossibility
  - independence_result
  - reformulation
  - decomposition

estimated_expert_time:
estimated_compute_cost:
verifier_type:
last_reviewed:
evidence:

這個格式的目的不是宣稱能客觀測量所有數學困難，而是讓不同團隊、AI 模型與研究平台能使用共同語言交換研究狀態。

10. 狀態分類：避免把未知誤寫成不可判定

建議猜想平台至少區分以下狀態：

OPEN

尚未有公認證明或反例。

ACTIVE_PARTIAL

存在可重用的局部結果，但不足以閉合。

FORMALIZATION_BLOCKED

命題或前置理論尚未成熟到可可靠形式化。

VERIFICATION_BLOCKED

已有候選解，但目前缺乏足夠可靠的驗證機制。

METHOD_RELATIVE_UNREACHABLE

在明確指定的方法族、資源上限或證書類型下，已證明無法完成。

CONDITIONALLY_RESOLVED

在附加假設下已解決。

DISPROVED

已有可接受反例或否定證明。

PROVED

已有可接受證明。

FORMALLY_INDEPENDENT

已證明相對某個明確公理系統獨立。

其中最重要的區分是：

\texttt{METHOD\_RELATIVE\_UNREACHABLE} \neq \texttt{FORMALLY\_INDEPENDENT}.

前者是研究方法或資源邊界；後者是數理邏輯定理。

11. 校準方法

MCDM 若要成為可用標準，不能只依靠作者直覺。建議採取多來源校準。

11.1 專家評分

每個維度至少由：

問題提出者；
同領域專家；
相鄰領域專家；
形式化專家；
計算或 verifier 專家；

分別評估。

使用中位數與分歧區間，而不是只公布單一數字。

11.2 經驗資料

可使用：

專家實際工時；
模型成功率；
平均 proof token；
搜尋分支數；
形式化依賴閉包大小；
verifier 執行時間；
失敗類型；
新增引理數量；
每輪有效累積率。

FrontierMath 已將專家時間、背景、創造性與執行成本納入難度評估。[1] TheoremBench 則證明子定理覆蓋率與 token 效率能揭露單一成功率看不見的證明行為差異。[5]

11.3 版本與審計

正式猜想卡應保存：

評分版本；
使用的公理系統；
形式化版本；
程式庫版本；
評分者角色；
模型與工具環境；
證據來源；
已知爭議。

數學基準本身也可能包含錯誤。FrontierMath 於 2026 年發布新版時，曾說明修正了相當比例的問題錯誤；形式證明基準的系統性審計也揭露了大量資料與評測缺陷。[6][8] 因此，難度表本身必須是可版本化、可修正的研究對象。

12. 應用

12.1 AI 自主研究調度

AI 平台可依 MCDM 決定：

哪些猜想適合直接攻擊；
哪些應先補形式化基礎；
哪些需要 verifier；
哪些適合反例搜尋；
哪些應分解成子猜想；
哪些需要多代理並行；
哪些暫時不應投入大量算力。

例如，對 (A2,P4,F5,V2) 的猜想，大量代理搜尋可能非常有效。

對 (A5,P0,F0,V6) 的猜想，直接增加推理輪數通常沒有意義，應先改造問題介面。

12.2 猜想資料庫

傳統資料庫通常只記錄：

命題；
狀態；
參考文獻；
已知部分結果。

MCDM 可進一步記錄：

難度向量；
方法失敗圖；
形式依賴；
驗證方式；
AI 相對難度；
進展累積性；
可能的解決型態。

這使資料庫從靜態百科全書轉變為研究控制平面。

12.3 模型能力比較

模型不應只比較「解對多少題」，也可以比較：

\Delta B,\Delta I,\Delta E,\Delta F,\Delta V,\Delta G.

例如某模型可能不會完成最終證明，但能顯著：

提高形式化成熟度；
降低驗證成本；
找到新的等價表述；
將高耦合問題拆成可管理模組；
建立可累積的失敗地圖。

這些都是研究能力，而不只是答題準確率。

12.4 資金與研究治理

MCDM 也可用於判斷一項長期研究計畫究竟需要：

個人研究；
小型團隊；
形式化工程；
大規模計算；
跨領域合作；
長期基礎設施；
新公理或基礎研究。

它不應用來決定某猜想「值不值得研究」，而是用來理解其資源結構。

13. 限制

MCDM 仍有以下限制。

13.1 難度具有觀察者相對性

不同研究者、模型與工具環境，對同一猜想的背景負載與執行成本不同。

因此評分必須標明：

\text{相對於誰、何時、使用什麼工具。}

13.2 新洞見可能使難度突然崩塌

重大理論突破可能把 (I6) 的問題瞬間降低為 (I2)。

所以難度評分不是對猜想本體的永恆判決，而是某個知識狀態下的最佳估計。

13.3 歷史阻力可能受注意力偏差影響

熱門猜想的 (R) 可能很高，冷門猜想則缺乏足夠觀測。

研究阻力必須附帶研究人口與文獻覆蓋的不確定性。

13.4 形式化不等於忠實形式化

機器核驗只能確認形式系統中的推導。若命題翻譯錯誤，形式證明仍可能與原問題無關。[6]

因此 (F) 與 (V) 都必須包含語義審計。

13.5 不能把難度等級當成學術價值

困難不等於重要，容易也不等於沒有價值。

MCDM 評估的是研究障礙結構，不是美學、重要性、社會價值或歷史地位。

14. 結論

現有數學與 AI 業界已經普遍使用分級、專家時間、創造性、執行成本、形式證明成功率與 verifier 等方法評估數學任務。但這些方法主要針對已整理好的題目或特定可驗證開放問題，尚不足以描述長期數學猜想的完整困難結構。

本文提出：

\boxed{ \mathfrak D(C) = (B,I,E,F,V,R,G,U) }

作為數學猜想的基本難度向量，並加入：

[ L_0-L_9 ]

的人類摘要難度、

[ A_0-A_5 ]

的 AI 可攀爬性，以及：

[ P_0-P_5 ]

的研究進展累積性。

本框架最核心的改變是：

\boxed{ \text{不再只問一個猜想有多難，} \text{而是問它被什麼阻擋、能否分解、如何驗證，} \text{以及研究是否真正累積。} }

對未來 AI 數學研究而言，最重要的預測變數可能不是單次模型分數，也不是總推理輪數，而是：

\boxed{ \text{模型能力} \times \text{研究狀態持續性} \times \text{有效累積率} \times \text{驗證可靠度}. }

數學猜想難度表因此不應只是一張排行榜，而應成為一個可版本化、可審計、可供人類與 AI 共用的研究基礎設施。

參考文獻

[1] Epoch AI. “About FrontierMath.” FrontierMath Tiers 1–4. 2026.
https://epoch.ai/frontiermath/tiers-1-4/about

[2] Epoch AI. “Submit a Problem — FrontierMath Open Problems.” 2026.
https://epoch.ai/frontiermath/open-problems/submissions

[3] Firsching, M., Lezeau, P., Mercuri, S., et al. “Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics.” arXiv:2605.13171, 2026.
https://arxiv.org/abs/2605.13171

[4] The Formal Conjectures Authors. “Formal Conjectures Repository.” Google DeepMind, 2025–2026.
https://github.com/google-deepmind/formal-conjectures

[5] Pham, Q. V., Karimov, E., Galichin, A., and Oseledets, I. “TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics.” arXiv:2606.09450, 2026.
https://arxiv.org/abs/2606.09450

[6] Ammanamanchi, P. S., Bhat, S., and Biderman, S. “Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving.” arXiv:2606.29493, 2026.
https://arxiv.org/abs/2606.29493

[7] Ravi, N., Ying, K., Nesterov, V., et al. “FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?” arXiv:2603.26996, 2026.
https://arxiv.org/abs/2603.26996

[8] Epoch AI. “FrontierMath Tiers 1–4.” Version information and benchmark revisions, 2026.
https://epoch.ai/frontiermath/tiers-1-4

數學猜想難度矩陣_MCDM_v0.1