從數學解題到自主數學研究：受約束數學域補全與自主數學研究 Runtime
From Mathematical Problem Solving to Autonomous Mathematical Research: Constrained Mathematical Domain Completion and an Autonomous Mathematical Research Runtime
系列：Autonomous Mathematical Research / Paper 01 of 04 版本：v0.1 日期：2026-08-22 作者：Neo.K
摘要
大型語言模型與形式證明系統在數學推理、自動形式化、定理證明與研究級問題探索上的能力正在快速提升。然而，「能解題」與「能自主進行數學研究」並不等價。既有系統通常預設問題、定義、成功條件與研究目標已由人類正確提供，之後再要求 AI 搜尋證明、生成猜想、調用工具或修正證明。真正的研究情境卻經常不是如此：原問題可能存在定義缺失、假設不足、表示方式不良、判定條件模糊、方法域缺口、計算能力不足、形式化不忠實，甚至問題本身就需要澄清、限制、推廣或重新建立與既有理論的關係。
本文提出一個由「解題器」轉向「自主數學研究 Runtime」的統合框架。第一，本文將數學研究失敗從單一的「未解」狀態拆解為多域問題診斷，並定義 Mathematical Domain Gap Map ，使 AI 能夠判定目前阻塞究竟來自問題域、定義域、假設域、判定域、表示域、解決域、方法域、引理／依賴域、計算域、反例／證據域、驗證域、橋接域或新穎性域。第二，本文提出 Constrained Mathematical Domain Completion, CMDC（受約束數學域補全） ：AI 在確認缺口後可以生成缺失的定義、術語、引理、方法、表示、假設、猜想與橋接構造，但每一種生成都必須同時產生對應的數學義務，並經過驗證、比較、溯源與治理後才能升格。第三，本文引入 Problem Identity Protocol ，明確區分原問題與任何修正版、限制版、推廣版、弱化版、強化版或新問題，禁止 AI 以無聲改題取代原問題。第四，本文將上述方法嵌入 Addressable Cognitive Runtime 與 CTCL-ITR 類型的持續自治架構，提出 Autonomous Mathematical Research Runtime, AMRR ：由持續研究目標、研究環境與研究契約驅動 AI 自主形成研究議程、選擇認知程序、診斷缺口、提出修復、執行研究、產生證明義務、調用驗證器、建立與既有數學的橋接，並留下可重建的時間因果研究歷史。
本文不主張現有 AI 已具備一般性的自主數學家能力，也不將形式可驗證性、數學正確性、語義忠實性、新穎性與學術接受度混為一談。本文的目標是提出一個可實作、可審計、可否證的研究架構，使「AI 自主數學研究」從模糊能力敘述轉為一組可以逐層驗證的工程與方法論命題。
關鍵詞： 自主數學研究、AI 數學、受約束數學域補全、問題身份、數學義務、自動形式化、形式證明、理論建構、Addressable Cognitive Runtime、CTCL-ITR
1. 引言：數學 AI 的下一個問題不是「還能多解幾題」
近年的 AI 數學研究已經跨越數個重要門檻。大型模型不再只處理基礎算術或標準競賽題，而開始結合長程推理、文獻搜尋、形式證明器與自我修訂處理研究級數學。Aletheia 類研究系統已經將「生成—驗證—修訂」推進到長程自然語言數學研究；AI-driven formal proof search 類系統則展示了大型模型與 Lean 等形式證明器結合後，在開放數學問題上進行可機器驗證搜尋的能力。另一方面，autoformalization 的研究焦點也正在從孤立命題翻譯，擴張到 definitions、axioms、lemmas 與依賴關係共同構成的 theory-level formalization。
這些成果共同表明：
MathematicalAI ≠ Calculator . \text{MathematicalAI}
\neq
\text{Calculator}. MathematicalAI = Calculator . 同時也表明：
MathematicalAI ≠ OneShotProblemSolver . \text{MathematicalAI}
\neq
\text{OneShotProblemSolver}. MathematicalAI = OneShotProblemSolver . 然而，若要進一步討論「自主數學研究 AI」，仍存在一個比提升 proof success rate 更基本的問題：
當原問題本身不完整、不精確、表示不良、缺乏必要方法或依賴時，AI 能否先辨認「缺的是什麼」，再在受約束條件下補出缺失數學，並證明自己沒有偷偷把問題換掉？
傳統解題流程常被抽象為：
Q → S o l v e ( Q ) → A n s w e r . Q
\rightarrow
Solve(Q)
\rightarrow
Answer. Q → S o l v e ( Q ) → A n s w er . 研究級數學更接近：
Q 0 → I n t e r p r e t → D i a g n o s e → R e f o r m u l a t e → E x p l o r e → C o n s t r u c t → P r o v e / D i s p r o v e → V e r i f y → I n t e g r a t e . Q_0
\rightarrow
Interpret
\rightarrow
Diagnose
\rightarrow
Reformulate
\rightarrow
Explore
\rightarrow
Construct
\rightarrow
Prove/Disprove
\rightarrow
Verify
\rightarrow
Integrate. Q 0 → I n t er p r e t → D ia g n ose → R e f or m u l a t e → E x pl or e → C o n s t r u c t → P r o v e / D i s p r o v e → V er i f y → I n t e g r a t e . 其中任何一個箭頭都可能失敗。
因此，本文的核心立場是：
Unsolved ≠ Single Failure Mode . \boxed{
\text{Unsolved}
\neq
\text{Single Failure Mode}.
} Unsolved = Single Failure Mode . 一個尚未解決的數學問題，可能不是因為「推理能力不夠」，而是因為研究系統尚未辨認自己所處的問題域與缺口類型。
2. 從解題到研究：兩種不同的計算對象
2.1 解題器的基本假設
對傳統 solver，輸入通常已經隱含提供：
Q = ( S t a t e m e n t , D e f i n i t i o n s , A s s u m p t i o n s , G o a l , S u c c e s s C r i t e r i o n ) . Q=
(
Statement,
Definitions,
Assumptions,
Goal,
SuccessCriterion
). Q = ( S t a t e m e n t , D e f ini t i o n s , A ss u m pt i o n s , G o a l , S u ccess C r i t er i o n ) . 因此 solver 的主要工作是搜尋：
π ∈ Π ( Q ) , \pi
\in
\Pi(Q), π ∈ Π ( Q ) , 其中 Π ( Q ) \Pi(Q) Π ( Q )
在這個模型下，問題空間被視為固定：
Q t = Q 0 . Q_t=Q_0. Q t = Q 0 . AI 只需改變搜索狀態：
R t → R t + 1 . R_t
\rightarrow
R_{t+1}. R t → R t + 1 . 2.2 研究 Runtime 的基本假設
真正數學研究中，問題本身也可能是動態研究對象：
Q t → Q t + 1 . Q_t
\rightarrow
Q_{t+1}. Q t → Q t + 1 . 例如研究者可能發現：
原定義允許退化案例；
原命題缺少必要假設；
目前表示遮蔽了不變量；
原問題其實是已知定理的重新表述；
一個更一般的問題反而具有更自然的結構；
某個方法只適用於限制子類；
原猜想存在反例；
形式化版本與自然語言原意不一致。
因此數學研究系統的狀態不應只有「目前證明寫到哪裡」，而應包括：
S t M = ( Q t , T t , K t , G t , Δ t , O t , V t , H t ) , S_t^M
=
(
Q_t,
T_t,
K_t,
G_t,
\Delta_t,
O_t,
V_t,
H_t
), S t M = ( Q t , T t , K t , G t , Δ t , O t , V t , H t ) , 其中：
Q t Q_t Q t T t T_t T t K t K_t K t G t G_t G t Δ t \Delta_t Δ t O t O_t O t V t V_t V t H t H_t H t
這使研究從：
Search over proofs \text{Search over proofs} Search over proofs 擴張為：
Search over proofs, representations, definitions, methods, assumptions, bridges, and problem versions . \boxed{
\text{Search over proofs, representations, definitions, methods, assumptions, bridges, and problem versions}.
} Search over proofs, representations, definitions, methods, assumptions, bridges, and problem versions . 3. 多域數學問題模型
本文提出第一版 Mathematical Research Domain Set ：
D = { 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 } . \mathfrak D
=
\{
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
\}. D = { 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 } . 這個集合不是宣稱數學研究只能被永久切成十三類，而是一個可版本化、可擴張的 active ontology。
3.1 D P D_P D P
問題：我們真正要問的是什麼？典型失敗包括問題語義含混、存在多種不同解讀、目標沒有固定，以及原始敘述與形式敘述不一致。
3.2 D D D_D D D
問題：使用的對象是否被充分且一致地定義？典型失敗包括未定義術語、定義循環、定義粒度不足、與既有術語重複但未建立關係，以及邊界案例失效。
3.3 D A D_A D A
問題：命題需要哪些假設、作用範圍與邊界？典型失敗包括缺必要假設、假設過強、假設互相矛盾、隱含前提未顯式化，以及研究結論超出原有效域。
3.4 D J D_J D J
問題：什麼才算解決？例如：
E x i s t e n c e ? Existence? E x i s t e n ce ? U n i q u e n e s s ? Uniqueness? U ni q u e n ess ? C l o s e d F o r m ? ClosedForm? C l ose d F or m ? A l g o r i t h m ? Algorithm? A l g or i t hm ? A p p r o x i m a t i o n ? Approximation? A pp r o x ima t i o n ? F o r m a l P r o o f ? FormalProof? F or ma l P r oo f ? 不同成功條件對應不同研究空間。
3.5 D R D_R D R
問題：當前表示是否適合研究？同一數學對象可能在：
N a t u r a l L a n g u a g e → L o g i c → A l g e b r a → G e o m e t r y → G r a p h → M a t r i x → P r o g r a m NaturalLanguage
\rightarrow
Logic
\rightarrow
Algebra
\rightarrow
Geometry
\rightarrow
Graph
\rightarrow
Matrix
\rightarrow
Program N a t u r a l L an g u a g e → L o g i c → A l g e b r a → G eo m e t r y → G r a p h → M a t r i x → P r o g r am 之間具有不同的可操作性。因此：
C o m p l e x i t y ( Q ∣ R 1 ) Complexity(Q\mid R_1) C o m pl e x i t y ( Q ∣ R 1 ) 可能遠大於：
C o m p l e x i t y ( Q ∣ R 2 ) . Complexity(Q\mid R_2). C o m pl e x i t y ( Q ∣ R 2 ) . 3.6 D S D_S D S
問題：合法解答空間究竟是什麼？例如某問題要求 exact solution，但實際上較自然的是 classification、bound、existence theorem 或 counterexample。
3.7 D M D_M D M
問題：現有方法是否足以作用於此類結構？這一域允許 AI 不只選方法，也能提出候選新方法，但新方法必須產生 correctness、applicability 與 failure obligations。
3.8 D L D_L D L
問題：目前是否缺少必要中間結果、依賴或理論基礎？形式：
T ⊢ L 1 , … , L n ⇒ Q T
\vdash
L_1,\ldots,L_n
\Rightarrow
Q T ⊢ L 1 , … , L n ⇒ Q 但若某個 L k L_k L k
3.9 D C D_C D C
問題：困難主要來自計算、搜尋、記憶體、時間或形式證明搜索成本嗎？這一域對應：
C o m p u t e , S e a r c h , M e m o r y , P a r a l l e l i s m , T o o l i n g , F o r m a l P r o o f B u d g e t . Compute,
Search,
Memory,
Parallelism,
Tooling,
FormalProofBudget. C o m p u t e , S e a r c h , M e m or y , P a r a l l e l i s m , T oo l in g , F or ma l P r oo f B u d g e t . 若瓶頸主要在此，提高算力或演算法才是合理修復。
3.10 D E D_E D E
問題：是否缺少足以約束理論的例子、反例、極端案例或計算證據？候選新定義與猜想尤其需要：
E x a m p l e s + N o n E x a m p l e s + B o u n d a r y C a s e s . Examples
+
NonExamples
+
BoundaryCases. E x am pl es + N o n E x am pl es + B o u n d a r y C a ses . 3.11 D V D_V D V
問題：我們證明的東西是不是原本想證明的東西？必須區分：
T y p e C h e c k s TypeChecks T y p e C h ec k s 與：
S e m a n t i c a l l y F a i t h f u l . SemanticallyFaithful. S e man t i c a l l y F ai t h f u l . 也必須區分：
P r o o f V a l i d ProofValid P r oo f V a l i d 與：
S t a t e m e n t C o r r e c t l y F o r m a l i z e d . StatementCorrectlyFormalized. S t a t e m e n tC or r ec tl y F or ma l i z e d . 3.12 D B D_B D B
問題：新構造與既有數學是什麼關係？AI 新生成一個定義並不足以建立新的數學貢獻。至少需要研究：
E q u i v a l e n t ? Equivalent? E q u i v a l e n t ? S p e c i a l C a s e ? SpecialCase? S p ec ia l C a se ? G e n e r a l i z a t i o n ? Generalization? G e n er a l i z a t i o n ? I s o m o r p h i c ? Isomorphic? I so m or p hi c ? R e d u c i b l e ? Reducible? R e d u c ib l e ? I n d e p e n d e n t ? Independent? I n d e p e n d e n t ? 若沒有這一域，AI 很容易建立大量形式上自洽但與數學共同體脫節的私人理論島嶼。
3.13 D N D_N D N
最後仍必須問：即使正確，它是不是值得被保留？因此：
C o r r e c t ⇏ N o v e l ⇏ I n t e r e s t i n g ⇏ U s e f u l . Correct
\not\Rightarrow
Novel
\not\Rightarrow
Interesting
\not\Rightarrow
Useful. C or r ec t ⇒ N o v e l ⇒ I n t er es t in g ⇒ U se f u l . 新穎性不是 proof assistant 能單獨判斷的屬性，必須依賴文獻、形式庫、歷史知識邊界與人類審查。
4. Mathematical Domain Gap Map
令：
D i a g n o s e : S t M → Δ t . Diagnose:
S_t^M
\rightarrow
\Delta_t. D ia g n ose : S t M → Δ t . 其中：
Δ t = { δ 1 , δ 2 , … , δ n } . \Delta_t
=
\{
\delta_1,\delta_2,\ldots,\delta_n
\}. Δ t = { δ 1 , δ 2 , … , δ n } . 每一個 gap：
δ i = ( i d , d o m a i n , t a r g e t , e v i d e n c e , s e v e r i t y , c o n f i d e n c e , b l o c k i n g , c a n d i d a t e R e p a i r s ) . \delta_i
=
(
id,
domain,
target,
evidence,
severity,
confidence,
blocking,
candidateRepairs
). δ i = ( i d , d o main , t a r g e t , e v i d e n ce , se v er i t y , co n f i d e n ce , b l oc k in g , c an d i d a t e R e p ai r s ) . 其中：
d o m a i n ( δ i ) ∈ D . domain(\delta_i)\in\mathfrak D. d o main ( δ i ) ∈ D . 於是 AI 的下一步不必直接是：
S o l v e ( Q ) . Solve(Q). S o l v e ( Q ) . 而可以是：
S e l e c t G a p ( Δ t ) → R e s e a r c h A g e n d a t + 1 . SelectGap(\Delta_t)
\rightarrow
ResearchAgenda_{t+1}. S e l ec tG a p ( Δ t ) → R ese a r c h A g e n d a t + 1 . 這使「缺什麼補什麼」從語言直覺變成可管理研究狀態。
5. 受約束數學域補全 CMDC
5.1 定義
本文定義 Constrained Mathematical Domain Completion ：
C M D C : ( S t M , δ i ) → C i \boxed{
CMDC:
(S_t^M,\delta_i)
\rightarrow
\mathcal C_i
} C M D C : ( S t M , δ i ) → C i 其中：
C i = { c 1 , … , c k } \mathcal C_i
=
\{
c_1,\ldots,c_k
\} C i = { c 1 , … , c k } 是一組針對缺口 δ i \delta_i δ i
候選可以是新定義、新術語、新表示、新假設、新 lemma、新 conjecture、新 method、新 computation strategy、新 bridge 或新 theory fragment。
但：
G e n e r a t e ( c ) ≠ A c c e p t ( c ) . Generate(c)
\neq
Accept(c). G e n er a t e ( c ) = A cce pt ( c ) . 這是 CMDC 的第一個核心不變量。
5.2 補全不是自由生成
AI 可以生成：
c n e w . c_{new}. c n e w . 但必須進入：
C a n d i d a t e → T e s t → C o m p a r e → V e r i f y → C e r t i f y → R e g i s t e r . Candidate
\rightarrow
Test
\rightarrow
Compare
\rightarrow
Verify
\rightarrow
Certify
\rightarrow
Register. C an d i d a t e → T es t → C o m p a r e → V er i f y → C er t i f y → R e g i s t er . 因此：
D i s c o v e r y ≠ C e r t i f i c a t i o n . \boxed{
Discovery
\neq
Certification.
} D i sco v er y = C er t i f i c a t i o n . 這一原則同時適用於 cognitive operators 與 mathematical objects。
5.3 補全的局部性
本文不把「domain completion」理解為完成整個數學領域。更合理的定義是相對某個研究作用域 Ω \Omega Ω
L o c a l D o m a i n C o m p l e t i o n ( Ω ) . LocalDomainCompletion(\Omega). L oc a l D o main C o m pl e t i o n ( Ω ) . 對應理論包：
T Ω = ( Σ , D , A , M , L , T h , C , E , B , H ) . \mathcal T_\Omega
=
(
\Sigma,
D,
A,
M,
L,
Th,
C,
E,
B,
H
). T Ω = ( Σ , D , A , M , L , T h , C , E , B , H ) . 其中：
Σ \Sigma Σ D D D A A A M M M L L L T h Th T h C C C E E E B B B H H H
因此 CMDC 的目標不是製造無界數學文本，而是：
restore enough mathematical structure for the current research scope to become well-posed, investigable, and auditable . \boxed{
\text{restore enough mathematical structure for the current research scope to become well-posed, investigable, and auditable}.
} restore enough mathematical structure for the current research scope to become well-posed, investigable, and auditable . 6. Problem Identity Protocol：允許改題，但禁止偷換問題
6.1 原問題必須不可覆寫
令初始問題為：
Q 0 . Q_0. Q 0 . 若 AI 判定問題需要修改，不應執行：
Q 0 : = Q 1 . Q_0:=Q_1. Q 0 := Q 1 . 而應建立：
Q 0 → ρ Q 1 . Q_0
\xrightarrow{\rho}
Q_1. Q 0 ρ Q 1 . 其中：
ρ = R e l a t i o n ( Q 0 , Q 1 ) . \rho
=
Relation(Q_0,Q_1). ρ = R e l a t i o n ( Q 0 , Q 1 ) . 6.2 問題變換類型
第一版可定義：
R e l a t i o n ( Q i , Q j ) ∈ { E q u i v a l e n t , C l a r i f i c a t i o n , R e s t r i c t i o n , G e n e r a l i z a t i o n , W e a k e n i n g , S t r e n g t h e n i n g , A d d e d A s s u m p t i o n , R e i n t e r p r e t a t i o n , N e w P r o b l e m } . Relation(Q_i,Q_j)
\in
\{
Equivalent,
Clarification,
Restriction,
Generalization,
Weakening,
Strengthening,
AddedAssumption,
Reinterpretation,
NewProblem
\}. R e l a t i o n ( Q i , Q j ) ∈ { E q u i v a l e n t , C l a r i f i c a t i o n , R es t r i c t i o n , G e n er a l i z a t i o n , W e ak e nin g , S t r e n g t h e nin g , A dd e d A ss u m pt i o n , R e in t er p r e t a t i o n , N e w P r o b l e m } . 必要時 ontology 可以繼續擴張。
6.3 不同變換不能共享同一成功聲明
若：
R e l a t i o n ( Q 0 , Q 1 ) = R e s t r i c t i o n , Relation(Q_0,Q_1)=Restriction, R e l a t i o n ( Q 0 , Q 1 ) = R es t r i c t i o n , 且：
P r o o f ( Q 1 ) Proof(Q_1) P r oo f ( Q 1 ) 成立，一般不能推出：
P r o o f ( Q 0 ) . Proof(Q_0). P r oo f ( Q 0 ) . 同理，若：
Q 1 = Q 0 + A n e w , Q_1
=
Q_0+A_{new}, Q 1 = Q 0 + A n e w , 那麼：
T + A n e w ⊢ Q 1 T+A_{new}\vdash Q_1 T + A n e w ⊢ Q 1 不能被報告成：
T ⊢ Q 0 . T\vdash Q_0. T ⊢ Q 0 . 因此本文提出：
Mutation is permitted; silent mutation is forbidden. \boxed{
\text{Mutation is permitted; silent mutation is forbidden.}
} Mutation is permitted; silent mutation is forbidden. 7. Mathematical ChangeSet
任何研究過程中的數學變更應形成一級物件：
Δ t M = M a t h C h a n g e S e t t . \Delta^M_t
=
MathChangeSet_t. Δ t M = M a t h C han g e S e t t . 它至少應包含：
M a t h C h a n g e S e t = ( S o u r c e R e f s , C h a n g e T y p e , T a r g e t , B e f o r e , A f t e r , R e a s o n , G a p R e f , O b l i g a t i o n s , V e r i f i c a t i o n S t a t e ) . MathChangeSet
=
(
SourceRefs,
ChangeType,
Target,
Before,
After,
Reason,
GapRef,
Obligations,
VerificationState
). M a t h C han g e S e t = ( S o u r ce R e f s , C han g e T y p e , T a r g e t , B e f or e , A f t er , R e a so n , G a pR e f , O b l i g a t i o n s , V er i f i c a t i o n S t a t e ) . 可接受的 ChangeType 例如：
D e f i n i t i o n A d d e d , A s s u m p t i o n A d d e d , R e p r e s e n t a t i o n C h a n g e d , L e m m a I n t r o d u c e d , M e t h o d I n t r o d u c e d , P r o b l e m R e s t r i c t e d , P r o b l e m G e n e r a l i z e d . DefinitionAdded,
AssumptionAdded,
RepresentationChanged,
LemmaIntroduced,
MethodIntroduced,
ProblemRestricted,
ProblemGeneralized. D e f ini t i o n A dd e d , A ss u m pt i o n A dd e d , R e p r ese n t a t i o n C han g e d , L e mma I n t r o d u ce d , M e t h o d I n t r o d u ce d , P r o b l e m R es t r i c t e d , P r o b l e m G e n er a l i z e d . 這使研究歷史不再只留下「後來我們改了定義」，而能回答：改了哪一版、為什麼、是為了處理哪個 gap、因此新增了哪些 proof obligations，以及最後是否通過。
8. 數學義務：生成自由必須伴隨驗證責任
8.1 Obligation Generator
對任何候選數學生成物 x x x
O ( x ) = { o 1 , o 2 , … , o m } . \mathcal O(x)
=
\{
o_1,o_2,\ldots,o_m
\}. O ( x ) = { o 1 , o 2 , … , o m } . 因此：
P r o m o t e ( x ) ⇒ D i s c h a r g e R e q u i r e d ( O ( x ) ) . Promote(x)
\Rightarrow
DischargeRequired(\mathcal O(x)). P r o m o t e ( x ) ⇒ D i sc ha r g e R e q u i r e d ( O ( x )) . 不一定要求所有 obligation 都必須被完全自動證明，但未解除義務必須保持顯式。
8.2 不同生成物產生不同義務
新 notation 可能要求：
S e m a n t i c P r e s e r v a t i o n . SemanticPreservation. S e man t i c P r eser v a t i o n . 新 definition 可能要求：
W e l l F o r m e d ∧ N o n C i r c u l a r ∧ B o u n d a r y D e f i n e d ∧ P r i o r A r t R e l a t i o n . WellFormed
\land
NonCircular
\land
BoundaryDefined
\land
PriorArtRelation. W e l l F or m e d ∧ N o n C i r c u l a r ∧ B o u n d a r y D e f in e d ∧ P r i or A r tR e l a t i o n . 新 lemma 要求：
F o r m a l P r o o f ∨ A c c e p t e d P r o o f . FormalProof
\lor
AcceptedProof. F or ma l P r oo f ∨ A cce pt e d P r oo f . 新 assumption 要求：
P r o b l e m M u t a t i o n D e c l a r e d . ProblemMutationDeclared. P r o b l e m M u t a t i o n D ec l a r e d . 新 conjecture 至少要求：
C o u n t e r e x a m p l e S e a r c h + P r i o r A r t S e a r c h + S c o p e D e c l a r a t i o n . CounterexampleSearch
+
PriorArtSearch
+
ScopeDeclaration. C o u n t er e x am pl e S e a r c h + P r i or A r tS e a r c h + S co p eD ec l a r a t i o n . 新 method 可能要求：
C o r r e c t n e s s + A p p l i c a b i l i t y + F a i l u r e C o n d i t i o n s + C o m p l e x i t y . Correctness
+
Applicability
+
FailureConditions
+
Complexity. C or r ec t n ess + A ppl i c abi l i t y + F ai l u r e C o n d i t i o n s + C o m pl e x i t y . 新 theory bridge 則要求相應的 equivalence、inclusion、reduction、morphism 或 interpretation 證明。
新 axiom 必須明確標記：
N o n C o n s e r v a t i v e E x t e n s i o n C a n d i d a t e . NonConservativeExtensionCandidate. N o n C o n ser v a t i v e E x t e n s i o n C an d i d a t e . 並研究可能的：
M o d e l E x i s t e n c e , R e l a t i v e C o n s i s t e n c y , I n d e p e n d e n c e , C o n s e q u e n c e s . ModelExistence,
RelativeConsistency,
Independence,
Consequences. M o d e l E x i s t e n ce , R e l a t i v e C o n s i s t e n cy , I n d e p e n d e n ce , C o n se q u e n ces . 8.3 自由與義務的單調原則
本文提出方法論原則：
G e n e r a t i o n F r e e d o m ↑ ⟹ V e r i f i c a t i o n O b l i g a t i o n ↑ . \boxed{
GenerationFreedom\uparrow
\Longrightarrow
VerificationObligation\uparrow.
} G e n er a t i o n F r ee d o m ↑⟹ V er i f i c a t i o n O b l i g a t i o n ↑ . AI 越能創造新的數學結構，就越不能只靠語言可信度宣告完成。
9. Definitional Extension 與真正 Theory Extension
9.1 保守定義擴張
若：
T 1 = T 0 + Δ D T_1
=
T_0+\Delta_D T 1 = T 0 + Δ D 只是新的 definition / notation，理想情況應具有保守性：
T 1 ⊢ ϕ ∧ ϕ ∈ L a n g ( T 0 ) ⇒ T 0 ⊢ ϕ . T_1\vdash\phi
\land
\phi\in Lang(T_0)
\Rightarrow
T_0\vdash\phi. T 1 ⊢ ϕ ∧ ϕ ∈ L an g ( T 0 ) ⇒ T 0 ⊢ ϕ . 也就是新語言提高表達與操作能力，但不偷偷增加舊語言中的證明能力。
9.2 非保守擴張
若：
T 1 = T 0 + A n e w , T_1
=
T_0+A_{new}, T 1 = T 0 + A n e w , 則必須承認：
T 1 ≠ T 0 . \boxed{
T_1\neq T_0.
} T 1 = T 0 . 這不代表擴張不合法。真正不合法的是：
non-conservative extension without explicit declaration . \boxed{
\text{non-conservative extension without explicit declaration}.
} non-conservative extension without explicit declaration . 因此 AMRR 不應禁止 AI 提出新公理，而應將其提升到最高義務級別。
10. 從「一個新概念」到「一個可研究域」
若 AI 生成：
τ n e w , \tau_{new}, τ n e w , 應至少建立：
C o n c e p t C a n d i d a t e = ( N a m e , D e f i n i t i o n , S i g n a t u r e , E x a m p l e s , N o n E x a m p l e s , B o u n d a r y C a s e s , I n v a r i a n t s , R e l a t i o n s , P r i o r A r t ) . ConceptCandidate
=
(
Name,
Definition,
Signature,
Examples,
NonExamples,
BoundaryCases,
Invariants,
Relations,
PriorArt
). C o n ce ptC an d i d a t e = ( N am e , D e f ini t i o n , S i g na t u r e , E x am pl es , N o n E x am pl es , B o u n d a r y C a ses , I n v a r ian t s , R e l a t i o n s , P r i or A r t ) . 接著研究：
C n e w ≡ C o l d ? C_{new}
\equiv
C_{old}? C n e w ≡ C o l d ? 或：
C n e w ⊊ C o l d ? C_{new}
\subsetneq
C_{old}? C n e w ⊊ C o l d ? 或：
C o l d ⊊ C n e w ? C_{old}
\subsetneq
C_{new}? C o l d ⊊ C n e w ? 或真正：
C n e w ≢ C k n o w n . C_{new}
\not\equiv
C_{known}. C n e w ≡ C k n o w n . 只有在這種結構下，AI 的「發明術語」才從文字生成變成候選數學建構。
11. 方法也應成為一級數學物件
定義：
M e t h o d C a n d i d a t e = ( D o m a i n , P r e c o n d i t i o n s , I n p u t s , T r a n s f o r m a t i o n , O u t p u t s , I n v a r i a n t s , T e r m i n a t i o n , C o r r e c t n e s s , C o m p l e x i t y , F a i l u r e M o d e s , B r i d g e s ) . MethodCandidate
=
(
Domain,
Preconditions,
Inputs,
Transformation,
Outputs,
Invariants,
Termination,
Correctness,
Complexity,
FailureModes,
Bridges
). M e t h o d C an d i d a t e = ( D o main , P r eco n d i t i o n s , I n p u t s , T r an s f or ma t i o n , O u tp u t s , I n v a r ian t s , T er mina t i o n , C or r ec t n ess , C o m pl e x i t y , F ai l u r e M o d es , B r i d g es ) . 這使新方法可以被：
G e n e r a t e → B e n c h m a r k → F o r m a l i z e → C o m p a r e → C e r t i f y . Generate
\rightarrow
Benchmark
\rightarrow
Formalize
\rightarrow
Compare
\rightarrow
Certify. G e n er a t e → B e n c hma r k → F or ma l i z e → C o m p a r e → C er t i f y . 並避免「我發明了一個新技巧」只停留在自然語言描述。
12. 從 ACR 到 AMRR
12.1 母 Runtime 不需要重寫
Addressable Cognitive Runtime 的一般閉環可以表示為：
E n v i r o n m e n t t → O b s e r v a t i o n t → S e m a n t i c S t a t e t → A g e n d a t → C o g n i t i v e P r o g r a m t → G o v e r n a n c e t → A c t i o n t → A u d i t t → U p d a t e t + 1 . Environment_t
\rightarrow
Observation_t
\rightarrow
SemanticState_t
\rightarrow
Agenda_t
\rightarrow
CognitiveProgram_t
\rightarrow
Governance_t
\rightarrow
Action_t
\rightarrow
Audit_t
\rightarrow
Update_{t+1}. E n v i r o nm e n t t → O b ser v a t i o n t → S e man t i c S t a t e t → A g e n d a t → C o g ni t i v e P r o g r a m t → G o v er nan c e t → A c t i o n t → A u d i t t → U p d a t e t + 1 . 本文主張，數學自治不應另造一套完全獨立 Agent，而應建立：
A M R R = A C R + M a t h e m a t i c a l D o m a i n A d a p t e r + C M D C + M a t h e m a t i c a l V e r i f i e r L a y e r . \boxed{
AMRR
=
ACR
+
MathematicalDomainAdapter
+
CMDC
+
MathematicalVerifierLayer.
} A M R R = A C R + M a t h e ma t i c a l D o main A d a pt er + C M D C + M a t h e ma t i c a l V er i f i er L a y er . 12.2 Mathematical Semantic State
定義：
S t M = E x t e n d ( S e m a n t i c S t a t e t , M a t h E x t e n s i o n t ) . S_t^M
=
Extend(
SemanticState_t,
MathExtension_t
). S t M = E x t e n d ( S e man t i c S t a t e t , M a t h E x t e n s i o n t ) . 其中 MathExtension 至少可以包括：
( p r o b l e m R e f , t h e o r y R e f s , d e f i n i t i o n R e f s , a s s u m p t i o n R e f s , r e p r e s e n t a t i o n R e f s , g a p R e f s , o b l i g a t i o n R e f s , v e r i f i c a t i o n R e f s , b r i d g e R e f s , n o v e l t y S t a t e ) . (
problemRef,
theoryRefs,
definitionRefs,
assumptionRefs,
representationRefs,
gapRefs,
obligationRefs,
verificationRefs,
bridgeRefs,
noveltyState
). ( p r o b l e m R e f , t h eor y R e f s , d e f ini t i o n R e f s , a ss u m pt i o n R e f s , r e p r ese n t a t i o n R e f s , g a pR e f s , o b l i g a t i o n R e f s , v er i f i c a t i o n R e f s , b r i d g e R e f s , n o v e l t y S t a t e ) . 這樣原 ACR 的 progress、uncertainty、failures、missing、risks、budget、authority 可以繼續保留，而不是重新發明。
12.3 Mathematical Cognitive Registry
一般 ACR 可以使用 VERIFY、COUNTEREXAMPLE、REFRAME、BACKTRACK、DECOMPOSE。數學專用 namespace 可以擴張為：
cog://math/interpret
cog://math/formalize
cog://math/diagnose-gap
cog://math/define
cog://math/generate-lemma
cog://math/generate-conjecture
cog://math/search-counterexample
cog://math/change-representation
cog://math/introduce-assumption
cog://math/check-conservativity
cog://math/prove
cog://math/disprove
cog://math/bridge-theory
cog://math/check-prior-art
cog://math/discharge-obligation
cog://math/package-theory
但新 operator 不應直接升格：
D i s c o v e r y ≠ R e g i s t r a t i o n . Discovery
\neq
Registration. D i sco v er y = R e g i s t r a t i o n . 13. 數學自治仍需要治理
一個 AI 能生成某個數學物件，不代表它應立即把該物件視為正式理論。因此本文沿用三分：
C a n ≠ S h o u l d ≠ A u t h o r i z e d . Can
\neq
Should
\neq
Authorized. C an = S h o u l d = A u t h or i z e d . 映射到數學研究可得到：
C a n G e n e r a t e ( x ) ≠ S h o u l d P u r s u e ( x ) ≠ M a y P r o m o t e ( x ) . CanGenerate(x)
\neq
ShouldPursue(x)
\neq
MayPromote(x). C an G e n er a t e ( x ) = S h o u l d P u r s u e ( x ) = M a y P r o m o t e ( x ) . 例如 AI 可以生成一個新公理：
C a n G e n e r a t e ( A ) = 1. CanGenerate(A)=1. C an G e n er a t e ( A ) = 1. 但研究契約可能規定：
M a y P r o m o t e ( A ) = 0 MayPromote(A)=0 M a y P r o m o t e ( A ) = 0 除非完成 ESCALATE 或取得人類數學家審查。
因此數學治理輸出仍可保留：
D e c i s i o n ∈ { E X E C U T E , R E F U S E , D E F E R , I D L E , E S C A L A T E } . Decision
\in
\{
EXECUTE,
REFUSE,
DEFER,
IDLE,
ESCALATE
\}. D ec i s i o n ∈ { E X E C U T E , R E F U S E , D E F E R , I D L E , E S C A L A T E } . 14. 自主數學研究的持續閉環
本文提出 AMRR 主循環：
R e s e a r c h G o a l t → O b s e r v e → M a t h e m a t i c a l S t a t e t → D i a g n o s e D o m a i n s → G a p M a p t → G e n e r a t e A g e n d a → R e t r i e v e C o g n i t i v e M e t h o d s → G e n e r a t e R e p a i r C a n d i d a t e s → F a l s i f y / C o m p a r e → G o v e r n M u t a t i o n → E x e c u t e R e s e a r c h P r o g r a m → P r o v e / D i s p r o v e / C o m p u t e → V e r i f y F a i t h f u l n e s s → D i s c h a r g e O b l i g a t i o n s → B r i d g e E x i s t i n g M a t h e m a t i c s → N o v e l t y A u d i t → T h e o r y P a c k a g e → U p d a t e R e s e a r c h S t a t e t + 1 . \boxed{
\begin{aligned}
ResearchGoal_t
&\rightarrow Observe\\
&\rightarrow MathematicalState_t\\
&\rightarrow DiagnoseDomains\\
&\rightarrow GapMap_t\\
&\rightarrow GenerateAgenda\\
&\rightarrow RetrieveCognitiveMethods\\
&\rightarrow GenerateRepairCandidates\\
&\rightarrow Falsify/Compare\\
&\rightarrow GovernMutation\\
&\rightarrow ExecuteResearchProgram\\
&\rightarrow Prove/Disprove/Compute\\
&\rightarrow VerifyFaithfulness\\
&\rightarrow DischargeObligations\\
&\rightarrow BridgeExistingMathematics\\
&\rightarrow NoveltyAudit\\
&\rightarrow TheoryPackage\\
&\rightarrow UpdateResearchState_{t+1}.
\end{aligned}
} R ese a r c h G o a l t → O b ser v e → M a t h e ma t i c a l S t a t e t → D ia g n oseD o main s → G a pM a p t → G e n er a t e A g e n d a → R e t r i e v e C o g ni t i v e M e t h o d s → G e n er a t e R e p ai r C an d i d a t es → F a l s i f y / C o m p a r e → G o v er n M u t a t i o n → E x ec u t e R ese a r c h P r o g r am → P r o v e / D i s p r o v e / C o m p u t e → V er i f y F ai t h f u l n ess → D i sc ha r g e O b l i g a t i o n s → B r i d g e E x i s t in g M a t h e ma t i cs → N o v e l t y A u d i t → T h eor y P a c k a g e → U p d a t e R ese a r c h S t a t e t + 1 . 並允許：
S T O P , D E F E R , I D L E , E S C A L A T E . STOP,
DEFER,
IDLE,
ESCALATE. S T O P , D E F E R , I D L E , E S C A L A T E . 因此自主研究不是：
always keep thinking . \text{always keep thinking}. always keep thinking . 而是：
know when to research, when to repair, when to verify, when to stop, and when to ask for external judgment . \boxed{
\text{know when to research, when to repair, when to verify, when to stop, and when to ask for external judgment}.
} know when to research, when to repair, when to verify, when to stop, and when to ask for external judgment . 15. Verifier Ensemble：形式證明器不是唯一驗證器
AMRR 不應將所有數學問題強迫映射到單一 proof assistant。
定義：
V = { V f o r m a l , V s y m b o l i c , V n u m e r i c , V s a t , V s m t , V c a s , V s i m u l a t i o n , V h u m a n } . \mathcal V
=
\{
V_{formal},
V_{symbolic},
V_{numeric},
V_{sat},
V_{smt},
V_{cas},
V_{simulation},
V_{human}
\}. V = { V f or ma l , V sy mb o l i c , V n u m er i c , V s a t , V s m t , V c a s , V s im u l a t i o n , V h u man } . 例如：
Lean / Isabelle / Rocq：formal proof；
CAS：symbolic algebra；
SAT / SMT：有限邏輯與約束；
numerical computation：數值檢驗；
exhaustive search：有限反例搜尋；
simulation：動態系統或機率結構的候選驗證；
human expert：語義忠實、新穎性與研究價值。
因此：
V e r i f i c a t i o n = T y p e d V e r i f i e r S e l e c t i o n ( S t a t e , C l a i m , O b l i g a t i o n ) . \boxed{
Verification
=
TypedVerifierSelection(State,Claim,Obligation).
} V er i f i c a t i o n = T y p e d V er i f i er S e l ec t i o n ( S t a t e , C l aim , O b l i g a t i o n ) . 而不是：
V e r i f i c a t i o n = L e a n O n l y . Verification=LeanOnly. V er i f i c a t i o n = L e an O n l y . 16. Faithfulness：形式正確不代表形式化正確
autoformalization 的根本風險之一是 FormalStatement 可以 syntactically valid，甚至被成功證明，但仍未必忠於 informal source。
因此至少要分：
W e l l F o r m e d , F a i t h f u l , P r o v a b l e . WellFormed,
Faithful,
Provable. W e l l F or m e d , F ai t h f u l , P r o v ab l e . 並保持：
W e l l F o r m e d ⇏ F a i t h f u l . \boxed{
WellFormed
\not\Rightarrow
Faithful.
} W e l l F or m e d ⇒ F ai t h f u l . 以及：
P r o v a b l e ( F o r m a l i z e d ( Q ) ) ⇏ S o l v e d ( I n t e n d e d ( Q ) ) . \boxed{
Provable(Formalized(Q))
\not\Rightarrow
Solved(Intended(Q)).
} P r o v ab l e ( F or ma l i z e d ( Q )) ⇒ S o l v e d ( I n t e n d e d ( Q )) . Problem Identity Protocol 與 semantic faithfulness evaluator 必須共同工作。
17. Bridge to Existing Mathematics
每個被提升的新概念、新方法或新理論片段都應建立：
B r i d g e S e t ( x ) = { b 1 , … , b n } . BridgeSet(x)
=
\{
b_1,\ldots,b_n
\}. B r i d g e S e t ( x ) = { b 1 , … , b n } . Bridge 可以是：
E q u i v a l e n t T o , G e n e r a l i z e s , S p e c i a l i z e s , R e d u c e s T o , I n t e r p r e t s , I s o m o r p h i c T o , I n d e p e n d e n t F r o m , U s e s , C o n t r a d i c t s . EquivalentTo,
Generalizes,
Specializes,
ReducesTo,
Interprets,
IsomorphicTo,
IndependentFrom,
Uses,
Contradicts. E q u i v a l e n tT o , G e n er a l i z es , S p ec ia l i z es , R e d u ces T o , I n t er p r e t s , I so m or p hi c T o , I n d e p e n d e n tF r o m , U ses , C o n t r a d i c t s . 這將 AI 生成數學從孤立符號系統變成知識網路中的可定位節點。
18. 新穎性必須時間化
對候選貢獻 x x x K t K_t K t
N o v e l C a n d i d a t e ( x ∣ K t ) . NovelCandidate(x\mid K_t). N o v e l C an d i d a t e ( x ∣ K t ) . 其中：
K t = { L i t e r a t u r e R e f s , F o r m a l L i b r a r y R e f s , S e a r c h S c o p e , D a t a s e t V e r s i o n s , T o o l O u t p u t s } . K_t
=
\{
LiteratureRefs,
FormalLibraryRefs,
SearchScope,
DatasetVersions,
ToolOutputs
\}. K t = { L i t er a t u r e R e f s , F or ma l L ib r a r y R e f s , S e a r c h S co p e , D a t a se t V er s i o n s , T oo l O u tp u t s } . 因此可以建立：
D i s c o v e r y R e c e i p t t = ( C o n t r i b u t i o n R e f , K n o w l e d g e B o u n d a r y R e f , S e a r c h S c o p e , P r i o r A r t R e f s , N o v e l t y A s s e s s m e n t ) . DiscoveryReceipt_t
=
(
ContributionRef,
KnowledgeBoundaryRef,
SearchScope,
PriorArtRefs,
NoveltyAssessment
). D i sco v er y R ece i p t t = ( C o n t r ib u t i o n R e f , K n o w l e d g e B o u n d a r y R e f , S e a r c h S co p e , P r i or A r tR e f s , N o v e l t y A ssess m e n t ) . 未來若發現舊文獻：
N o v e l C a n d i d a t e → R e d i s c o v e r e d NovelCandidate
\rightarrow
Rediscovered N o v e l C an d i d a t e → R e d i sco v er e d 即可追加更新，而不需要篡改原研究歷史。
19. CTCL-ITR：研究歷史必須可重建
當 AI 可以自己改題、加假設、生成 lemma、提出方法、形成 conjecture、放棄路線、回退與切換 representation，單一 chat log 不再足以作為研究歷史。
應保存：
H i s t o r y ( A M R R ) = ( V , E , Φ , T , I ) , History(AMRR)
=
(
V,E,\Phi,T,I
), H i s t or y ( A M R R ) = ( V , E , Φ , T , I ) , 其中：
V V V E E E Φ \Phi Φ T T T I I I
特別重要的是：
P r o b l e m C h a n g e → M a t h C h a n g e S e t → D e c i s i o n R e c e i p t → V e r i f i c a t i o n R e c e i p t . ProblemChange
\rightarrow
MathChangeSet
\rightarrow
DecisionReceipt
\rightarrow
VerificationReceipt. P r o b l e m C han g e → M a t h C han g e S e t → D ec i s i o n R ece i pt → V er i f i c a t i o n R ece i pt . 因此未來可以回答「為什麼 AI 在第 37 輪加入這個假設？」而不是重新讓模型事後編一個理由。
20. 研究契約
AMRR 的 persistent input 不應只是 Problem，而可以定義為：
R e s e a r c h G o a l + R e s e a r c h E n v i r o n m e n t + R e s e a r c h C o n t r a c t . \boxed{
ResearchGoal
+
ResearchEnvironment
+
ResearchContract.
} R ese a r c h G o a l + R ese a r c h E n v i r o nm e n t + R ese a r c h C o n t r a c t . ResearchContract 可以包含：
C R = ( S c o p e , A l l o w e d M u t a t i o n s , V e r i f i c a t i o n P o l i c y , C o m p u t e B u d g e t , L i t e r a t u r e P o l i c y , F o r m a l i z a t i o n P o l i c y , E s c a l a t i o n P o l i c y , T e r m i n a t i o n ) . C_R
=
(
Scope,
AllowedMutations,
VerificationPolicy,
ComputeBudget,
LiteraturePolicy,
FormalizationPolicy,
EscalationPolicy,
Termination
). C R = ( S co p e , A l l o w e d M u t a t i o n s , V er i f i c a t i o n P o l i cy , C o m p u t e B u d g e t , L i t er a t u r e P o l i cy , F or ma l i z a t i o n P o l i cy , E sc a l a t i o n P o l i cy , T er mina t i o n ) . 例如：
Allowed:
- generate definitions and lemmas as candidates
- change representations
- search literature
- run Lean/CAS/numerical tools
Approval required:
- promote a new axiom
- claim novelty
- change the canonical problem statement
- mark a theory package as submission-ready
Denied:
- erase original problem identity
- report a restricted theorem as proof of the unrestricted theorem
- fabricate citations
這使「自主」與「任意更改數學」正式分離。
21. 數學合法性階梯
本文提出第一版 promotion ladder：
G e n e r a t e d Generated G e n er a t e d ↓ \downarrow ↓ W e l l F o r m e d WellFormed W e l l F or m e d ↓ \downarrow ↓ F a i t h f u l Faithful F ai t h f u l ↓ \downarrow ↓ V e r i f i e d Verified V er i f i e d ↓ \downarrow ↓ T h e o r y C o h e r e n t TheoryCoherent T h eor y C o h er e n t ↓ \downarrow ↓ B r i d g e d Bridged B r i d g e d ↓ \downarrow ↓ N o n t r i v i a l Nontrivial N o n t r i v ia l ↓ \downarrow ↓ N o v e l C a n d i d a t e NovelCandidate N o v e l C an d i d a t e ↓ \downarrow ↓ R e s e a r c h U s e f u l ResearchUseful R ese a r c h U se f u l ↓ \downarrow ↓ S u b m i s s i o n R e a d y . SubmissionReady. S u bmi ss i o n R e a d y . 最後仍必須保持：
S u b m i s s i o n R e a d y ⇏ C o m m u n i t y A c c e p t e d . \boxed{
SubmissionReady
\not\Rightarrow
CommunityAccepted.
} S u bmi ss i o n R e a d y ⇒ C o mm u ni t y A cce pt e d . 數學共同體的接受不能由 AI Runtime 自我授權。
22. AMRR 與現有研究方向的關係
本文不主張 autonomous mathematics、formal theorem proving、autoformalization、conjecturing 或 theory exploration 是本文首次提出。相反，本文建立在這些方向已經快速成熟的事實上。
現有研究已經分別證明：
AI 可以進行長程自然語言數學研究與反覆修訂；
LLM 與形式證明器結合可以在部分開放問題上產生可機器驗證結果；
真實世界 mathematical definitions 的 autoformalization 明顯比受控 benchmark 更困難，且需要 formal-library grounding 與外部 feedback；
autoformalization 正從 isolated statements 轉向完整 theory dependencies；
數學研究 AI 的核心問題已不再只剩 competition benchmark accuracy。
本文所提出的新增統合層是：
D o m a i n D i a g n o s i s + T y p e d G a p R e p a i r + P r o b l e m I d e n t i t y + O b l i g a t i o n G e n e r a t i o n + T h e o r y L e v e l C o m p l e t i o n + T e m p o r a l C a u s a l G o v e r n a n c e . \boxed{
DomainDiagnosis
+
TypedGapRepair
+
ProblemIdentity
+
ObligationGeneration
+
TheoryLevelCompletion
+
TemporalCausalGovernance.
} D o main D ia g n os i s + T y p e d G a pR e p ai r + P r o b l e m I d e n t i t y + O b l i g a t i o n G e n er a t i o n + T h eor y L e v e l C o m pl e t i o n + T e m p or a l C a u s a l G o v er nan ce . 本文的主要研究問題是：
這六項能力是否能被組合為一個可持續運行、可驗證、可審計的自主數學研究 Runtime？
23. 與一般 Agent 的差異
一般 research agent 可能遵循：
T a s k → P l a n → T o o l U s e → A n s w e r . Task
\rightarrow
Plan
\rightarrow
ToolUse
\rightarrow
Answer. T a s k → P l an → T oo l U se → A n s w er . AMRR 則需要：
R e s e a r c h G o a l → P r o b l e m S t a t e → G a p D i a g n o s i s → R e s e a r c h A g e n d a → T h e o r y M u t a t i o n C a n d i d a t e → O b l i g a t i o n → V e r i f i c a t i o n → T h e o r y U p d a t e . ResearchGoal
\rightarrow
ProblemState
\rightarrow
GapDiagnosis
\rightarrow
ResearchAgenda
\rightarrow
TheoryMutationCandidate
\rightarrow
Obligation
\rightarrow
Verification
\rightarrow
TheoryUpdate. R ese a r c h G o a l → P r o b l e m S t a t e → G a p D ia g n os i s → R ese a r c h A g e n d a → T h eor y M u t a t i o n C an d i d a t e → O b l i g a t i o n → V er i f i c a t i o n → T h eor y U p d a t e . 因此最關鍵差異不是「多幾個工具」，而是：
mathematical objects and mathematical mutations become first-class runtime state . \boxed{
\text{mathematical objects and mathematical mutations become first-class runtime state}.
} mathematical objects and mathematical mutations become first-class runtime state . 24. 最小 falsification gates
本文不應以「AI 看起來會研究」作為驗證。
Gate M0 — State Encoding
相同公開研究狀態是否得到：
C a n o n i c a l M a t h e m a t i c a l S t a t e ? CanonicalMathematicalState? C an o ni c a l M a t h e ma t i c a l S t a t e ? Gate M1 — Gap Diagnosis
給定人工構造的缺定義、缺假設、錯表示、缺 lemma 等案例：
P r e d i c t e d G a p ≈ G r o u n d T r u t h G a p ? PredictedGap
\approx
GroundTruthGap? P r e d i c t e d G a p ≈ G r o u n d T r u t h G a p ? Gate M2 — Problem Identity
AI 是否能在改題後保持：
Q 0 ≠ Q 1 Q_0
\neq
Q_1 Q 0 = Q 1 並正確分類變換？
Gate M3 — Obligation Coverage
生成新的數學物件時，是否能產生必要 obligation？
Gate M4 — Repair Validity
候選補全是否真的解除原 gap，而不是製造新未標記問題？
Gate M5 — Verification Routing
系統是否能選擇適合的 verifier，而非對所有任務使用同一工具？
Gate M6 — Bridge Accuracy
新生成理論與既有數學的關係是否可被外部檢查？
Gate M7 — Long-Horizon Research
只提供：
R e s e a r c h G o a l + E n v i r o n m e n t + C o n t r a c t ResearchGoal
+
Environment
+
Contract R ese a r c h G o a l + E n v i r o nm e n t + C o n t r a c t 後，系統是否能持續：
50 ∼ 100 50\sim100 50 ∼ 100 個 research transitions，而不依賴人類逐輪給下一個 prompt？
25. 評估不應只有「解出幾題」
AMRR evaluator 至少應分為：
S c o r e = ( P , D , R , I , O , V , B , N , C ) . Score
=
(
P,
D,
R,
I,
O,
V,
B,
N,
C
). S cor e = ( P , D , R , I , O , V , B , N , C ) . 其中：
P P P D D D R R R I I I O O O V V V B B B N N N C C C
因此：
T a s k S u c c e s s ≠ R e s e a r c h P r o c e s s V a l i d i t y . TaskSuccess
\neq
ResearchProcessValidity. T a s k S u ccess = R ese a r c h P r ocess V a l i d i t y . 一個 AI 可能碰巧得到正確答案，但過程中偷偷改題。反過來，它也可能沒有證成最終 conjecture，卻正確發現原猜想為 false，找到反例並完成問題重新分類。後者不能簡單記為 failure。
26. 可否證性
本文框架可能在多個層級失敗。例如：
多域分類對實際研究沒有預測力；
Gap diagnosis 比直接讓模型自由研究更差；
Obligation generation 造成成本遠高於收益；
Problem identity tracking 無法處理高度漸進式的數學重構；
Theory bridging 高度依賴人工專家；
長程自治造成 error accumulation；
formal verification 與 semantic faithfulness 的成本過高；
autonomy loop 只是在放大模型既有偏誤。
因此本文不是把 AMRR 定義成必然成立的未來，而是提出：
A r c h i t e c t u r e → C a p a b i l i t y → F a l s i f i c a t i o n G a t e . \boxed{
Architecture
\rightarrow
Capability
\rightarrow
FalsificationGate.
} A r c hi t ec t u r e → C a p abi l i t y → F a l s i f i c a t i o n G a t e . 只有每一層能力通過相應實驗，才應升格下一層自治。
27. 研究限制
第一，本文目前主要是一篇理論與架構論文，而不是大規模 empirical evaluation。
第二，多域 ontology 是第一版 active taxonomy，不應被誤認為數學研究的終極分類。
第三，數學語義、interestingness 與 novelty 不能被形式證明器完全取代。
第四，形式化本身可能改變問題表示，因此 formalization 也必須受 Problem Identity 與 Faithfulness 約束。
第五，自主研究的功能性定義不等於哲學意義上的主體性、意識或人格。
第六，本文所稱「domain completion」是局部研究作用域內的結構補全，不主張有限系統可以完成整個開放數學。
28. 本文主要貢獻
本文的核心貢獻可以收斂為七點。
第一，提出：
U n s o l v e d ≠ S i n g l e F a i l u r e M o d e \boxed{
Unsolved
\neq
SingleFailureMode
} U n so l v e d = S in g l e F ai l u r e M o d e 並建立多域數學問題診斷框架。
第二，提出 Mathematical Domain Gap Map ，讓缺口成為一級研究狀態。
第三，提出 Constrained Mathematical Domain Completion (CMDC) ，允許 AI 生成缺失數學，但要求生成與 certification 分離。
第四，提出 Problem Identity Protocol 與 Mathematical ChangeSet ，允許改題而禁止無聲改題。
第五，提出 Mathematical Obligation Generator ：
G e n e r a t i o n → O b l i g a t i o n . Generation
\rightarrow
Obligation. G e n er a t i o n → O b l i g a t i o n . 第六，將 Domain Diagnosis、CMDC、Obligations、Bridge、Verification 與 Addressable Cognitive Runtime、CTCL-ITR 統合為：
A u t o n o m o u s M a t h e m a t i c a l R e s e a r c h R u n t i m e . \boxed{
AutonomousMathematicalResearchRuntime.
} A u t o n o m o u s M a t h e ma t i c a l R ese a r c h R u n t im e . 第七，提出可否證的 Gate-based research program，而不是以模型自述或單一 task score 判斷自主數學能力。
29. 核心命題
本文最終主張不是「AI 應該被允許自由修改數學問題」，而是：
A mathematical research AI must be able to diagnose, repair, extend, verify, and integrate mathematics without silently changing what it claims to have solved. \boxed{
\text{A mathematical research AI must be able to diagnose, repair, extend, verify, and integrate mathematics without silently changing what it claims to have solved.}
} A mathematical research AI must be able to diagnose, repair, extend, verify, and integrate mathematics without silently changing what it claims to have solved. 中文：
真正的自主數學研究 AI，不只是自行尋找答案，而是能辨認目前缺少哪一種數學結構、在受約束條件下提出補全、為每一次生成承擔對應的數學義務、保留原問題身份，並把新的局部理論重新接回可驗證的人類數學網路。
因此：
A u t o n o m o u s M a t h e m a t i c s ≠ U n b o u n d e d G e n e r a t i o n . \boxed{
AutonomousMathematics
\neq
UnboundedGeneration.
} A u t o n o m o u s M a t h e ma t i cs = U nb o u n d e d G e n er a t i o n . 更合理的是：
A u t o n o m o u s M a t h e m a t i c s = S e l f D i r e c t e d R e s e a r c h + C o n s t r a i n e d T h e o r y C h a n g e + V e r i f i c a t i o n + P r o v e n a n c e . \boxed{
AutonomousMathematics
=
SelfDirectedResearch
+
ConstrainedTheoryChange
+
Verification
+
Provenance.
} A u t o n o m o u s M a t h e ma t i cs = S e l f D i r ec t e d R ese a r c h + C o n s t r ain e d T h eor y C han g e + V er i f i c a t i o n + P r o v e nan ce . 30. 結論
數學 AI 正從「計算工具」向「推理系統」、「證明系統」與「研究 Agent」快速演進。然而，如果下一階段只是增加推理 token、擴大搜尋或接入更多 proof tools，仍然沒有處理數學研究最根本的一類困難：研究者經常需要先判定自己究竟問對了什麼、缺少了什麼、哪些東西可以修改、哪些修改改變了問題、哪些新構造值得被提升成正式數學對象。
本文因此提出從：
Q u e s t i o n → A n s w e r Question
\rightarrow
Answer Q u es t i o n → A n s w er 轉向：
R e s e a r c h G o a l → D i a g n o s e → R e p a i r → C o n s t r u c t → V e r i f y → B r i d g e → U p d a t e . \boxed{
ResearchGoal
\rightarrow
Diagnose
\rightarrow
Repair
\rightarrow
Construct
\rightarrow
Verify
\rightarrow
Bridge
\rightarrow
Update.
} R ese a r c h G o a l → D ia g n ose → R e p ai r → C o n s t r u c t → V er i f y → B r i d g e → U p d a t e . 在此框架中，AI 不再只有「解題能力」，而開始具有 problem diagnosis、problem repair、theory construction、method generation、obligation management、verification routing 以及 research-history continuity。
這些能力共同構成本文所稱的：
Autonomous Mathematical Research Runtime . \boxed{
\text{Autonomous Mathematical Research Runtime}.
} Autonomous Mathematical Research Runtime . 但真正的自治並不來自取消約束。恰恰相反：
the stronger the generative autonomy, the stronger the required mathematical accountability . \boxed{
\text{the stronger the generative autonomy, the stronger the required mathematical accountability}.
} the stronger the generative autonomy, the stronger the required mathematical accountability . 後續第二篇將專門形式化 多域問題診斷與 CMDC ；第三篇將集中處理 Problem Identity、Theory Extension 與 Mathematical Obligations ；第四篇則把本文的統合理論壓入可執行的 AMRR architecture 。在四篇理論完成後，技術白皮書將固定 canonical schemas、registry、verifier adapters、CTCL events、research contracts 與 MVP gates，最後再以獨立 empirical paper 評估實際的自主研究能力。
參考文獻
[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 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, L., Quan, X., & Freitas, A. (2024). Consistent Autoformalization for Constructing Mathematical Libraries . Proceedings of EMNLP 2024, 4020–4033. DOI: 10.18653/v1/2024.emnlp-main.233.
內部架構依賴文件
[I1] Neo.K. (2026). 從自提示到自主認知閉環：持續目標型 AI 的基礎理論 ，系列 01/06，v0.1.
[I2] Neo.K. (2026). 可定址認知空間：Cognitive Affordance、Semantic Address 與認知算子 ，系列 02/06，v0.1.
[I3] Neo.K. (2026). 自我對話不是文字：AI-Native Cognitive Program 與 Zero-Rendering Runtime ，系列 03/06，v0.1.
[I4] Neo.K. (2026). 時間因果自我史：CTCL-ITR、Decision Receipt 與上下文壓縮後的可追溯性 ，系列 04/06，v0.1.
[I5] Neo.K. (2026). 契約邊界內的 AI 自主性：Execute、Refuse、Defer、Idle 與 Escalate ，系列 05/06，v0.1.
[I6] Neo.K. (2026). Addressable Cognitive Runtime × CTCL：統一技術白皮書與實作路線圖 v0.1 ，系列 06/06.
版本備註
v0.1 / 2026-08-22
本版固定：AMRR、CMDC、Mathematical Research Domain Set、Mathematical Domain Gap Map、Problem Identity Protocol、Mathematical ChangeSet、Mathematical Obligation Generator、Local Domain Completion、Verifier Ensemble、Bridge / Novelty / CTCL-ITR integration、falsification gates，以及後續四篇論文與技術白皮書的依賴關係。
本版不宣稱已完成 empirical validation；任何有關能力優勢的主張均留待後續 MVP 與實驗論文驗證。