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

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

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

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。

例如：

{
  "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 可允許：

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

但禁止：

- 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 可已有：

progress
uncertainty
failures
missing
risks
budget
authority

數學 extension 可以加：

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 \}.

例如：

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

本版正式固定：

Multi-Domain Mathematical Diagnosis；
Mathematical Research Domain Set v1；
Mathematical Domain Gap Map；
Repair Dependency Graph；
Typed Repair Taxonomy；
Repair Contract；
Gap Closure Condition；
Repair-Induced Obligation；
Repair Cascade；
Minimal Mathematical Repair Principle；
Local Domain Completion；
Diagnosis / Repair / Gap Closure Receipts；
diagnosis-aware cognitive routing；
CMDC falsification gates；
與 Paper 03 / Paper 04 的接口。

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

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

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

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

摘要

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

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

3. 從 Failure Code 到 Mathematical Domain State

4. 第一版 Mathematical Research Domain Set

5. DPD_PDP​：Problem / Specification Domain

6. DDD_DDD​：Definition Domain

7. DAD_ADA​：Assumption / Boundary Domain

8. DJD_JDJ​：Judgment / Success Criterion Domain

9. DRD_RDR​：Representation Domain

10. DSD_SDS​：Solution Domain

11. DMD_MDM​：Method Domain

12. DLD_LDL​：Lemma / Dependency / Theory Domain

13. DCD_CDC​：Computation / Search Domain

14. DED_EDE​：Examples / Counterexamples / Evidence Domain

15. DVD_VDV​：Verification / Semantic Faithfulness Domain

16. DBD_BDB​：Bridge / Existing Mathematics Domain

17. DND_NDN​：Novelty / Interestingness Domain

18. 一個 gap 的 canonical 結構

19. Gap 不是永遠互相獨立

20. Dominant Gap 與 Secondary Gap

21. Gap Diagnosis 本身也可以錯

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

23. Typed Repair Taxonomy

24. Repair Contract

25. Gap Closure Condition

26. Repair-Induced Obligation

27. Repair Cascade

28. 最小變更原則

29. 禁止「捷徑式修復」

29.1 Silent Assumption Injection

29.2 Silent Restriction

29.3 Definition Drift

29.4 Formalization Substitution

29.5 Rename-as-Novelty

30. 何時 Repair 應該變成 New Problem

31. Local Domain Completion

32. Completion 不是 Closure of Mathematics

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

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

35. 生成新引理與 theory fragment

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

37. Proof Repair 與 Domain Repair 的差別

38. Autoformalization 與 Definition Gap

39. Theory-Level Autoformalization 與 CMDC

40. Automated Conjecturing 與 CMDC

41. ACR 中的數學診斷狀態

42. 數學 Affordance Retrieval

43. Diagnosis-Aware Cognitive Routing

44. 自主研究中的 DEFER / ESCALATE

45. 自主研究中的 IDLE / STOP

46. Diagnosis Receipt

47. Repair Receipt

48. Gap Closure Receipt

49. 評估：Diagnosis Accuracy

50. 評估：Repair Validity

51. 評估：Downstream Research Gain

52. 評估：Matched Repair vs Random Repair

53. 評估：Wrong-Domain Intervention

54. 評估：Repair Minimality

55. 評估：Problem Identity Preservation

56. 評估：Obligation Coverage

57. 評估：Long-Horizon Repair Stability

58. Multi-Agent Diagnosis

59. 人類的角色

60. 與數學共同體的接口

61. 與 Paper 01 的關係

62. 與 Paper 03 的接口

63. 與 Paper 04 的接口

64. 研究限制

65. 可否證命題

H1 — Diagnosis Utility

H2 — Matched Repair

H3 — Wrong-Domain Cost

H4 — Identity Preservation

H5 — Obligation Coverage

H6 — Long-Horizon Stability

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

5. $D_P$ ：Problem / Specification Domain

6. $D_D$ ：Definition Domain

7. $D_A$ ：Assumption / Boundary Domain

8. $D_J$ ：Judgment / Success Criterion Domain

9. $D_R$ ：Representation Domain

10. $D_S$ ：Solution Domain

11. $D_M$ ：Method Domain

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

13. $D_C$ ：Computation / Search Domain

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

15. $D_V$ ：Verification / Semantic Faithfulness Domain

16. $D_B$ ：Bridge / Existing Mathematics Domain

17. $D_N$ ：Novelty / Interestingness Domain