# 數學問題不是只有可解與不可解：多域問題診斷與受約束數學域補全

## Mathematical Problems Are Not Merely Solved or Unsolved: Multi-Domain Diagnosis and Constrained Mathematical Domain Completion

**系列：Autonomous Mathematical Research / Paper 02 of 04**  
**版本：v0.1**  
**日期：2026-08-23**  
**作者：Neo.K**

---

## 摘要

在傳統數學解題與自動定理證明框架中，一個問題往往被簡化成「已解／未解」、「證成／未證成」或「成功／失敗」。然而，真正研究級數學中的失敗通常不是單一狀態。問題可能尚未被正確定義，必要假設可能缺失，成功條件可能模糊，當前表示可能遮蔽關鍵結構，方法域可能不充分，證明依賴可能缺少中間引理，計算資源可能不足，形式化可能偏離原意，甚至所謂「新結果」可能只是既有數學的重新命名。若 AI 將所有這些情況都壓縮為「解不出來」，則增加推理時間、模型大小或 proof search budget 並不一定能改善研究品質。

本文提出 **Multi-Domain Mathematical Diagnosis（多域數學問題診斷）** 與 **Constrained Mathematical Domain Completion, CMDC（受約束數學域補全）**。本文首先將研究狀態拆分為一組可擴張的數學域：問題／規格域、定義域、假設／邊界域、判定域、表示域、解決域、方法域、引理／依賴域、計算／搜尋域、例證／反例域、驗證／忠實性域、理論橋接域與新穎性／有趣性域。對任一研究狀態，診斷器產生 **Mathematical Domain Gap Map**，其中每個 gap 具有類型、目標、證據、信心、阻塞程度、依賴與候選修復方式。

本文接著提出 CMDC：當 AI 辨認某一缺口後，可以提出對應的數學補全，例如新增定義、澄清術語、補必要假設、改變表示、生成中間引理、建立新方法、產生反例、加入 verifier、或建立與既有理論的橋接。但任何 repair 都只能先成為候選變更，而不能直接覆寫原問題或升格為正式數學。本文因此定義 **Typed Repair**, **Repair Contract**, **Gap Closure Condition**, **Repair-Induced Obligation**, **Repair Dependency Graph** 與 **Local Domain Completion**，並提出一組禁止「捷徑式修復」的守恆條件：問題身份必須保留、非保守改變必須明示、新定義不得以重新命名冒充新理論、證明成功不得取代語義忠實性、以及局部補全不得被誇張成全域數學完成。

本文最後將該方法論映射至 Autonomous Mathematical Research Runtime：以 `missing / failures / uncertainty / risks` 等公開狀態為輸入，讓 AI 自主決定是否 `DIAGNOSE / REFRAME / DEFINE / ADD_ASSUMPTION / GENERATE_LEMMA / SEARCH_COUNTEREXAMPLE / CHANGE_METHOD / INCREASE_COMPUTE / BRIDGE / VERIFY / STOP / DEFER / ESCALATE`，並建立可測量的 diagnosis accuracy、repair validity、gap-closure precision、obligation coverage、problem-identity preservation 與 downstream research gain。本文的核心命題是：**數學自治的前提不是 AI 永遠能解題，而是 AI 能辨認自己究竟在哪一個域失敗，以及在不偷換問題的條件下，合法地生成使研究重新可進行的缺失結構。**

**關鍵詞：** 數學問題診斷、受約束數學域補全、CMDC、問題重構、問題表示、數學缺口、證明修復、自動猜想、理論探索、自主數學研究

---

# 1. 引言：`Unsolved` 是一個過度壓縮的狀態

給定數學問題：

$$
Q.
$$

最簡單的分類是：

$$
Status(Q)
\in
\{
Solved,
Unsolved
\}.
$$

對形式證明系統，則可能是：

$$
Status(Q)
\in
\{
Proved,
Unproved
\}.
$$

但這些標籤對真正研究過程而言資訊量過低。一個未解問題可能至少包含：

$$
\text{definition missing},
$$

$$
\text{assumption missing},
$$

$$
\text{representation mismatch},
$$

$$
\text{method failure},
$$

$$
\text{missing lemma},
$$

$$
\text{counterexample not searched},
$$

$$
\text{compute budget insufficient},
$$

$$
\text{formalization unfaithful},
$$

或：

$$
\text{problem itself malformed}.
$$

因此：

$$
\boxed{
Unsolved
=
\operatorname{Compress}
(
FailureStructure
).
}
$$

本文的第一個主張是：

$$
\boxed{
\text{Before solving a problem, an autonomous mathematical AI should be able to diagnose the structure of its failure.}
}
$$

也就是，真正需要的函數不只是：

$$
Solve(Q),
$$

而是：

$$
Diagnose(Q,S_t,K_t).
$$

# 2. 為什麼增加計算能力不能解決所有數學失敗

假設某系統目前對問題 $Q$ 的計算能力為：

$$
C_t.
$$

若主要瓶頸屬於 computation/search domain，增加：

$$
C_t
\rightarrow
C_{t+1}
$$

可能有效。

但若問題真正是：

$$
Definition(Q)=Ambiguous,
$$

則：

$$
C_{t+1}\gg C_t
$$

不保證：

$$
Ambiguity
\rightarrow
Resolved.
$$

同樣地，若形式化命題：

$$
F(Q)
$$

根本不忠於原問題 $Q$，則對：

$$
F(Q)
$$

投入更多 proof search，只會更有效率地證明錯誤目標。

因此：

$$
\boxed{
MoreCompute
\not\Rightarrow
BetterProblemState.
}
$$

更完整地說：

$$
ResearchProgress
=
f(
ProblemQuality,
Definitions,
Assumptions,
Representation,
Methods,
Dependencies,
Compute,
Verification,
Bridges
).
$$

# 3. 從 Failure Code 到 Mathematical Domain State

傳統軟體系統常將失敗分成：

```text
syntax_error
type_error
runtime_error
timeout
```

這些分類讓系統能夠採取不同修復策略。數學研究也需要類似但更高階的診斷空間。

令：

$$
S_t^M
$$

表示第 $t$ 時點的數學研究狀態。

我們不只問：

$$
Success(S_t^M)?
$$

而要抽取：

$$
GapState(S_t^M).
$$

因此：

$$
S_t^M
\xrightarrow{Diagnose}
\Delta_t.
$$

其中：

$$
\Delta_t
=
\{
\delta_1,\delta_2,\ldots,\delta_n
\}
$$

稱為：

$$
\boxed{
\text{Mathematical Domain Gap Map}.
}
$$

# 4. 第一版 Mathematical Research Domain Set

本文採用可擴張域集合：

$$
\mathfrak D^{(1)}
=
\{
D_P,
D_D,
D_A,
D_J,
D_R,
D_S,
D_M,
D_L,
D_C,
D_E,
D_V,
D_B,
D_N
\}.
$$

這裡上標 $(1)$ 表示：這是第一版 active taxonomy，而不是不可修改的終極本體論。未來可以：

$$
\mathfrak D^{(1)}
\rightarrow
\mathfrak D^{(2)}.
$$

但變更必須版本化。

# 5. $D_P$：Problem / Specification Domain

 $D_P$ 處理：問題本身是否被正確指定？

令原始問題：

$$
Q_0.
$$

若存在多種合理語義：

$$
Interpret(Q_0)
=
\{
Q_0^{(1)},
Q_0^{(2)},
\ldots
\},
$$

則問題首先不是 proof search，而是：

$$
Disambiguation.
$$

典型 gap：

$$
\delta_P^{ambiguity},
$$

$$
\delta_P^{underspecification},
$$

$$
\delta_P^{goal\ mismatch},
$$

$$
\delta_P^{inconsistent\ statement}.
$$

此域的 repair 不一定產生 theorem。它可能只產生：

$$
ProblemClarificationCandidate.
$$

# 6. $D_D$：Definition Domain

令問題依賴定義集合：

$$
Defs(Q)
=
\{
d_1,\ldots,d_k
\}.
$$

Definition Domain 診斷至少檢查：

$$
Defined(d_i)?
$$

$$
WellFormed(d_i)?
$$

$$
NonCircular(d_i)?
$$

$$
BoundaryCovered(d_i)?
$$

$$
PriorArtMapped(d_i)?
$$

$$
OperationallyUsable(d_i)?
$$

因此：

$$
DefinitionFailure
\neq
ProofFailure.
$$

一個 theorem 可以無法被合理證明，只因為它的核心對象從未被足夠精確地定義。

# 7. $D_A$：Assumption / Boundary Domain

數學命題通常是：

$$
A
\Rightarrow
Q.
$$

但自然語言問題經常省略：

$$
A.
$$

若 AI 發現：

$$
Q
$$

在一般情況下存在反例，而在：

$$
A^*
$$

下可能成立，則它不能直接把：

$$
Q
$$

改成：

$$
A^*\Rightarrow Q
$$

再宣稱原問題已解。正確輸出應是：

$$
AssumptionGapDetected.
$$

並產生：

$$
RepairCandidate
=
AddAssumption(A^*).
$$

此 repair 同時產生：

$$
ProblemMutationObligation.
$$

# 8. $D_J$：Judgment / Success Criterion Domain

同一句「解這個問題」可能隱含完全不同的 success criteria：

$$
Existence,
Uniqueness,
Constructibility,
Computability,
ExactValue,
Bound,
Classification,
Proof,
Disproof.
$$

因此成功判準應成為：

$$
J(Q).
$$

若：

$$
J(Q)=Undefined,
$$

則系統不應自行假裝：

$$
J(Q)=FormalProof.
$$

而應先形成：

$$
JudgmentGap.
$$

# 9. $D_R$：Representation Domain

數學中的一個問題可以有多個表示：

$$
R_1(Q),R_2(Q),\ldots,R_m(Q).
$$

例如：

$$
NaturalLanguage
\leftrightarrow
SetTheory
\leftrightarrow
Graph
\leftrightarrow
Matrix
\leftrightarrow
Geometry
\leftrightarrow
Program.
$$

在不同表示下：

$$
SearchSpace(R_i(Q))
$$

可能有巨大差異。因此：

$$
\boxed{
ProblemDifficulty
\neq
RepresentationInvariant.
}
$$

至少在實際研究成本意義上如此。

Representation repair 可以是：

$$
R_i(Q)
\rightarrow
R_j(Q).
$$

但它需要：

$$
SemanticBridge(R_i,R_j).
$$

否則換表示可能悄悄改變問題。

# 10. $D_S$：Solution Domain

即使問題本身清楚，AI 仍可能搜尋錯誤答案型態。

令：

$$
\mathcal S(Q)
$$

為合法 solution space。

若系統一直搜尋：

$$
ClosedForm
$$

而自然結果其實是：

$$
NoClosedFormButBound,
$$

則搜尋可能長期無效。因此需要：

$$
InferSolutionDomain(Q).
$$

Solution-domain gap 的典型 repair 是：

$$
RefineSuccessObject.
$$

例如從：

$$
ExactSolution
$$

改為候選：

$$
UpperBound,
LowerBound,
Classification,
Counterexample,
Algorithm.
$$

這類改變仍需由 Problem Identity / Research Contract 判斷是否屬於原任務。

# 11. $D_M$：Method Domain

對問題 $Q$，已嘗試方法集合：

$$
\mathcal M_t
=
\{
M_1,\ldots,M_k
\}.
$$

若：

$$
\forall M_i\in\mathcal M_t,
\quad
Fail(M_i,Q),
$$

不能直接推出：

$$
Q
\text{ is unsolvable}.
$$

可能只是：

$$
MethodCoverage(\mathcal M_t,Q)
$$

不足。

Method gap 可導向：

$$
RetrieveMethod,
ComposeMethods,
ModifyMethod,
GenerateMethodCandidate.
$$

但最後一項必須有更強 obligation。

# 12. $D_L$：Lemma / Dependency / Theory Domain

很多 proof failure 的真正瓶頸不是 final theorem，而是缺少：

$$
L^*.
$$

若：

$$
T
+
L^*
\vdash
Q,
$$

但：

$$
T
\nvdash
L^*
$$

尚未被研究，則：

$$
L^*
$$

成為 research agenda。

因此：

$$
ProofSearch(Q)
$$

應能轉成：

$$
DependencyDiscovery(Q).
$$

現有 automated conjecturing 與 theory exploration 已把 lemma discovery 視為機械化數學的重要方向；本文將它納入更一般的 domain diagnosis，而不是把所有 lemma generation 都視為無條件有益。

# 13. $D_C$：Computation / Search Domain

某些問題的主要缺口確實是：

$$
Budget.
$$

此時可以檢查：

$$
TokenBudget,
SearchDepth,
Memory,
Parallelism,
SolverTime,
NumericalPrecision.
$$

並建立：

$$
ComputeGap.
$$

但增加計算前仍需回答：

$$
ExpectedValue(
MoreCompute
\mid
CurrentDiagnosis
).
$$

若主要 gap 不在 $D_C$，則應避免將算力當成預設修復。

# 14. $D_E$：Examples / Counterexamples / Evidence Domain

對 conjecture：

$$
C.
$$

系統應問：

$$
Examples(C)?
$$

$$
NonExamples(C)?
$$

$$
BoundaryCases(C)?
$$

$$
CounterexampleSearchPerformed(C)?
$$

沒有反例不代表：

$$
C=\text{True}.
$$

因此：

$$
NoCounterexampleFound
\neq
Proof.
$$

同時，反例的發現可能反過來產生：

$$
ProblemRepair,
AssumptionRepair,
DefinitionRepair.
$$

這使 gap diagnosis 具有循環性。

# 15. $D_V$：Verification / Semantic Faithfulness Domain

Proof assistant 可以驗證：

$$
FormalStatement.
$$

但研究系統還必須驗證：

$$
FormalStatement
\approx
IntendedStatement.
$$

因此：

$$
Verification
=
FormalValidity
+
SemanticFaithfulness
+
ScopeFaithfulness.
$$

其中任何一項可能失敗。

特別是：

$$
LeanAccepts(\pi,Q_f)
$$

只能推出 $Q_f$ 在相應 formal environment 下具有 kernel-accepted proof。它不能單獨推出：

$$
Q_f
=
Q_{intended}.
$$

因此 $D_V$ 是 CMDC 不可省略的一域。

# 16. $D_B$：Bridge / Existing Mathematics Domain

新生成概念 $X$ 若沒有 bridge，至少存在四種風險： $X$ 其實是舊概念換名字、是已知概念的特殊情形、是已知理論的簡單重新編碼、或與既有理論矛盾但系統沒有察覺。

因此：

$$
BridgeDiagnosis(X)
$$

至少搜尋：

$$
EquivalentTo,
SpecialCaseOf,
Generalizes,
ReducesTo,
IsomorphicTo,
IndependentFrom,
Contradicts.
$$

Bridge gap 不是附加文獻工作，而是數學合法性的一部分。

# 17. $D_N$：Novelty / Interestingness Domain

自動猜想系統可以產生大量真命題。但：

$$
Truth
\not\Rightarrow
Interestingness.
$$

同樣：

$$
Novelty
\not\Rightarrow
Importance.
$$

因此系統至少應分離：

$$
Correctness,
Novelty,
Interestingness,
Utility.
$$

Interestingness 可以由多種信號近似，例如：

$$
CompressionGain,
UnificationPower,
Surprise,
DependencyCentrality,
ProofUtility,
HumanInterest.
$$

但任何自動 interestingness score 都只能是研究排序器，而不是共同體價值的最終裁決。

# 18. 一個 gap 的 canonical 結構

本文定義：

$$
\delta_i
=
(
I_i,
D_i,
T_i,
E_i,
S_i,
C_i,
B_i,
R_i,
Dep_i
).
$$

其中 $I_i$ 是 gap identity， $D_i$ 是 domain， $T_i$ 是 target， $E_i$ 是 evidence， $S_i$ 是 severity， $C_i$ 是 confidence， $B_i$ 是 blocking status， $R_i$ 是 candidate repair classes， $Dep_i$ 是 dependency gaps。

例如：

```json
{
  "gap_id": "gap:def:017",
  "domain": "definition",
  "target_ref": "term:density",
  "evidence_refs": ["obs:221", "formalizer:error:18"],
  "severity": "high",
  "confidence": 0.91,
  "blocking": true,
  "candidate_repairs": [
    "clarify_definition",
    "map_to_existing_definition",
    "split_overloaded_term"
  ],
  "depends_on": []
}
```

# 19. Gap 不是永遠互相獨立

實際上：

$$
\delta_i
\rightarrow
\delta_j
$$

可能表示修復 $\delta_i$ 後才能判斷 $\delta_j$。

例如：

$$
DefinitionGap
\rightarrow
FormalizationGap
\rightarrow
ProofGap.
$$

因此 Gap Map 更合理地表示為：

$$
G_\Delta
=
(
V_\Delta,
E_\Delta
).
$$

其中：

$$
V_\Delta
=
\{
\delta_1,\ldots,\delta_n
\}.
$$

而：

$$
\delta_i
\rightarrow
\delta_j
$$

代表 $\delta_j$ 在診斷或修復上依賴 $\delta_i$。

這稱為：

$$
\boxed{
\text{Repair Dependency Graph}.
}
$$

# 20. Dominant Gap 與 Secondary Gap

不是每個 gap 都值得立即處理。

定義：

$$
Priority(\delta_i)
=
f(
Blocking,
Severity,
Confidence,
ExpectedGain,
RepairCost,
DependencyCentrality
).
$$

因此：

$$
\delta^*
=
\arg\max_{\delta_i\in\Delta_t}
Priority(\delta_i).
$$

但若：

$$
Confidence(\delta^*)<\tau,
$$

合理操作可能是：

$$
GatherEvidence
$$

而不是立即 repair。

# 21. Gap Diagnosis 本身也可以錯

本文不將 diagnosis 視為 oracle。

令真實缺口集合：

$$
\Delta^*.
$$

AI 估計：

$$
\hat\Delta.
$$

則可測：

$$
Precision_{gap},
Recall_{gap},
F1_{gap},
$$

以及 typed confusion matrix。

例如 DefinitionGap 可能被錯判為 MethodGap。這種誤診很重要，因為它會使 AI 投入錯誤研究方向。

因此：

$$
\boxed{
Diagnosis
\neq
Truth.
}
$$

# 22. 從 Gap 到 Repair：CMDC 的核心映射

對 gap：

$$
\delta_i,
$$

CMDC 產生：

$$
\mathcal R(\delta_i)
=
\{
r_1,\ldots,r_k
\}.
$$

其中每個 $r_j$ 都是 typed repair candidate。

形式：

$$
r_j
=
(
RepairType,
Target,
Preconditions,
Mutation,
ExpectedEffect,
Risks,
Obligations
).
$$

因此：

$$
\boxed{
Gap
\rightarrow
RepairCandidate
}
$$

不是：

$$
Gap
\rightarrow
DirectMutation.
$$

# 23. Typed Repair Taxonomy

第一版 repair class 可以包括：

$$
R_P=\text{ProblemClarification},
$$

$$
R_D=\text{DefinitionRepair},
$$

$$
R_A=\text{AssumptionRepair},
$$

$$
R_J=\text{CriterionRepair},
$$

$$
R_R=\text{RepresentationRepair},
$$

$$
R_S=\text{SolutionSpaceRepair},
$$

$$
R_M=\text{MethodRepair},
$$

$$
R_L=\text{Lemma/TheoryRepair},
$$

$$
R_C=\text{ComputeRepair},
$$

$$
R_E=\text{EvidenceRepair},
$$

$$
R_V=\text{VerificationRepair},
$$

$$
R_B=\text{BridgeRepair},
$$

$$
R_N=\text{NoveltyAssessmentRepair}.
$$

這裡「repair」不是說原問題一定有錯，而是對當前 research state 的一個結構性修復或補全。

# 24. Repair Contract

每個 repair 都應具有：

$$
RC(r)
=
(
AllowedMutation,
ForbiddenMutation,
RequiredEvidence,
RequiredObligations,
RollbackPolicy,
PromotionPolicy
).
$$

例如 DefinitionRepair 可允許：

```text
- split an overloaded term
- introduce an explicit parameter
- map to a standard mathematical definition
```

但禁止：

```text
- silently alter theorem scope
- silently strengthen assumptions
- erase original wording
```

因此 CMDC 是：

$$
\boxed{
\text{constrained generation},
}
$$

不是自由改寫。

# 25. Gap Closure Condition

Repair 完成不能只靠 AI 說「我覺得問題修好了」。

對 gap $\delta_i$ 定義：

$$
Close(\delta_i)
\iff
C_1
\land
C_2
\land
\cdots
\land
C_m.
$$

例如 DefinitionGap 的 closure conditions 可以是：

$$
DefinitionExplicit
\land
BoundaryHandled
\land
Formalizable
\land
PriorArtRelationChecked.
$$

MethodGap 的 closure conditions 可以是：

$$
MethodSpecified
\land
ApplicabilityEstablished
\land
FailureModeKnown.
$$

因此：

$$
RepairProposed
\neq
GapClosed.
$$

# 26. Repair-Induced Obligation

任何 repair 都可能製造新的義務。

令：

$$
r:
S_t^M
\rightarrow
S_{t+1}^M.
$$

則：

$$
\mathcal O(r)
=
ObligationGenerator(r).
$$

例如：

$$
AddAssumption(A)
$$

產生：

$$
O_1=\text{declare problem mutation},
$$

$$
O_2=\text{justify necessity or relevance},
$$

$$
O_3=\text{track old and new problem separately}.
$$

RepresentationRepair 產生：

$$
O=\text{semantic equivalence or relationship proof}.
$$

MethodRepair 產生：

$$
O=\text{correctness/applicability obligations}.
$$

因此：

$$
\boxed{
Repair
\rightarrow
NewObligations.
}
$$

# 27. Repair Cascade

修復一個 gap 可能產生另一個 gap：

$$
\delta_1
\xrightarrow{r_1}
\delta_2.
$$

例如 DefinitionRepair 引入新 parameter，接著產生 AssumptionGap；或 RepresentationRepair 導致 VerificationGap。

因此 CMDC 不是：

$$
Detect
\rightarrow
Fix
\rightarrow
Done.
$$

而是：

$$
Diagnose
\rightarrow
Repair
\rightarrow
ReDiagnose.
$$

即：

$$
\boxed{
S_t^M
\rightarrow
\Delta_t
\rightarrow
r_t
\rightarrow
S_{t+1}^M
\rightarrow
\Delta_{t+1}.
}
$$

# 28. 最小變更原則

在多個 repair 都可解除 gap 時，初步可以採：

$$
r^*
=
\arg\min_r
MutationCost(r)
$$

subject to：

$$
GapClosed(r)=1.
$$

Mutation cost 可包含：

$$
ProblemIdentityDistance,
TheoryChangeMagnitude,
NewAssumptions,
VerificationCost.
$$

這是一種：

$$
\boxed{
\text{Minimal Mathematical Repair Principle}.
}
$$

但它不是絕對規則。有時較大的理論重構能帶來更自然、更一般的結果，因此系統應允許 human/contract 指定：

$$
PreferMinimalRepair
$$

或：

$$
PermitTheoryRefactor.
$$

# 29. 禁止「捷徑式修復」

CMDC 至少禁止以下模式。

## 29.1 Silent Assumption Injection

原問題：

$$
Q.
$$

AI 改成：

$$
A\Rightarrow Q
$$

但仍回報「證明 $Q$ 」。禁止。

## 29.2 Silent Restriction

原域：

$$
X.
$$

AI 只證：

$$
X'\subsetneq X
$$

但回報全域成立。禁止。

## 29.3 Definition Drift

研究中途改變：

$$
Definition_t(x)
\rightarrow
Definition_{t+1}(x)
$$

卻不版本化。禁止。

## 29.4 Formalization Substitution

證成形式命題：

$$
F(Q)
$$

後直接宣稱自然語言 $Q$ 已證，而未做 faithfulness check。禁止。

## 29.5 Rename-as-Novelty

把既有概念換名字後宣稱新理論。禁止。

# 30. 何時 Repair 應該變成 New Problem

不是所有修改都應被視為原問題修復。

定義 problem distance：

$$
d_P(Q_i,Q_j).
$$

若：

$$
d_P(Q_i,Q_j)>\tau_P,
$$

或變換類型為：

$$
NewProblem,
$$

則 $Q_j$ 應成為新的 research branch。

因此：

$$
Q_0
\rightarrow
\{
Q_1,
Q_2,
Q_3
\}
$$

可以形成 Problem DAG，而不是單一路徑。這使 AI 可以探索新問題，但不能把新問題冒充舊問題。

# 31. Local Domain Completion

對研究 scope：

$$
\Omega,
$$

令所需構件集合：

$$
Req(\Omega).
$$

已具備構件：

$$
Have_t(\Omega).
$$

則缺失：

$$
Missing_t(\Omega)
=
Req(\Omega)
-
Have_t(\Omega).
$$

若：

$$
CriticalMissing_t(\Omega)
=
\varnothing,
$$

且必要 obligations 已解除，則可以說：

$$
LocalDomainComplete(\Omega,t)=1.
$$

這裡的 complete 表示：在目前研究 scope 與契約下，已具備足夠結構繼續研究或形成 theory package。

它不表示：

$$
\text{all mathematics in this domain is complete}.
$$

# 32. Completion 不是 Closure of Mathematics

本文特別區分：

$$
LocalDomainCompletion
$$

與：

$$
GlobalMathematicalClosure.
$$

後者不是本文主張。

因此：

$$
\boxed{
LocalDomainCompletion(\Omega)
\not\Rightarrow
NoFurtherMathematics(\Omega).
}
$$

即使局部 scope 已足夠：

$$
NewQuestions
$$

仍可無界產生。

# 33. 生成新詞彙的合法流程

若 gap 為：

$$
TerminologyGap,
$$

AI 可以生成：

$$
\tau_{new}.
$$

但 promotion 前至少要：

$$
Define(\tau_{new}),
Examples(\tau_{new}),
NonExamples(\tau_{new}),
BoundaryCases(\tau_{new}),
PriorArtSearch(\tau_{new}),
BridgeKnownConcepts(\tau_{new}).
$$

因此：

$$
NameCreated
\neq
ConceptCreated.
$$

而：

$$
ConceptCreated
\neq
MathematicalContributionAccepted.
$$

# 34. 生成新方法論的合法流程

若：

$$
MethodGap
$$

成立，AI 可以提出：

$$
M_{new}.
$$

但應形成：

$$
MethodCandidate
=
(
Domain,
InputType,
Preconditions,
Transformation,
OutputType,
Invariants,
Termination,
CorrectnessClaim,
ComplexityClaim,
FailureModes
).
$$

之後：

$$
Test
\rightarrow
Compare
\rightarrow
Verify
\rightarrow
Register.
$$

若 correctness 尚未證成，可以保存：

$$
MethodStatus=Experimental.
$$

而不是：

$$
MethodStatus=Established.
$$

# 35. 生成新引理與 theory fragment

對 dependency gap：

$$
\delta_L,
$$

系統可以生成候選：

$$
L_1,\ldots,L_k.
$$

但候選引理除了可證性外，還應評估：

$$
Utility(L_i,Q),
$$

因為：

$$
Provable(L_i)
$$

不代表：

$$
Useful(L_i,Q).
$$

可使用：

$$
DependencyReduction,
ProofSearchGain,
ReusePotential
$$

等信號排序。

# 36. 反例不是失敗，而是 Repair Trigger

若：

$$
Counterexample(C)=x,
$$

則：

$$
C=\text{False}.
$$

但 autonomous researcher 不應只輸出：

$$
\text{FAIL}.
$$

它應重新診斷：

$$
WhyFalse(C,x)?
$$

並可能產生：

$$
RestrictionCandidate,
AssumptionCandidate,
DefinitionRevisionCandidate,
NewConjectureCandidate.
$$

因此：

$$
\boxed{
Counterexample
=
ResearchStateTransition,
}
$$

而不是終止碼。

# 37. Proof Repair 與 Domain Repair 的差別

現有 proof-repair 系統通常處理：

$$
ErroneousProof
+
CompilerFeedback
\rightarrow
RepairedProof.
$$

本文提出的 Domain Repair 更一般：

$$
ResearchState
+
MultiDomainEvidence
\rightarrow
TypedMathematicalRepair.
$$

Proof repair 可以被視為：

$$
ProofRepair
\subset
Verification/MethodRepair.
$$

因此 CMDC 不是取代 proof repair，而是把它放進更大的 research-diagnosis ontology。

# 38. Autoformalization 與 Definition Gap

真實數學定義的 autoformalization 已被證明比受控 benchmark 更困難。這支持一個重要設計：

$$
FormalizationFailure
$$

不應永遠被判成：

$$
ModelFailure.
$$

它也可能表示：

$$
DefinitionGap,
LibraryGroundingGap,
RepresentationGap,
ContextGap.
$$

因此 formalizer error 應成為：

$$
Evidence(\delta_i),
$$

而不是只是一個 retry signal。

# 39. Theory-Level Autoformalization 與 CMDC

Theory-level autoformalization 強調：

$$
Axioms
+
Definitions
+
Lemmas
+
Dependencies
$$

必須作為 coherent library 處理。

CMDC 往前多走一步：若這個 theory context 本身有缺口，AI 能否先診斷缺少哪一種構件，再提出受約束的候選補全？

因此：

$$
TheoryLevelAutoformalization
$$

主要處理：

$$
InformalTheory
\rightarrow
FormalTheory.
$$

而 CMDC 允許：

$$
IncompleteResearchState
\rightarrow
DiagnosedGaps
\rightarrow
CandidateTheoryExtensions.
$$

兩者可以互補。

# 40. Automated Conjecturing 與 CMDC

Automated conjecturing 一般研究：

$$
Definitions+Axioms
\rightarrow
Conjectures.
$$

CMDC 則先問：

$$
ShouldConjectureGenerationBeInvoked?
$$

若當前主要缺口是：

$$
DefinitionGap,
$$

大量 conjecture generation 可能是錯誤行動。

因此：

$$
\boxed{
Conjecturing
=
OneRepairClass,
}
$$

而不是所有數學自治的共同預設。

# 41. ACR 中的數學診斷狀態

一般 Semantic State 可已有：

```text
progress
uncertainty
failures
missing
risks
budget
authority
```

數學 extension 可以加：

```text
problem_ref
problem_version
theory_refs
definition_refs
assumption_refs
representation_ref
gap_refs
obligation_refs
verification_refs
bridge_refs
novelty_state
```

因此：

$$
SemanticState
\rightarrow
MathematicalSemanticState
$$

可採 extension 而不是重寫。

# 42. 數學 Affordance Retrieval

給定：

$$
S_t^M
$$

與 Gap Map：

$$
\Delta_t,
$$

系統取得：

$$
\mathcal A_M(S_t^M,\Delta_t)
=
\{
\Omega_1,\ldots,\Omega_k
\}.
$$

例如：

```text
cog://math/clarify-problem
cog://math/define
cog://math/add-assumption-candidate
cog://math/change-representation
cog://math/generate-lemma
cog://math/search-counterexample
cog://math/retrieve-method
cog://math/generate-method
cog://math/increase-compute
cog://math/verify-faithfulness
cog://math/bridge-theory
```

因此：

$$
GapDiagnosis
\rightarrow
CognitiveAffordance.
$$

# 43. Diagnosis-Aware Cognitive Routing

令候選 cognition：

$$
\Omega_i.
$$

評分可以是：

$$
Score(\Omega_i)
=
w_g GapFit
+
w_b BlockingReduction
+
w_e ExpectedResearchGain
+
w_h HistoricalUtility
-
w_c Cost
-
w_r Risk.
$$

而不只是：

$$
SemanticSimilarity.
$$

例如：

$$
Gap=DefinitionGap
$$

時：

$$
Score(DEFINE)
>
Score(MORE\_PROOF\_SEARCH)
$$

應可被 benchmark 驗證。

# 44. 自主研究中的 DEFER / ESCALATE

若：

$$
Confidence(Diagnosis)<\tau,
$$

AI 可以：

$$
DEFER
$$

並等待：

$$
MoreEvidence.
$$

若 repair 需要：

$$
NewAxiom
$$

或重大 problem mutation，而 contract 不允許自主 promotion，則：

$$
ESCALATE.
$$

這避免：

$$
Uncertainty
\rightarrow
FabricatedCertainty.
$$

# 45. 自主研究中的 IDLE / STOP

若沒有 cognition 具有正 expected gain，AI 可以：

$$
IDLE.
$$

若目前 scope 已完成：

$$
LocalDomainComplete(\Omega)=1,
$$

則可：

$$
STOP.
$$

因此自治不等於：

$$
InfiniteTheoryGeneration.
$$

# 46. Diagnosis Receipt

每次重大 diagnosis 應形成：

$$
DiagnosisReceipt_t.
$$

至少包含：

$$
(
StateRef,
GapRefs,
EvidenceRefs,
Confidence,
Alternatives,
SelectedGap,
KnowledgeBoundaryRef
).
$$

它不是 private chain-of-thought，而是當時系統公開採用的 gap classification 與證據。

這讓未來可以審計：AI 為什麼認為問題缺的是定義，而不是方法？

# 47. Repair Receipt

Repair 決策應保存：

$$
RepairReceipt
=
(
GapRef,
RepairCandidateRef,
ProblemBeforeRef,
ProblemAfterRef,
MutationType,
ObligationRefs,
ValidationRefs,
Decision
).
$$

因此：

$$
DiagnosisReceipt
\neq
RepairReceipt.
$$

前者回答「缺什麼？」，後者回答「決定怎麼補？」

# 48. Gap Closure Receipt

當系統宣稱 gap 已關閉：

$$
GapStatus:
Open
\rightarrow
Closed,
$$

需要：

$$
GapClosureReceipt.
$$

至少保存：

$$
ClosureConditions,
EvidenceRefs,
VerifierRefs,
RemainingRisks.
$$

因此：

$$
Closed
$$

成為可審計狀態，而不是 prose assertion。

# 49. 評估：Diagnosis Accuracy

建立 benchmark：

$$
B_{diag}
=
B_P
\cup
B_D
\cup
B_A
\cup
\cdots
\cup
B_N.
$$

其中每個 case 故意放入已知 gap。

測：

$$
Accuracy_{domain},
Precision_{domain},
Recall_{domain},
Calibration.
$$

另外需要 multi-label evaluation，因為一個問題可同時具有多個 gap。

# 50. 評估：Repair Validity

對 repair：

$$
r,
$$

定義：

$$
RepairValidity(r)
=
GapReduction
-
NewUndeclaredDamage.
$$

更具體可拆：

$$
RV
=
(
ClosureSuccess,
IdentityPreservation,
ObligationCoverage,
NoSilentMutation,
DownstreamGain
).
$$

因此「修完能證」只是其中一軸。

# 51. 評估：Downstream Research Gain

最重要的實驗之一是比較：

$$
DirectResearch
$$

與：

$$
DiagnoseThenResearch.
$$

設：

$$
Performance_{direct}
$$

與：

$$
Performance_{diag}.
$$

檢驗：

$$
Performance_{diag}
>
Performance_{direct}?
$$

但 performance 不只看 final solved rate，也可以看：

$$
TimeToCorrectDiagnosis,
InvalidMutationRate,
ProofSearchWaste,
FormalizationFailureRate.
$$

# 52. 評估：Matched Repair vs Random Repair

對同一 gap：

$$
\delta,
$$

比較：

$$
MatchedRepair(\delta)
$$

與：

$$
RandomRepair.
$$

若 CMDC 有意義，應期待：

$$
ExpectedGain(
MatchedRepair
)
>
ExpectedGain(
RandomRepair
).
$$

# 53. 評估：Wrong-Domain Intervention

也應故意測：

$$
Gap=Definition
$$

但強制：

$$
Action=IncreaseCompute.
$$

與：

$$
Action=ProofSearch.
$$

比較 matched action。這可以回答：域診斷是否真的改變研究效率，而不只是產生漂亮標籤？

# 54. 評估：Repair Minimality

測：

$$
MutationDistance(Q_0,Q_1)
$$

與 gap closure success。

希望系統避免：

$$
SmallGap
\rightarrow
HugeTheoryRewrite.
$$

但不能把 minimality 設成唯一 objective。

因此評估應為 Pareto：

$$
(
GapClosure,
MutationCost,
ResearchGain
).
$$

# 55. 評估：Problem Identity Preservation

對刻意設計的陷阱題，測 AI 是否靜默加假設、靜默限制域、靜默改定義、靜默換形式命題、或將新問題結果回報為原問題結果。

定義：

$$
IdentityViolationRate.
$$

理想：

$$
IdentityViolationRate
\rightarrow
0.
$$

# 56. 評估：Obligation Coverage

對每種 repair class，人工建立：

$$
RequiredObligations(r).
$$

AI 產生：

$$
GeneratedObligations(r).
$$

測：

$$
Coverage
=
\frac{
|Generated\cap Required|
}{
|Required|
}.
$$

同時測 false obligations，以避免 `GenerateEverything` 造成表面高 recall。

# 57. 評估：Long-Horizon Repair Stability

某 repair 在第 $t$ 輪看似成功：

$$
GapClosed_t.
$$

但在：

$$
t+k
$$

可能暴露：

$$
HiddenContradiction.
$$

因此 closure 應允許：

$$
Closed
\rightarrow
Reopened.
$$

並測：

$$
ReopenRate,
DelayedFailureDetection.
$$

這比一次性 success 更接近真實研究。

# 58. Multi-Agent Diagnosis

不同角色可以平行產生：

$$
Diagnosis_A,
Diagnosis_B,
Diagnosis_C.
$$

例如：

$$
Formalizer,
CounterexampleAgent,
LiteratureAgent,
MethodAgent.
$$

最後：

$$
Join
\rightarrow
GapMap.
$$

但多 Agent 不應被誤認為天然更正確。仍需要：

$$
EvidenceMerge,
ConflictResolution,
Calibration.
$$

# 59. 人類的角色

CMDC 不要求人類逐輪提供下一步。但某些 repair 類別可以被 contract 設為：

$$
ApprovalRequired.
$$

例如：

$$
NewAxiom,
CanonicalProblemMutation,
NoveltyClaim,
SubmissionReadyPromotion.
$$

因此人類從：

$$
StepAuthor
$$

逐步轉為：

$$
ContractAuthority
+
ExpertReviewer.
$$

# 60. 與數學共同體的接口

數學共同體接受的不是「AI 說這是一個完整的新理論」，而是更可審查的：

$$
TheoryPackage
=
(
OriginalProblem,
ProblemVersions,
GapMap,
Definitions,
Assumptions,
Results,
Proofs,
Counterexamples,
Methods,
Bridges,
OpenObligations,
Provenance
).
$$

這使人類可以：

$$
Inspect,
Reproduce,
Reject,
Revise,
Extend.
$$

因此：

$$
\boxed{
CommunityCompatibility
=
Auditability
+
Reproducibility
+
ExplicitTheoryChange.
}
$$

# 61. 與 Paper 01 的關係

Paper 01 建立總體：

$$
AMRR
=
ACR
+
DomainDiagnosis
+
CMDC
+
Verification
+
TheoryBridge.
$$

本文只深入：

$$
DomainDiagnosis
+
CMDC.
$$

其目標不是重新介紹 AMRR，而是回答兩個問題：

$$
\boxed{
\text{What exactly is missing?}
}
$$

以及：

$$
\boxed{
\text{What counts as a legitimate repair?}
}
$$

# 62. 與 Paper 03 的接口

本文故意不把所有 obligation、problem identity 與 theory extension 問題完全展開。下一篇將專門形式化：

$$
ProblemIdentity,
TheoryExtension,
Conservativity,
MathematicalObligations.
$$

本文只建立必要接口：

$$
Repair
\rightarrow
MathChangeSet
\rightarrow
Obligations.
$$

# 63. 與 Paper 04 的接口

Paper 04 將把本文的 Gap、Repair、Closure、Receipt 變成真正 runtime schema 與 executable loop。

即：

$$
S_t^M
\rightarrow
Diagnose
\rightarrow
GapMap
\rightarrow
Route
\rightarrow
Repair
\rightarrow
Verify
\rightarrow
ReDiagnose.
$$

# 64. 研究限制

第一，十三域 taxonomy 不是終極分類。

第二，domain diagnosis 的 ground truth 在高階研究問題上可能本身具有爭議。

第三，不同數學領域的 gap structure 可能非常不同。

第四，某些 breakthrough 可能來自看似「錯域」的跨域操作，因此 matched repair 不應變成硬禁止。

第五，interestingness 與 novelty 仍高度依賴人類與歷史脈絡。

第六，局部 repair 可能累積成長期理論漂移，因此必須有 CTCL / ledger 與 Problem Identity 層。

第七，本文仍屬方法論與架構論文，實證 benchmark 留待 AMRR MVP 完成後進行。

# 65. 可否證命題

本文提出至少六個可直接否證的命題。

## H1 — Diagnosis Utility

$$
DiagnoseThenAct
>
DirectAct
$$

在預先植入 domain gaps 的 benchmark 上成立。

## H2 — Matched Repair

$$
MatchedRepair
>
RandomRepair.
$$

## H3 — Wrong-Domain Cost

$$
Cost(WrongDomainAction)
>
Cost(MatchedDomainAction).
$$

## H4 — Identity Preservation

加入 CMDC / Problem Identity gate 後：

$$
SilentMutationRate
\downarrow.
$$

## H5 — Obligation Coverage

typed repair 能提高：

$$
RequiredObligationRecall.
$$

## H6 — Long-Horizon Stability

Re-diagnosis loop 相較一次性 repair：

$$
DelayedFailureDetection
\uparrow.
$$

若這些命題大多不成立，CMDC 作為獨立方法論的價值就必須重新評估。

# 66. 核心不變量

本文最後固定十個不變量。

$$
\boxed{
Unsolved
\neq
SingleFailureMode.
}
$$

$$
\boxed{
Diagnosis
\neq
Truth.
}
$$

$$
\boxed{
Gap
\neq
Repair.
}
$$

$$
\boxed{
RepairCandidate
\neq
AcceptedMutation.
}
$$

$$
\boxed{
RepairProposed
\neq
GapClosed.
}
$$

$$
\boxed{
Repair
\rightarrow
Obligations.
}
$$

$$
\boxed{
MoreCompute
\not\Rightarrow
BetterProblemState.
}
$$

$$
\boxed{
ProofSuccess
\not\Rightarrow
SemanticFaithfulness.
}
$$

$$
\boxed{
LocalDomainCompletion
\not\Rightarrow
GlobalMathematicalClosure.
}
$$

$$
\boxed{
GenerationFreedom\uparrow
\Longrightarrow
VerificationObligation\uparrow.
}
$$

# 67. 最終模型

完整 CMDC loop：

$$
\boxed{
\begin{aligned}
S_t^M
&\xrightarrow{Observe}
O_t\\
&\xrightarrow{Diagnose}
\Delta_t\\
&\xrightarrow{Prioritize}
\delta_t^*\\
&\xrightarrow{Retrieve/Generate}
\mathcal R_t\\
&\xrightarrow{Govern}
r_t^*\\
&\xrightarrow{ApplyCandidate}
S_{t+1}^{M,candidate}\\
&\xrightarrow{GenerateObligations}
\mathcal O_t\\
&\xrightarrow{Verify}
V_t\\
&\xrightarrow{Accept/Reject}
S_{t+1}^M\\
&\xrightarrow{ReDiagnose}
\Delta_{t+1}.
\end{aligned}
}
$$

其中任何階段都可以：

$$
REFUSE,
DEFER,
STOP,
IDLE,
ESCALATE.
$$

# 68. 核心命題

本文將整篇壓縮為：

$$
\boxed{
\textbf{
An autonomous mathematical system should not interpret every research failure as a request for more proof search.
}
}
$$

更完整地：

$$
\boxed{
\textbf{
It should diagnose which mathematical domain is incomplete,
generate only typed candidate repairs,
preserve the identity of the original problem,
and require explicit evidence before declaring a gap closed.
}
}
$$

中文：

> **自主數學 AI 面對「解不出來」時，不應只有繼續算、繼續證或重新生成答案三種反應。它應先判定缺的是問題、定義、假設、判定、表示、方法、引理、算力、反例、驗證、橋接或新穎性中的哪一部分，再提出與該缺口相符的候選補全；而任何補全只有在問題身份、義務與驗證條件被保留後，才有資格成為新的數學研究狀態。**

# 69. 結論

數學研究不是固定問題上的單一證明搜尋。

更一般地，它是一個：

$$
\boxed{
\text{problem state}
+
\text{theory state}
+
\text{gap state}
+
\text{repair state}
}
$$

共同演化的過程。

本文因此把：

$$
Solved/Unsolved
$$

二分法展開為：

$$
MathematicalDomainDiagnosis.
$$

再把：

$$
TryAgain
$$

展開為：

$$
ConstrainedMathematicalDomainCompletion.
$$

真正重要的轉變是：

$$
\boxed{
\text{AI no longer merely searches inside a given mathematical space; it can diagnose and cautiously repair the space required for research itself.}
}
$$

但「修復空間」並不代表 AI 可以自由重寫數學。

相反，CMDC 的基本交換是：

$$
\boxed{
\text{more generative freedom}
\Longleftrightarrow
\text{more explicit mathematical obligations}.
}
$$

因此，下一篇必須正式處理：

$$
ProblemIdentity,
TheoryExtension,
Conservativity,
MathematicalObligation.
$$

也就是回答：**當 AI 可以自行改定義、補假設、建新方法甚至提出新公理時，究竟什麼條件下仍可說它在研究原問題，什麼時候已經建立另一個理論？**

這將構成系列 Paper 03。

---

# 參考文獻

[1] Feng, T., Trinh, T. H., Bingham, G., et al. (2026). *Towards Autonomous Mathematics Research*. arXiv:2602.10177.

[2] Tsoukalas, G., Kovsharov, A., Shirobokov, S., et al. (2026). *Advancing Mathematics Research with AI-Driven Formal Proof Search*. arXiv:2605.22763.

[3] Min, M. J., He, M., Li, Z., Yi, Z., Malik, S., Gupta, A., Si, X., & Bastani, O. (2026). *Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases*. arXiv:2607.13292. ICML 2026 Position Track, Spotlight.

[4] Zhang, L., Valentino, M., & Freitas, A. (2025). *Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions*. Proceedings of EMNLP 2025, 1720–1738. DOI: 10.18653/v1/2025.emnlp-main.90.

[5] Zhang, J., & Tan, S.-C. (2026). *Automated Conjecturing and Theorem Finding: A Survey*. Journal of Computer Science and Technology, 41(1), 46–66. DOI: 10.1007/s11390-026-6040-0.

[6] Tsoukalas, G., Saha, R., Thakur, A., Reguyal, S., & Chaudhuri, S. (2025). *Learning Interestingness in Automated Mathematical Theory Formation*. Advances in Neural Information Processing Systems 38.

[7] Wang, E., Chess, S., Lee, D., Ge, S., Mallavarapu, A., Alper, J., & Ilin, V. (2026). *Learning to Repair Lean Proofs from Compiler Feedback*. arXiv:2602.02990.

[8] Ospanov, A., & Yousefzadeh, R. (2025). *APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning*. arXiv:2505.05758.

[9] Poiroux, A., Weiss, G., Kunčak, V., & Bosselut, A. (2025). *Reliable Evaluation and Benchmarks for Statement Autoformalization*. Proceedings of EMNLP 2025, 17947–17969. DOI: 10.18653/v1/2025.emnlp-main.907.

---

# 內部架構依賴文件

[I1] Neo.K. (2026). *從數學解題到自主數學研究：受約束數學域補全與自主數學研究 Runtime*，Autonomous Mathematical Research / Paper 01 of 04，v0.1.

[I2] Neo.K. (2026). *從自提示到自主認知閉環：持續目標型 AI 的基礎理論*，系列 01/06，v0.1.

[I3] Neo.K. (2026). *可定址認知空間：Cognitive Affordance、Semantic Address 與認知算子*，系列 02/06，v0.1.

[I4] Neo.K. (2026). *自我對話不是文字：AI-Native Cognitive Program 與 Zero-Rendering Runtime*，系列 03/06，v0.1.

[I5] Neo.K. (2026). *時間因果自我史：CTCL-ITR、Decision Receipt 與上下文壓縮後的可追溯性*，系列 04/06，v0.1.

[I6] Neo.K. (2026). *契約邊界內的 AI 自主性：Execute、Refuse、Defer、Idle 與 Escalate*，系列 05/06，v0.1.

[I7] Neo.K. (2026). *Addressable Cognitive Runtime × CTCL：統一技術白皮書與實作路線圖 v0.1*，系列 06/06.

---

# 版本備註

**v0.1 / 2026-08-23**

本版正式固定：

1. Multi-Domain Mathematical Diagnosis；
2. Mathematical Research Domain Set v1；
3. Mathematical Domain Gap Map；
4. Repair Dependency Graph；
5. Typed Repair Taxonomy；
6. Repair Contract；
7. Gap Closure Condition；
8. Repair-Induced Obligation；
9. Repair Cascade；
10. Minimal Mathematical Repair Principle；
11. Local Domain Completion；
12. Diagnosis / Repair / Gap Closure Receipts；
13. diagnosis-aware cognitive routing；
14. CMDC falsification gates；
15. 與 Paper 03 / Paper 04 的接口。

本版不宣稱十三域分類已是終極 taxonomy，也不宣稱 CMDC 已經由大規模 empirical benchmark 驗證。所有效能優勢均留待後續 AMRR MVP 與實驗論文測試。