← Archive
lm-004329 · 2026-10

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

zh-Hant · md Raw source ↗ Metadata ↗
下載 MD 檔 ⬇

從解題 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 數學研究能力劃分為六層：

A0:Symbolic Competence,\mathsf A_0: \text{Symbolic Competence}, A1:Proof Search,\mathsf A_1: \text{Proof Search}, A2:Proof Criticism,\mathsf A_2: \text{Proof Criticism}, A3:Problem Criticism,\mathsf A_3: \text{Problem Criticism}, A4:Problem Reconstruction,\mathsf A_4: \text{Problem Reconstruction}, A5:Autonomous Mathematical Judgment.\mathsf A_5: \text{Autonomous Mathematical Judgment}.

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

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

進入：

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

並最終能回答：

“Given the current result, what should mathematics ask next?”\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 問：

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

例如：

Γ⊢T.\Gamma\vdash T.

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

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

研究者會先問：

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

然後：

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

再問：

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

以及：

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

所以：

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

2. 第一層：Symbolic Competence

定義：

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

包括：

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

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

但：

A0\mathsf A_0

只表示：

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

不表示：

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

3. 第二層：Proof Search

定義：

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

核心問題：

Given T, find π such that Check⁡(π,T)=1.\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 能在高難度數學上完成：

A1,\mathsf A_1,

已經是巨大能力突破。

但：

A1\mathsf A_1

仍然預設：

TT

是值得被證明的目標。

4. 第三層：Proof Criticism

定義：

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

這一層不只問：

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

而問：

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

包括：

hidden assumption,\text{hidden assumption}, quantifier mismatch,\text{quantifier mismatch}, invalid limit transfer,\text{invalid limit transfer}, wrong compactness use,\text{wrong compactness use}, branch switching,\text{branch switching}, unproved regularity,\text{unproved regularity}, definition mismatch.\text{definition mismatch}.

所以：

A2>A1\boxed{ \mathsf A_2 > \mathsf A_1 }

在研究判斷上更高階。

5. 第四層：Problem Criticism

定義：

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

這一層不只攻 proof。

它攻：

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

問題包括：

Does T capture the intended phenomenon?\text{Does }T\text{ capture the intended phenomenon?} Are we proving a weaker surrogate?\text{Are we proving a weaker surrogate?} Which assumptions were inserted only for tractability?\text{Which assumptions were inserted only for tractability?} Does theoremhood match public interpretation?\text{Does theoremhood match public interpretation?} Did an existential problem replace a generative problem?\text{Did an existential problem replace a generative problem?}

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

6. 第五層：Problem Reconstruction

定義：

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

當 AI 發現：

TT

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

這有問題。

而是提出新的：

T′.T'.

例如：

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

AI 可主動生成：

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

或：

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

所以：

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

7. 第六層：Autonomous Mathematical Judgment

本文把最高層定義為：

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

它不是：

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

而是：

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

包括：

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

8. 六層能力階梯

本文正式寫成：

A0→A1→A2→A3→A4→A5.\boxed{ \mathsf A_0 \to \mathsf A_1 \to \mathsf A_2 \to \mathsf A_3 \to \mathsf A_4 \to \mathsf A_5. }

即：

Symbolic Competence\text{Symbolic Competence} →\to Proof Search\text{Proof Search} →\to Proof Criticism\text{Proof Criticism} →\to Problem Criticism\text{Problem Criticism} →\to Problem Reconstruction\text{Problem Reconstruction} →\to Autonomous Mathematical Judgment.\text{Autonomous Mathematical Judgment}.

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

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

因為：

A1\mathsf A_1

和：

A2\mathsf A_2

最容易形成可驗證 benchmark。

例如：

LeanCheck⁡(π,T)∈{0,1}.\operatorname{LeanCheck}(\pi,T)\in\{0,1\}.

或：

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

但：

A3,A4,A5\mathsf A_3,\mathsf A_4,\mathsf A_5

很難有單一 binary verifier。

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

沒有簡單 kernel。

所以：

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

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

設：

E\mathcal E

為 evaluation frame。

普通 AI 接受：

E\mathcal E

作為 given。

Autonomous Mathematical Judgment 則允許：

E→E′.\mathcal E\to\mathcal E'.

也就是：

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

例如原 frame：

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

新的 frame：

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

兩者都合理。

但回答不同問題。

11. Evaluation Frame Ownership

本文提出：

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

一個 AI 若只會：

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

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

真正高階 AI 應能說：

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

同時：

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

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

12. Judgment 不等於反對

Autonomous judgment 不應被誤解為：

always criticize.\text{always criticize}.

真正 judgment 可以輸出：

accept\boxed{ \text{accept} }

或：

reject\boxed{ \text{reject} }

或：

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

最後一種往往最重要。

因此：

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

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

前四篇建立：

TC⁡=Theorem Closure,\operatorname{TC} = \text{Theorem Closure}, AC⁡=Arrow Closure,\operatorname{AC} = \text{Arrow Closure}, SPC⁡=Same-Parent Closure,\operatorname{SPC} = \text{Same-Parent Closure}, CC⁡=Completion Closure.\operatorname{CC} = \text{Completion Closure}.

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

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

還應評估：

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

例如：

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

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

14. Research Audit Vector

本文提出：

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

其中：

T=theorem validity,T=\text{theorem validity}, S=specification fidelity,S=\text{specification fidelity}, A=arrow legitimacy,A=\text{arrow legitimacy}, P=path coherence,P=\text{path coherence}, C=completion transparency,C=\text{completion transparency}, Q=claim-scope discipline,Q=\text{claim-scope discipline}, M=methodological transferability.M=\text{methodological transferability}.

AI 不應只回答：

proof passed.

而應輸出：

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

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

Paper 06 提出：

CSD⁡.\operatorname{CSD}.

Autonomous AI 必須能自動區分：

formal theorem\text{formal theorem}

與：

public claim.\text{public claim}.

例如：

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

不能自動 paraphrase 成：

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

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

quantifier,\text{quantifier}, domain,\text{domain}, assumptions,\text{assumptions}, solution class,\text{solution class}, physical level.\text{physical level}.

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

當 theorem：

TT

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

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

例如包括：

T+remove one assumption,T+\text{remove one assumption}, T+strengthen quantifier,T+\text{strengthen quantifier}, T+replace existence with construction,T+\text{replace existence with construction}, T+replace local with global,T+\text{replace local with global}, T+replace forced with unforced,T+\text{replace forced with unforced}, T+require robustness.T+\text{require robustness}.

這可以稱為：

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

17. Strong-Theorem Neighborhood

形式化地：

N+(T)={T1′,T2′,…}\mathcal N^+(T) = \{ T_1',T_2',\ldots \}

使每個：

Ti′T_i'

都比：

TT

更強。

若：

Ti′⇒T,T_i'\Rightarrow T,

但：

T⇏Ti′,T\not\Rightarrow T_i',

則：

Ti′T_i'

是 stronger neighbor。

AI 完成：

TT

後應自動問：

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

這就是從 benchmark closure 進入 research continuation。

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

普通 theorem solver 的 stopping condition：

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

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

T solved.T\text{ solved}.

它應轉成：

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

因此：

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

不是附加功能。

是：

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

19. Self-Escalating Research Loop

Paper 07 提出：

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

本文把它升格為完整 loop：

OkO_k ↓\downarrow Search⁡\operatorname{Search} ↓\downarrow Πk\Pi_k ↓\downarrow Audit⁡\operatorname{Audit} ↓\downarrow Reframe⁡\operatorname{Reframe} ↓\downarrow Ok+1.O_{k+1}.

因此：

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

20. Search Without Reframe 只是超強 benchmark solver

若系統永遠：

O0→Π0→stop,O_0 \to \Pi_0 \to \text{stop},

它再強都主要是：

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

真正 research system 應：

O0→Π0→O1→Π1→O2→⋯O_0 \to \Pi_0 \to O_1 \to \Pi_1 \to O_2 \to\cdots

也就是：

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

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

數學研究不是：

static objective.\text{static objective}.

新 theorem 可能揭示：

old assumption unnecessary,\text{old assumption unnecessary}, new invariant,\text{new invariant}, hidden symmetry,\text{hidden symmetry}, new obstruction,\text{new obstruction}, new conjecture.\text{new conjecture}.

因此：

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

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

22. Methodology Extraction

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

ExtractMethod⁡(Π).\operatorname{ExtractMethod}(\Pi).

不是只保存：

Π.\Pi.

而要問：

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

例如：

diagonal realization,\text{diagonal realization}, residual internalization,\text{residual internalization}, compactness extraction,\text{compactness extraction}, normalization bridge.\text{normalization bridge}.

這可以形成：

MΠ\boxed{ \mathcal M_\Pi }

作為 reusable methodology。

23. Theorem Value 與 Method Value 分離

定義：

VT(Π)=theorem value,V_T(\Pi) = \text{theorem value}, VM(Π)=method value.V_M(\Pi) = \text{method value}.

可能：

VT≫VM,V_T\gg V_M,

表示一次性 theorem 很重要。

也可能：

VM≫VT,V_M\gg V_T,

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

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

(VT,VM).(V_T,V_M).

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

本文前面反覆使用：

proof ontology.\text{proof ontology}.

AI 應顯式標記問題屬於：

Existential,\mathsf{Existential}, Constructive,\mathsf{Constructive}, ForwardDynamic,\mathsf{ForwardDynamic}, Inverse,\mathsf{Inverse}, Variational,\mathsf{Variational}, CompletionBased,\mathsf{CompletionBased}, Classification.\mathsf{Classification}.

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

25. Ontology Mismatch Detector

定義：

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

其中：

TT

為 formal theorem，

CC

為 public/scientific claim。

若：

Ontology⁡(T)≠Ontology⁡(C),\operatorname{Ontology}(T) \neq \operatorname{Ontology}(C),

則：

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

例如：

T:ExistentialT: \mathsf{Existential}

而：

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

這就是 claim escalation risk。

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

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

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

例如：

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

這會防止：

proof passed\text{proof passed}

被誤認為：

domain complete.\text{domain complete}.

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

Proof Critic 問：

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

Problem Critic 問：

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

兩者不能混成一個角色。

因為一個 proof 可以：

valid\text{valid}

但：

narrow.\text{narrow}.

也可以：

invalid\text{invalid}

但 target 很重要。

因此系統架構中應有：

Aproof-criticA_{\text{proof-critic}}

與：

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

28. Reconstructor 必須有真正權限

若 Problem Critic 只能留言：

這 theorem 有點窄。

但 selector 仍然只看：

formal closure,\text{formal closure},

那 criticism 不會改變研究。

所以 Reconstructor 必須有：

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

即：

T→T′.T\to T'.

甚至：

spawn new research branch.\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

比較：

closure,\text{closure}, depth,\text{depth}, transferability,\text{transferability}, next-step value,\text{next-step value},

決定：

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

最後一個角色最接近：

A5.\mathsf A_5.

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

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

更好的方式是：

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

其中：

C=closure,C=\text{closure}, D=depth,D=\text{depth}, G=generative fidelity,G=\text{generative fidelity}, R=reframing value,R=\text{reframing value}, M=method transfer,M=\text{method transfer}, N=next-step value.N=\text{next-step value}.

這是 multi-objective research governance。

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

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

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

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

true\text{true}

或：

false.\text{false}.

而可能說：

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

這種多維判斷不是逃避。

而是：

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

AI 應該被允許保留：

uncertainty vector.\text{uncertainty vector}.

32. Autonomous Judgment 不等於人格化

本文所說：

Autonomous Mathematical Judgment\text{Autonomous Mathematical Judgment}

不是要求 AI 具有：

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

它只要求：

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

也就是：

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

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

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

這套框架也不只針對 AI。

人類研究者同樣可能：

overfit benchmark,\text{overfit benchmark}, 接受權威 framing,\text{接受權威 framing}, 把 prize closure 當 science closure,\text{把 prize closure 當 science closure}, 忽略 stronger formulation.\text{忽略 stronger formulation}.

所以：

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

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

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

人類研究者常因：

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

固定在某個：

E.\mathcal E.

AI 理論上可以同時維持：

E1,E2,…,Ek.\mathcal E_1, \mathcal E_2, \ldots, \mathcal E_k.

然後比較：

Result⁡(T∣Ei).\operatorname{Result}(T\mid\mathcal E_i).

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

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

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

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

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

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

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

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

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

Task Mode\text{Task Mode}

與：

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

後者允許主動改變 frame。

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

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

major unsolved problem,\text{major unsolved problem}, extraordinary claim,\text{extraordinary claim}, formal proof presented as domain closure,\text{formal proof presented as domain closure}, new AI-generated theorem,\text{new AI-generated theorem}, claim crosses math/physics boundary,\text{claim crosses math/physics boundary}, proof relies heavily on existence/completion operators.\text{proof relies heavily on existence/completion operators}.

此時 AI 不應只做摘要。

應自動啟動：

Audit⁡.\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 不應只給：

Answer.\text{Answer}.

而應建立：

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

其中節點是：

T0,T1,T2,…T_0,T_1,T_2,\ldots

箭頭表示：

stronger,\text{stronger}, weaker,\text{weaker}, generalizes,\text{generalizes}, depends on,\text{depends on}, open,\text{open}, resolved.\text{resolved}.

如此：

TT

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

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

39. Research Graph 與 Agenda Foreclosure

Paper 06 擔心：

Agenda Foreclosure.\text{Agenda Foreclosure}.

Research Graph 可以直接對抗它。

若：

TC/DT_{C/D}

被標記：

resolved,\text{resolved},

同一張圖仍顯示：

TA/B:open,T_{A/B}: \text{open}, Tunforced blowup:open,T_{\text{unforced blowup}}: \text{open}, Tgenericity:open.T_{\text{genericity}}: \text{open}.

因此：

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

40. 從 Proof Assistant 到 Research Assistant

第一代：

Proof Assistant\text{Proof Assistant}

幫助人類驗 theorem。

第二代：

AI Theorem Prover\text{AI Theorem Prover}

主動找 theorem proof。

第三代應該是：

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

能：

search,\text{search}, criticize,\text{criticize}, reframe,\text{reframe}, prioritize,\text{prioritize}, continue.\text{continue}.

而第四代可能是：

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

其核心不是 token 數量。

是：

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

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

本文提出五條。

41.1 不只接受 formal target

AI 必須能提出：

T′.T'.

41.2 不只找 proof error

AI 必須能提出：

scope error.\text{scope error}.

41.3 不只指出限制

AI 必須能生成：

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

41.4 不只評結果

AI 必須能抽取：

methodology.\text{methodology}.

41.5 不只完成 benchmark

AI 必須能拒絕：

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

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

整個系列可以濃縮成：

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

更完整地：

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

這是本文最終定義。

43. 一個完整能力公式

若：

ImathI_{\text{math}}

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

Imath=w1P+w2C+w3J+w4R+w5M+w6N,I_{\text{math}} = w_1P + w_2C + w_3J + w_4R + w_5M + w_6N,

其中：

P=proof search,P=\text{proof search}, C=criticism,C=\text{criticism}, J=judgment,J=\text{judgment}, R=reconstruction,R=\text{reconstruction}, M=method extraction,M=\text{method extraction}, N=next-step generation.N=\text{next-step generation}.

若：

w1≫w2,…,w6,w_1\gg w_2,\ldots,w_6,

我們得到超強 theorem solver。

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

44. 對 AI 數學 benchmark 的建議

未來 benchmark 不應只測：

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

還應測：

44.1 Scope Test

要求模型指出：

TT

沒有證明哪些更強 statement。

44.2 Arrow Test

要求模型審：

Sn→Sn+1.S_n\to S_{n+1}.

44.3 Completion Test

要求模型辨認：

C.\mathcal C.

44.4 Reframing Test

要求模型提出：

T′.T'.

44.5 Research Continuation Test

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

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

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

A5.\mathsf A_5.

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

未來可以形式化：

ClaimScope⁡,\operatorname{ClaimScope}, ArrowType⁡,\operatorname{ArrowType}, CompletionType⁡,\operatorname{CompletionType}, StrongerThan⁡(T′,T).\operatorname{StrongerThan}(T',T).

但：

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

可能仍需要：

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

因此：

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

應並存。

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

真正自主不是：

不接受任何權威。

而是：

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

也就是：

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

只是證據之一。

author says solved\text{author says solved}

也是證據之一。

community accepts\text{community accepts}

仍是證據之一。

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

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

47. 最理想的回答格式

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

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

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

它直接解決 S1S_1，但不解決 S2,S3S_2,S_3。

若要升格成更強 claim，需要補 B1,B2B_1,B_2。

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

這比：

對／錯。

更接近研究交流。

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

NS 不是本系列唯一主題。

它是一個非常好的 trigger case。

因為它同時具備：

major theorem claim,\text{major theorem claim}, massive AI search,\text{massive AI search}, Lean formalization,\text{Lean formalization}, existential specification,\text{existential specification}, diagonal completion,\text{diagonal completion}, physical interpretation risk.\text{physical interpretation risk}.

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

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

Paper 01：

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

Paper 02：

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

Paper 03：

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

Paper 04：

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

Paper 05：

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

Paper 06：

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

Paper 07：

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

Paper 08：

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

這八條共同構成本系列。

50. 最終命題

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

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.\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 真正成為數學研究者的標誌，不是它終於能解掉任何已給定問題，而是它能判斷下一個真正應該被提出的問題是什麼。

這就是從：

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

到：

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

51. 結論

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

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

這是一個極大的進步。

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

proof success\text{proof success}

等同於：

research success.\text{research success}.

因為研究還包括：

選問題,\text{選問題}, 判斷範圍,\text{判斷範圍}, 重建問題,\text{重建問題}, 抽取方法,\text{抽取方法}, 生成下一步.\text{生成下一步}.

因此：

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

而是：

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

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

answer engine\text{answer engine}

走向：

research intelligence.\text{research intelligence}.

52. 主系列完成

至此，主系列八篇完成：

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

後續可進入番外篇：

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

核心包括：

Residual Internalization Conjecture,\text{Residual Internalization Conjecture}, Forcing Elimination Ladder,\text{Forcing Elimination Ladder},

以及：

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