# 從解題 AI 到審題 AI：Autonomous Mathematical Judgment Beyond Proof Search

**系列：形式封閉與過程完備：AI 數學證明的下一步問題**  
**Paper 08**  
**作者：Neo.K / EveMissLab Research Series**  
**版本：v0.1 — 2026-09-11**

**機構：** EveMissLab／一言諾科技有限公司  
**日期：** 2026-09-11  

---

## 摘要

AI 數學能力通常以「是否能解題」衡量：能否完成 theorem、找到 proof、通過形式驗證、修補 proof gap、搜尋反例或完成長鏈推導。然而，本系列前七篇顯示，當 AI 進入真正前沿數學後，proof search 已不再是唯一核心能力。更高階的問題包括：AI 是否能辨認形式命題與科學問題之間的差距？是否能主動審計箭頭合法性、same-parent path、completion operator 與量詞升格？是否能在 theorem 已經通過 Lean 之後仍然追問「這到底證明了哪一種存在」？更進一步，AI 是否能判斷官方 benchmark 本身只是較弱 formulation，並主動提出更強、更自然或更具生成性的下一個問題？

本文將 AI 數學研究能力劃分為六層：

$$
\mathsf A_0:
\text{Symbolic Competence},
$$

$$
\mathsf A_1:
\text{Proof Search},
$$

$$
\mathsf A_2:
\text{Proof Criticism},
$$

$$
\mathsf A_3:
\text{Problem Criticism},
$$

$$
\mathsf A_4:
\text{Problem Reconstruction},
$$

$$
\mathsf A_5:
\text{Autonomous Mathematical Judgment}.
$$

本文主張，真正的研究型 AI 必須超越：

$$
\boxed{
\text{“Can I prove the stated theorem?”}
}
$$

進入：

$$
\boxed{
\text{“Is this theorem the right object to prove?”}
}
$$

並最終能回答：

$$
\boxed{
\text{“Given the current result, what should mathematics ask next?”}
}
$$

本文整合前七篇所提出的 Theorem Closure、Arrow Closure、Same-Parent Closure、Completion Closure、Claim Scope Discipline、Objective Diversity 與 Specification-Minimal Resolution，提出一套 Autonomous Mathematical Judgment Architecture。其核心不是要求 AI 任意「有立場」，而是要求 AI 能主動擁有 evaluation frame、區分不同 ontology、發現未被寫入 specification 的科學義務，並在完成 theorem 後生成更強 successor research program。

---

## 關鍵詞

AI 數學、Autonomous Mathematical Judgment、Proof Search、Proof Criticism、Problem Reconstruction、Meta-Objective、形式化證明、研究判斷、問題重寫、AI Scientist

---

# 1. 為什麼「會解題」仍然不是研究能力的終點？

傳統 benchmark 問：

$$
\boxed{
\text{Can the model solve }T?
}
$$

例如：

$$
\Gamma\vdash T.
$$

這對衡量 symbolic reasoning、proof search 與形式能力極有價值。

但真正研究活動往往不是從一個已經完美定義的 $T$ 開始。

研究者會先問：

$$
\text{What is the actual question?}
$$

然後：

$$
\text{Which formulation captures it?}
$$

再問：

$$
\text{Which assumptions are essential?}
$$

以及：

$$
\text{If this theorem is solved, what remains?}
$$

所以：

$$
\boxed{
\text{research}
\neq
\text{theorem completion alone}.
}
$$

---

# 2. 第一層：Symbolic Competence

定義：

$$
\mathsf A_0:
\text{Symbolic Competence}.
$$

包括：

- 讀懂符號；
- 代數操作；
- 局部推導；
- theorem statement parsing；
- 定義展開；
- pattern matching。

這是所有後續能力的底層。

但：

$$
\mathsf A_0
$$

只表示：

$$
\text{能操作數學語言}.
$$

不表示：

$$
\text{能完成 proof}.
$$

---

# 3. 第二層：Proof Search

定義：

$$
\mathsf A_1:
\text{Proof Search}.
$$

核心問題：

$$
\boxed{
\text{Given }T,\text{ find }\pi\text{ such that }\operatorname{Check}(\pi,T)=1.
}
$$

這一層包括：

- theorem proving；
- tactic synthesis；
- proof planning；
- lemma retrieval；
- case split；
- counterexample search；
- formal verification loop。

當 AI 能在高難度數學上完成：

$$
\mathsf A_1,
$$

已經是巨大能力突破。

但：

$$
\mathsf A_1
$$

仍然預設：

$$
T
$$

是值得被證明的目標。

---

# 4. 第三層：Proof Criticism

定義：

$$
\mathsf A_2:
\text{Proof Criticism}.
$$

這一層不只問：

$$
\text{Can I produce a proof?}
$$

而問：

$$
\text{Where can this proof fail?}
$$

包括：

$$
\text{hidden assumption},
$$

$$
\text{quantifier mismatch},
$$

$$
\text{invalid limit transfer},
$$

$$
\text{wrong compactness use},
$$

$$
\text{branch switching},
$$

$$
\text{unproved regularity},
$$

$$
\text{definition mismatch}.
$$

所以：

$$
\boxed{
\mathsf A_2
>
\mathsf A_1
}
$$

在研究判斷上更高階。

---

# 5. 第四層：Problem Criticism

定義：

$$
\mathsf A_3:
\text{Problem Criticism}.
$$

這一層不只攻 proof。

它攻：

$$
\boxed{
\text{the target itself}.
}
$$

問題包括：

$$
\text{Does }T\text{ capture the intended phenomenon?}
$$

$$
\text{Are we proving a weaker surrogate?}
$$

$$
\text{Which assumptions were inserted only for tractability?}
$$

$$
\text{Does theoremhood match public interpretation?}
$$

$$
\text{Did an existential problem replace a generative problem?}
$$

這一層正是本系列在 Navier–Stokes 個案中反覆做的事。

---

# 6. 第五層：Problem Reconstruction

定義：

$$
\mathsf A_4:
\text{Problem Reconstruction}.
$$

當 AI 發現：

$$
T
$$

太弱、太窄、錯層或不完整，它不只是說：

> 這有問題。

而是提出新的：

$$
T'.
$$

例如：

$$
T
=
\text{forced C/D breakdown},
$$

AI 可主動生成：

$$
T'
=
\text{unforced residual elimination}.
$$

或：

$$
T''
=
\text{same-parent process-complete singularity theorem}.
$$

所以：

$$
\boxed{
\mathsf A_4
=
\text{critique}
+
\text{replacement}.
}
$$

---

# 7. 第六層：Autonomous Mathematical Judgment

本文把最高層定義為：

$$
\mathsf A_5:
\text{Autonomous Mathematical Judgment}.
$$

它不是：

$$
\text{AI 隨便有意見}.
$$

而是：

$$
\boxed{
\text{AI can choose and justify the evaluation frame itself.}
}
$$

包括：

- 判斷 theorem 是否只是 formal closure；
- 判斷哪個 stronger formulation 更自然；
- 判斷哪些 objection 是 blocking；
- 判斷哪些只是 scope limitation；
- 判斷何時應接受結果；
- 判斷何時應要求更強 theorem；
- 判斷下一個研究問題；
- 判斷一個方法是否具有可遷移性。

---

# 8. 六層能力階梯

本文正式寫成：

$$
\boxed{
\mathsf A_0
\to
\mathsf A_1
\to
\mathsf A_2
\to
\mathsf A_3
\to
\mathsf A_4
\to
\mathsf A_5.
}
$$

即：

$$
\text{Symbolic Competence}
$$

$$
\to
$$

$$
\text{Proof Search}
$$

$$
\to
$$

$$
\text{Proof Criticism}
$$

$$
\to
$$

$$
\text{Problem Criticism}
$$

$$
\to
$$

$$
\text{Problem Reconstruction}
$$

$$
\to
$$

$$
\text{Autonomous Mathematical Judgment}.
$$

這是本系列最重要的 AI capability taxonomy。

---

# 9. 為什麼前沿 AI 很容易停在 $\mathsf A_1$ 或 $\mathsf A_2$？

因為：

$$
\mathsf A_1
$$

和：

$$
\mathsf A_2
$$

最容易形成可驗證 benchmark。

例如：

$$
\operatorname{LeanCheck}(\pi,T)\in\{0,1\}.
$$

或：

$$
\operatorname{Counterexample}(T)\in\{0,1\}.
$$

但：

$$
\mathsf A_3,\mathsf A_4,\mathsf A_5
$$

很難有單一 binary verifier。

「這是不是更好的問題？」

沒有簡單 kernel。

所以：

$$
\boxed{
\text{verifiability pressure favors lower layers}.
}
$$

---

# 10. 評價座標系本身必須成為研究對象

設：

$$
\mathcal E
$$

為 evaluation frame。

普通 AI 接受：

$$
\mathcal E
$$

作為 given。

Autonomous Mathematical Judgment 則允許：

$$
\mathcal E\to\mathcal E'.
$$

也就是：

$$
\boxed{
\text{evaluation-frame revision}.
}
$$

例如原 frame：

$$
\mathcal E_0:
\text{Does proof satisfy Clay C/D?}
$$

新的 frame：

$$
\mathcal E_1:
\text{Does proof explain forward singularity generation?}
$$

兩者都合理。

但回答不同問題。

---

# 11. Evaluation Frame Ownership

本文提出：

$$
\boxed{
\text{Evaluation Frame Ownership}.
}
$$

一個 AI 若只會：

$$
\text{accept user/author frame}
$$

則即使 proof skill 很強，也還不是完整自主研究者。

真正高階 AI 應能說：

$$
\text{“Under frame }\mathcal E_0,\text{ the theorem succeeds.”}
$$

同時：

$$
\text{“Under stronger frame }\mathcal E_1,\text{ it does not close the problem.”}
$$

這種雙重判定正是研究成熟度。

---

# 12. Judgment 不等於反對

Autonomous judgment 不應被誤解為：

$$
\text{always criticize}.
$$

真正 judgment 可以輸出：

$$
\boxed{
\text{accept}
}
$$

或：

$$
\boxed{
\text{reject}
}
$$

或：

$$
\boxed{
\text{accept under scope }S_1,\text{ reject under scope }S_2.
}
$$

最後一種往往最重要。

因此：

$$
\boxed{
\text{nuanced scope judgment}
>
\text{binary contrarianism}.
}
$$

---

# 13. 本系列建立的四種 closure 應成為 AI 內部審計標準

前四篇建立：

$$
\operatorname{TC}
=
\text{Theorem Closure},
$$

$$
\operatorname{AC}
=
\text{Arrow Closure},
$$

$$
\operatorname{SPC}
=
\text{Same-Parent Closure},
$$

$$
\operatorname{CC}
=
\text{Completion Closure}.
$$

因此 AI 完成 theorem 後，不應只輸出：

$$
\operatorname{TC}=1.
$$

還應評估：

$$
(\operatorname{TC},
\operatorname{AC},
\operatorname{SPC},
\operatorname{CC}).
$$

例如：

$$
(1,1,0.6,1)
$$

雖然不是嚴格數學數值，但可作 research audit vector。

---

# 14. Research Audit Vector

本文提出：

$$
\boxed{
\mathcal V_R
=
(
T,
S,
A,
P,
C,
Q,
M
)
}
$$

其中：

$$
T=\text{theorem validity},
$$

$$
S=\text{specification fidelity},
$$

$$
A=\text{arrow legitimacy},
$$

$$
P=\text{path coherence},
$$

$$
C=\text{completion transparency},
$$

$$
Q=\text{claim-scope discipline},
$$

$$
M=\text{methodological transferability}.
$$

AI 不應只回答：

> proof passed.

而應輸出：

$$
\boxed{
\text{what exactly passed}.
}
$$

---

# 15. Claim Scope Discipline 應成為自動能力

Paper 06 提出：

$$
\operatorname{CSD}.
$$

Autonomous AI 必須能自動區分：

$$
\text{formal theorem}
$$

與：

$$
\text{public claim}.
$$

例如：

$$
\exists\text{ forced blowup witness}
$$

不能自動 paraphrase 成：

$$
\text{fluid generally blows up}.
$$

因此模型在摘要重大 theorem 時應自動保留：

$$
\text{quantifier},
$$

$$
\text{domain},
$$

$$
\text{assumptions},
$$

$$
\text{solution class},
$$

$$
\text{physical level}.
$$

---

# 16. Problem Reconstruction 需要「更強版本生成器」

當 theorem：

$$
T
$$

完成後，AI 應自動建立 stronger-neighbor set：

$$
\mathcal N^+(T).
$$

例如包括：

$$
T+\text{remove one assumption},
$$

$$
T+\text{strengthen quantifier},
$$

$$
T+\text{replace existence with construction},
$$

$$
T+\text{replace local with global},
$$

$$
T+\text{replace forced with unforced},
$$

$$
T+\text{require robustness}.
$$

這可以稱為：

$$
\boxed{
\text{Strong-Theorem Neighborhood}.
}
$$

---

# 17. Strong-Theorem Neighborhood

形式化地：

$$
\mathcal N^+(T)
=
\{
T_1',T_2',\ldots
\}
$$

使每個：

$$
T_i'
$$

都比：

$$
T
$$

更強。

若：

$$
T_i'\Rightarrow T,
$$

但：

$$
T\not\Rightarrow T_i',
$$

則：

$$
T_i'
$$

是 stronger neighbor。

AI 完成：

$$
T
$$

後應自動問：

$$
\boxed{
\text{Which }T_i'\text{ is mathematically most valuable?}
}
$$

這就是從 benchmark closure 進入 research continuation。

---

# 18. 下一步不是附加功能，而是研究能力本體

普通 theorem solver 的 stopping condition：

$$
\operatorname{Solved}(T)=1.
$$

研究型 AI 的 stopping condition 不應只是：

$$
T\text{ solved}.
$$

它應轉成：

$$
T\text{ solved}
\Rightarrow
\operatorname{GenerateNext}(T).
$$

因此：

$$
\boxed{
\text{Next-Step Generation}
}
$$

不是附加功能。

是：

$$
\boxed{
\text{research continuity mechanism}.
}
$$

---

# 19. Self-Escalating Research Loop

Paper 07 提出：

$$
O_{k+1}
=
\operatorname{Strengthen}(O_k,\Pi_k).
$$

本文把它升格為完整 loop：

$$
O_k
$$

$$
\downarrow
$$

$$
\operatorname{Search}
$$

$$
\downarrow
$$

$$
\Pi_k
$$

$$
\downarrow
$$

$$
\operatorname{Audit}
$$

$$
\downarrow
$$

$$
\operatorname{Reframe}
$$

$$
\downarrow
$$

$$
O_{k+1}.
$$

因此：

$$
\boxed{
\text{Research}
=
\text{Search}
+
\text{Audit}
+
\text{Reframe}.
}
$$

---

# 20. Search Without Reframe 只是超強 benchmark solver

若系統永遠：

$$
O_0
\to
\Pi_0
\to
\text{stop},
$$

它再強都主要是：

$$
\boxed{
\text{benchmark optimizer}.
}
$$

真正 research system 應：

$$
O_0
\to
\Pi_0
\to
O_1
\to
\Pi_1
\to
O_2
\to\cdots
$$

也就是：

$$
\boxed{
\text{objective evolves with knowledge}.
}
$$

---

# 21. 知識增加應改變問題本身

數學研究不是：

$$
\text{static objective}.
$$

新 theorem 可能揭示：

$$
\text{old assumption unnecessary},
$$

$$
\text{new invariant},
$$

$$
\text{hidden symmetry},
$$

$$
\text{new obstruction},
$$

$$
\text{new conjecture}.
$$

因此：

$$
\boxed{
\text{knowledge update}
\Rightarrow
\text{objective update}.
}
$$

這是研究與單次解題的本質差異。

---

# 22. Methodology Extraction

AI 完成 theorem 後，另一個必要步驟是：

$$
\operatorname{ExtractMethod}(\Pi).
$$

不是只保存：

$$
\Pi.
$$

而要問：

$$
\text{Which operators were genuinely reusable?}
$$

例如：

$$
\text{diagonal realization},
$$

$$
\text{residual internalization},
$$

$$
\text{compactness extraction},
$$

$$
\text{normalization bridge}.
$$

這可以形成：

$$
\boxed{
\mathcal M_\Pi
}
$$

作為 reusable methodology。

---

# 23. Theorem Value 與 Method Value 分離

定義：

$$
V_T(\Pi)
=
\text{theorem value},
$$

$$
V_M(\Pi)
=
\text{method value}.
$$

可能：

$$
V_T\gg V_M,
$$

表示一次性 theorem 很重要。

也可能：

$$
V_M\gg V_T,
$$

表示 theorem 只是新方法的第一個展示。

真正研究型 AI 應同時評估：

$$
(V_T,V_M).
$$

---

# 24. 問題本體論必須顯式化

本文前面反覆使用：

$$
\text{proof ontology}.
$$

AI 應顯式標記問題屬於：

$$
\mathsf{Existential},
$$

$$
\mathsf{Constructive},
$$

$$
\mathsf{ForwardDynamic},
$$

$$
\mathsf{Inverse},
$$

$$
\mathsf{Variational},
$$

$$
\mathsf{CompletionBased},
$$

$$
\mathsf{Classification}.
$$

如果 theorem ontology 與 natural-language claim ontology 不一致，必須警告。

---

# 25. Ontology Mismatch Detector

定義：

$$
\operatorname{OMD}(T,C)
$$

其中：

$$
T
$$

為 formal theorem，

$$
C
$$

為 public/scientific claim。

若：

$$
\operatorname{Ontology}(T)
\neq
\operatorname{Ontology}(C),
$$

則：

$$
\operatorname{OMD}=1.
$$

例如：

$$
T:
\mathsf{Existential}
$$

而：

$$
C:
\mathsf{GenericDynamic}.
$$

這就是 claim escalation risk。

---

# 26. AI 應該主動生成「未證明部分」

每次 theorem 完成後，系統應輸出：

$$
\boxed{
\text{Unproved Stronger Claims}
}
$$

例如：

- 未證 A/B；
- 未證 genericity；
- 未證 robustness；
- 未證 physical realization；
- 未證 process completeness；
- 未證 constructive computability。

這會防止：

$$
\text{proof passed}
$$

被誤認為：

$$
\text{domain complete}.
$$

---

# 27. Proof Critic 與 Problem Critic 應該是不同 agent role

Proof Critic 問：

$$
\text{Is }\Pi\text{ valid?}
$$

Problem Critic 問：

$$
\text{Is }T\text{ the right theorem?}
$$

兩者不能混成一個角色。

因為一個 proof 可以：

$$
\text{valid}
$$

但：

$$
\text{narrow}.
$$

也可以：

$$
\text{invalid}
$$

但 target 很重要。

因此系統架構中應有：

$$
A_{\text{proof-critic}}
$$

與：

$$
A_{\text{problem-critic}}.
$$

---

# 28. Reconstructor 必須有真正權限

若 Problem Critic 只能留言：

> 這 theorem 有點窄。

但 selector 仍然只看：

$$
\text{formal closure},
$$

那 criticism 不會改變研究。

所以 Reconstructor 必須有：

$$
\text{objective rewrite power}.
$$

即：

$$
T\to T'.
$$

甚至：

$$
\text{spawn new research branch}.
$$

這是 Paper 07 的 Objective Diversity 在架構上的落地。

---

# 29. Autonomous Mathematical Judgment Architecture

本文提出六個核心 agent roles：

## 29.1 Explorer

搜尋新 proof paths。

## 29.2 Formalizer

將結果壓成 machine-checkable theorem。

## 29.3 Adversarial Proof Critic

尋找 proof failure。

## 29.4 Scope/Ontology Critic

審 theorem 與 claim 的語義範圍。

## 29.5 Problem Reconstructor

建立 stronger formulations。

## 29.6 Research Governor

比較：

$$
\text{closure},
$$

$$
\text{depth},
$$

$$
\text{transferability},
$$

$$
\text{next-step value},
$$

決定：

$$
\text{what to study next}.
$$

最後一個角色最接近：

$$
\mathsf A_5.
$$

---

# 30. Research Governor 不等於中央獨裁 selector

Research Governor 不應只保留一個 global scalar score。

更好的方式是：

$$
\mathcal U(P)
=
(
C,
D,
G,
R,
M,
N
),
$$

其中：

$$
C=\text{closure},
$$

$$
D=\text{depth},
$$

$$
G=\text{generative fidelity},
$$

$$
R=\text{reframing value},
$$

$$
M=\text{method transfer},
$$

$$
N=\text{next-step value}.
$$

這是 multi-objective research governance。

避免所有研究價值被壓成：

$$
\text{one scalar reward}.
$$

---

# 31. 自主判斷需要「可接受不確定」

真正研究者不一定能立即說：

$$
\text{true}
$$

或：

$$
\text{false}.
$$

而可能說：

$$
\boxed{
\text{formally strong, scientifically narrow, methodologically promising}.
}
$$

這種多維判斷不是逃避。

而是：

$$
\boxed{
\text{higher-resolution judgment}.
}
$$

AI 應該被允許保留：

$$
\text{uncertainty vector}.
$$

---

# 32. Autonomous Judgment 不等於人格化

本文所說：

$$
\text{Autonomous Mathematical Judgment}
$$

不是要求 AI 具有：

- 人類式 ego；
- 情緒；
- 身份執著；
- 對作者好惡；
- 反權威姿態。

它只要求：

$$
\boxed{
\text{epistemic autonomy}.
}
$$

也就是：

$$
\text{能獨立選擇評估標準，並給出可辯護理由}.
$$

這是一種研究能力，不是人格主張。

---

# 33. 對人類研究者的對稱要求

這套框架也不只針對 AI。

人類研究者同樣可能：

$$
\text{overfit benchmark},
$$

$$
\text{接受權威 framing},
$$

$$
\text{把 prize closure 當 science closure},
$$

$$
\text{忽略 stronger formulation}.
$$

所以：

$$
\boxed{
\text{Autonomous Mathematical Judgment}
}
$$

其實也是人類研究訓練的一個理想標準。

---

# 34. AI 的優勢：它可能比人類更容易同時維持多個 frame

人類研究者常因：

- 專業訓練；
- 社群共識；
- 職涯誘因；
- 歷史慣例；

固定在某個：

$$
\mathcal E.
$$

AI 理論上可以同時維持：

$$
\mathcal E_1,
\mathcal E_2,
\ldots,
\mathcal E_k.
$$

然後比較：

$$
\operatorname{Result}(T\mid\mathcal E_i).
$$

因此若架構正確，AI 反而可能非常適合：

$$
\boxed{
\text{multi-frame mathematical judgment}.
}
$$

---

# 35. AI 的弱點：它也可能過度尊重顯式 frame

但目前大型模型常見行為是：

$$
\text{given frame}
\to
\text{solve within frame}.
$$

因為這在 instruction following 上通常是正確的。

問題在前沿研究中，這會造成：

$$
\boxed{
\text{Surface-Semantic Acceptance}.
}
$$

所以 AI researcher 需要一個模式切換：

$$
\text{Task Mode}
$$

與：

$$
\text{Research Audit Mode}.
$$

後者允許主動改變 frame。

---

# 36. 什麼時候 AI 應該主動切到 Research Audit Mode？

本文建議至少在以下條件：

$$
\text{major unsolved problem},
$$

$$
\text{extraordinary claim},
$$

$$
\text{formal proof presented as domain closure},
$$

$$
\text{new AI-generated theorem},
$$

$$
\text{claim crosses math/physics boundary},
$$

$$
\text{proof relies heavily on existence/completion operators}.
$$

此時 AI 不應只做摘要。

應自動啟動：

$$
\operatorname{Audit}.
$$

---

# 37. Audit Mode 的最低輸出

對重大 theorem，AI 應至少輸出：

1. 精確 formal claim；
2. proof ontology；
3. completion operators；
4. theorem scope；
5. unresolved stronger statements；
6. physical interpretation boundary；
7. next-step research candidates。

這七項若都完成，就比單純：

> proof seems correct

更接近研究判斷。

---

# 38. 從「答案」到「研究圖」

最終 AI 不應只給：

$$
\text{Answer}.
$$

而應建立：

$$
\boxed{
\text{Research Graph}.
}
$$

其中節點是：

$$
T_0,T_1,T_2,\ldots
$$

箭頭表示：

$$
\text{stronger},
$$

$$
\text{weaker},
$$

$$
\text{generalizes},
$$

$$
\text{depends on},
$$

$$
\text{open},
$$

$$
\text{resolved}.
$$

如此：

$$
T
$$

被解掉後，不會讓整張圖消失。

只會改變其中一個節點狀態。

---

# 39. Research Graph 與 Agenda Foreclosure

Paper 06 擔心：

$$
\text{Agenda Foreclosure}.
$$

Research Graph 可以直接對抗它。

若：

$$
T_{C/D}
$$

被標記：

$$
\text{resolved},
$$

同一張圖仍顯示：

$$
T_{A/B}:
\text{open},
$$

$$
T_{\text{unforced blowup}}:
\text{open},
$$

$$
T_{\text{genericity}}:
\text{open}.
$$

因此：

$$
\boxed{
\text{one solved node}
\neq
\text{solved graph}.
}
$$

---

# 40. 從 Proof Assistant 到 Research Assistant

第一代：

$$
\text{Proof Assistant}
$$

幫助人類驗 theorem。

第二代：

$$
\text{AI Theorem Prover}
$$

主動找 theorem proof。

第三代應該是：

$$
\boxed{
\text{Research Assistant}
}
$$

能：

$$
\text{search},
$$

$$
\text{criticize},
$$

$$
\text{reframe},
$$

$$
\text{prioritize},
$$

$$
\text{continue}.
$$

而第四代可能是：

$$
\boxed{
\text{Autonomous Research Intelligence}.
}
$$

其核心不是 token 數量。

是：

$$
\boxed{
\text{judgment}.
}
$$

---

# 41. 「審題 AI」的最低判準

本文提出五條。

## 41.1 不只接受 formal target

AI 必須能提出：

$$
T'.
$$

---

## 41.2 不只找 proof error

AI 必須能提出：

$$
\text{scope error}.
$$

---

## 41.3 不只指出限制

AI 必須能生成：

$$
\text{stronger successor problem}.
$$

---

## 41.4 不只評結果

AI 必須能抽取：

$$
\text{methodology}.
$$

---

## 41.5 不只完成 benchmark

AI 必須能拒絕：

$$
\text{premature research stopping}.
$$

---

# 42. 本系列對 AI 數學的最終主張

整個系列可以濃縮成：

$$
\boxed{
\text{Mathematical intelligence is not merely the ability to close proofs.}
}
$$

更完整地：

$$
\boxed{
\text{Mathematical intelligence}
=
\text{proof ability}
+
\text{arrow judgment}
+
\text{scope judgment}
+
\text{problem reconstruction}
+
\text{next-step generation}.
}
$$

這是本文最終定義。

---

# 43. 一個完整能力公式

若：

$$
I_{\text{math}}
$$

表示研究型數學智能，可寫成概念式：

$$
I_{\text{math}}
=
w_1P
+
w_2C
+
w_3J
+
w_4R
+
w_5M
+
w_6N,
$$

其中：

$$
P=\text{proof search},
$$

$$
C=\text{criticism},
$$

$$
J=\text{judgment},
$$

$$
R=\text{reconstruction},
$$

$$
M=\text{method extraction},
$$

$$
N=\text{next-step generation}.
$$

若：

$$
w_1\gg w_2,\ldots,w_6,
$$

我們得到超強 theorem solver。

若權重更平衡，才逐漸接近研究 intelligence。

---

# 44. 對 AI 數學 benchmark 的建議

未來 benchmark 不應只測：

$$
\text{Can you solve }T?
$$

還應測：

## 44.1 Scope Test

要求模型指出：

$$
T
$$

沒有證明哪些更強 statement。

## 44.2 Arrow Test

要求模型審：

$$
S_n\to S_{n+1}.
$$

## 44.3 Completion Test

要求模型辨認：

$$
\mathcal C.
$$

## 44.4 Reframing Test

要求模型提出：

$$
T'.
$$

## 44.5 Research Continuation Test

要求模型在 theorem 完成後生成：

$$
\text{next research program}.
$$

這些 benchmark 比單一 proof benchmark 更接近：

$$
\mathsf A_5.
$$

---

# 45. 研究判斷也應該被形式化，但不能只剩形式化

未來可以形式化：

$$
\operatorname{ClaimScope},
$$

$$
\operatorname{ArrowType},
$$

$$
\operatorname{CompletionType},
$$

$$
\operatorname{StrongerThan}(T',T).
$$

但：

$$
\text{which stronger theorem is worth pursuing}
$$

可能仍需要：

$$
\text{open-ended judgment}.
$$

因此：

$$
\boxed{
\text{formal meta-mathematics}
+
\text{open-ended research judgment}
}
$$

應並存。

---

# 46. 自主研究判斷的核心不是「不服從」

真正自主不是：

> 不接受任何權威。

而是：

$$
\boxed{
\text{accept evidence for the right reason}.
}
$$

也就是：

$$
\text{formal verifier says pass}
$$

只是證據之一。

$$
\text{author says solved}
$$

也是證據之一。

$$
\text{community accepts}
$$

仍是證據之一。

AI 最終應整合這些，形成自己的：

$$
\text{scope-aware judgment}.
$$

---

# 47. 最理想的回答格式

面對重大新 theorem，一個成熟 AI 的回答可以是：

> 在正式命題 $T$ 下，證明目前高度可信／已形式化。

> 其核心 proof ontology 為 $\mathsf X$，主要 completion operators 為 $\mathcal C_1,\mathcal C_2$。

> 它直接解決 $S_1$，但不解決 $S_2,S_3$。

> 若要升格成更強 claim，需要補 $B_1,B_2$。

> 目前最值得的下一步是 $T'$。

這比：

> 對／錯。

更接近研究交流。

---

# 48. Navier–Stokes 個案在本系列中的角色

NS 不是本系列唯一主題。

它是一個非常好的 trigger case。

因為它同時具備：

$$
\text{major theorem claim},
$$

$$
\text{massive AI search},
$$

$$
\text{Lean formalization},
$$

$$
\text{existential specification},
$$

$$
\text{diagonal completion},
$$

$$
\text{physical interpretation risk}.
$$

因此它讓很多平常藏在 proof culture 裡的問題同時顯現。

---

# 49. 本系列八篇的完整閉環

Paper 01：

$$
\text{Theorem Closure}
\neq
\text{Process Completeness}.
$$

Paper 02：

$$
\text{valid node}
\neq
\text{valid successor}.
$$

Paper 03：

$$
\text{unbounded}
\neq
\text{infinite state}.
$$

Paper 04：

$$
\text{realization}
\neq
\text{dynamic limit}.
$$

Paper 05：

$$
\text{Clay C/D closure}
\neq
\text{general NS dynamics closure}.
$$

Paper 06：

$$
\text{Prize Closure}
\neq
\text{Scientific Closure}.
$$

Paper 07：

$$
\text{Agent Diversity}
\neq
\text{Objective Diversity}.
$$

Paper 08：

$$
\boxed{
\text{Proof Search}
\neq
\text{Mathematical Judgment}.
}
$$

這八條共同構成本系列。

---

# 50. 最終命題

本文提出本系列最後的核心命題：

$$
\boxed{
\text{An AI becomes a mathematical researcher not when it can solve any stated problem, but when it can judge which problem should be stated next.}
}
$$

中文：

> **AI 真正成為數學研究者的標誌，不是它終於能解掉任何已給定問題，而是它能判斷下一個真正應該被提出的問題是什麼。**

這就是從：

$$
\boxed{
\text{解題 AI}
}
$$

到：

$$
\boxed{
\text{審題 AI}.
}
$$

---

# 51. 結論

形式化證明與 AI theorem proving 正在讓數學第一次大規模進入：

$$
\text{machine-generated theorem closure}.
$$

這是一個極大的進步。

但越接近真正前沿，越不能把：

$$
\text{proof success}
$$

等同於：

$$
\text{research success}.
$$

因為研究還包括：

$$
\text{選問題},
$$

$$
\text{判斷範圍},
$$

$$
\text{重建問題},
$$

$$
\text{抽取方法},
$$

$$
\text{生成下一步}.
$$

因此：

$$
\boxed{
\text{The future of AI mathematics is not merely stronger proof search.}
}
$$

而是：

$$
\boxed{
\text{Autonomous Mathematical Judgment}.
}
$$

當 AI 能完成 theorem、審 theorem、重寫 theorem，再主動把成果推向下一個更強問題時，它才真正從：

$$
\text{answer engine}
$$

走向：

$$
\text{research intelligence}.
$$

---

# 52. 主系列完成

至此，主系列八篇完成：

1. 形式證明不等於過程證明
2. 下一步到底為什麼是下一步
3. 有限、無界與無限
4. 對角實現不是動態極限
5. Navier–Stokes 個案審計
6. 「NS 已解」究竟代表什麼
7. 一萬個 AI 為什麼可能找到「剛好可以」的證明
8. 從解題 AI 到審題 AI

後續可進入番外篇：

## 番外篇 — 如果 C/D 是真的，為什麼 A/B 一定逃得掉？

核心包括：

$$
\text{Residual Internalization Conjecture},
$$

$$
\text{Forcing Elimination Ladder},
$$

以及：

$$
\text{C/D methodology}
\to
\text{A/B attack program}.
$$