# 數學猜想難度矩陣
## 從單一難度等級到障礙向量、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 不是只以答案長度分級，而是使用三個主要維度：

1. **Background**：解題所需的背景知識；
2. **Creativity**：專家找到核心想法所需的時間；
3. **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 的主要比較方式應是：

1. **向量比較**；
2. **瓶頸維度比較**；
3. **Pareto 偏序**；
4. **方法相對投影**；
5. **時間序列變化**。

---

## 4.1 Pareto 偏序

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

\[
C_1 \prec C_2.
\]

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

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

---

## 4.2 瓶頸表示

可定義主要瓶頸集合：

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

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

```text
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\) 的認識，同時縮小方法空間。

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

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

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

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

---

# 9. MCDM 猜想卡

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

```yaml
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