數學研究空間方法論
從線性證明文本到可計算的動態證明空間
Mathematical Research Space Methodology: From Linear Proof Texts to Computable Dynamic Proof Spaces
作者： Neo.K機構： EveMissLab／一言諾科技有限公司
摘要
傳統數學通常以「定義—引理—定理—證明」作為主要知識表示形式，其核心判斷可以抽象為：
Γ ⊢ P . \Gamma \vdash P. Γ ⊢ P . 這一形式極其適合描述一個已完成或局部完成的證明，卻不擅長表達大型長期研究過程中同時存在的多條證明路線、局部阻礙、失敗分支、條件式結論、表示轉換、跨領域橋接、未清償證明義務、歷史版本、重新開啟與相對閉包等結構。
當研究問題的文獻規模、證明路線數量與形式表示數量持續增加時，數學研究本身逐漸呈現出一個高維、非線性、動態、部分可觀察的狀態空間。若仍僅使用線性文本與人類工作記憶維護此空間，將不可避免地產生大量有損壓縮，例如「這條路大概不行」、「那個方法已經被證明失敗」、「目前只剩幾種可能」等無法精確追溯其作用域與證據層級的研究敘述。
本文提出一套通用的 Mathematical Research Space Methodology（MRSM，數學研究空間方法論） 。其核心思想不是單純「用圖論表示數學」，而是將數學研究過程本身提升為一級數學與計算對象，使命題、證明路線、阻礙、survivor、frontier、scope、representation、certificate、proof debt、reopening、transfer 與 closure 均成為可型別化、可追溯、可重播、可驗證的狀態單元。
在此方法論下，一個數學問題不再只是等待某個證明文字完成的單一命題，而是一個隨時間演化的動態證明空間：
M Q ( t ) . \mathcal M_Q(t). M Q ( t ) . 研究目標也不再僅是「找到一份證明」，而包含建立、觀察、約化、切割、阻斷、重開與最終閉合整個可容許研究空間。
本文建立 MRSM 的基本對象、狀態語義、圖結構、閉包條件、權限層級、投影原則與機器執行框架，並指出此方法尤其適合 AI、形式驗證系統、大型數學知識庫與長期開放問題研究。
關鍵詞： 數學研究空間、證明圖、閉包、圖論、證明理論、形式驗證、研究方法論、AI 數學、知識圖譜、動態證明系統
1. 問題：證明是數學物件，研究過程卻通常不是
數學最典型的形式為：
Γ ⊢ P , \Gamma\vdash P, Γ ⊢ P , 其中：
Γ \Gamma Γ (P) 為欲建立的命題。
此形式對完成的數學推導十分有效。
然而真實研究通常不是：
Γ → P \Gamma\to P Γ → P 這樣的一條單線。
更常見的是：
P ⇝ { R 1 , R 2 , … , R n } , P
\rightsquigarrow
\{
R_1,R_2,\ldots,R_n
\}, P ⇝ { R 1 , R 2 , … , R n } , 其中不同 R i R_i R i
每條 route 又可能：
依賴不同假設；
採用不同 representation；
遇到不同 obstruction；
只在部分 scope 成立；
被某個 no-go theorem 阻斷；
在新的 lemma 出現後重新開啟；
與其他 route 合流；
僅形成 conditional closure；
或只證明其中一個 quotient class 不可行。
因此真正的研究狀態更接近：
Research State = Claims + Routes + Dependencies + Obstructions + Frontiers + Certificates + Debts + History . \boxed{
\text{Research State}
=
\text{Claims}
+
\text{Routes}
+
\text{Dependencies}
+
\text{Obstructions}
+
\text{Frontiers}
+
\text{Certificates}
+
\text{Debts}
+
\text{History}.
} Research State = Claims + Routes + Dependencies + Obstructions + Frontiers + Certificates + Debts + History . 傳統論文可以描述這些資訊，但通常沒有把它們提升為具有明確語義的第一級數學物件。
2. 核心命題：研究過程本身應被物件化
MRSM 的第一原則為：
Mathematical Research Process ⟶ Mathematical Research Object . \boxed{
\textbf{Mathematical Research Process}
\longrightarrow
\textbf{Mathematical Research Object}.
} Mathematical Research Process ⟶ Mathematical Research Object . 這並不表示研究者的心理活動本身需要形式化。
真正需要物件化的是可外部觀察與驗證的研究結構，例如：
Claim , Assumption , Lemma , Proof Route , Obstruction , No-Go , Survivor , Frontier , Representation , Bridge , Certificate , Proof Debt , Reopening Event . \begin{aligned}
&\text{Claim},\\
&\text{Assumption},\\
&\text{Lemma},\\
&\text{Proof Route},\\
&\text{Obstruction},\\
&\text{No-Go},\\
&\text{Survivor},\\
&\text{Frontier},\\
&\text{Representation},\\
&\text{Bridge},\\
&\text{Certificate},\\
&\text{Proof Debt},\\
&\text{Reopening Event}.
\end{aligned} Claim , Assumption , Lemma , Proof Route , Obstruction , No-Go , Survivor , Frontier , Representation , Bridge , Certificate , Proof Debt , Reopening Event . 因此研究狀態可以表示成：
M Q ( t ) = ⟨ V t , E t , Σ t , C t , D t , F t , H t ⟩ , \mathfrak M_Q(t)
=
\langle
V_t,
E_t,
\Sigma_t,
\mathcal C_t,
\mathcal D_t,
\mathcal F_t,
\mathcal H_t
\rangle, M Q ( t ) = ⟨ V t , E t , Σ t , C t , D t , F t , H t ⟩ , 其中：
V t V_t V t E t E_t E t Σ t \Sigma_t Σ t C t \mathcal C_t C t D t \mathcal D_t D t F t \mathcal F_t F t H t \mathcal H_t H t
3. 為什麼單純的 theorem graph 還不夠
「用圖表示數學」本身並不是新的思想。
可以建立：
Theorem A → Lemma B → Theorem C . \text{Theorem A}
\to
\text{Lemma B}
\to
\text{Theorem C}. Theorem A → Lemma B → Theorem C . 但一般 theorem dependency graph 主要描述：
what depends on what . \boxed{
\text{what depends on what}.
} what depends on what . MRSM 所需要描述的卻更多：
what is possible , what has failed , why it failed , under which scope , what still survives . \boxed{
\text{what is possible},
\quad
\text{what has failed},
\quad
\text{why it failed},
\quad
\text{under which scope},
\quad
\text{what still survives}.
} what is possible , what has failed , why it failed , under which scope , what still survives . 例如：
R 1 → blocked by O 1 ⊥ R_1
\xrightarrow{\text{blocked by }O_1}
\bot R 1 blocked by O 1 ⊥ 並不代表：
P = f a l s e . P=\mathrm{false}. P = false . 因此必須嚴格區分：
R o u t e B l o c k e d ≠ C l a i m R e f u t e d ≠ B r a n c h C l o s e d ≠ P r o b l e m C l o s e d . \boxed{
\mathsf{RouteBlocked}
\neq
\mathsf{ClaimRefuted}
\neq
\mathsf{BranchClosed}
\neq
\mathsf{ProblemClosed}.
} RouteBlocked = ClaimRefuted = BranchClosed = ProblemClosed . 這是研究空間方法論與一般 dependency graph 最重要的差異之一。
4. Typed Research Graph
令一個數學研究問題 (Q) 的研究圖為：
G Q = ( V , E , τ V , τ E , σ , χ ) . \mathcal G_Q
=
(V,E,\tau_V,\tau_E,\sigma,\chi). G Q = ( V , E , τ V , τ E , σ , χ ) . 其中：
τ V : V → T V \tau_V:V\to\mathcal T_V τ V : V → T V 為節點型別，例如：
T V = { CLAIM , LEMMA , ROUTE , OBSTRUCTION , SURVIVOR , FRONTIER , CERTIFICATE , DEBT , BRIDGE } . \mathcal T_V=
\{
\text{CLAIM},
\text{LEMMA},
\text{ROUTE},
\text{OBSTRUCTION},
\text{SURVIVOR},
\text{FRONTIER},
\text{CERTIFICATE},
\text{DEBT},
\text{BRIDGE}
\}. T V = { CLAIM , LEMMA , ROUTE , OBSTRUCTION , SURVIVOR , FRONTIER , CERTIFICATE , DEBT , BRIDGE } . 邊也具有型別：
τ E : E → T E , \tau_E:E\to\mathcal T_E, τ E : E → T E , 例如：
T E = { IMPLIES , DEPENDS_ON , ASSUMES , REFINES , BLOCKS , REFUTES , SURVIVES , REDUCES_TO , BRIDGES_TO , VALIDATED_BY , REOPENS , NEXT_FRONTIER } . \begin{aligned}
\mathcal T_E=\{
&\text{IMPLIES},
\text{DEPENDS\_ON},
\text{ASSUMES},
\text{REFINES},\\
&\text{BLOCKS},
\text{REFUTES},
\text{SURVIVES},
\text{REDUCES\_TO},\\
&\text{BRIDGES\_TO},
\text{VALIDATED\_BY},
\text{REOPENS},
\text{NEXT\_FRONTIER}
\}.
\end{aligned} T E = { IMPLIES , DEPENDS_ON , ASSUMES , REFINES , BLOCKS , REFUTES , SURVIVES , REDUCES_TO , BRIDGES_TO , VALIDATED_BY , REOPENS , NEXT_FRONTIER } . 這樣一來：
A BLOCKS B A\ \text{BLOCKS}\ B A BLOCKS B 與：
A REFUTES B A\ \text{REFUTES}\ B A REFUTES B 在機器層不再可能被當成同一件事。
5. Status 不再只有 True / False
大型研究問題不適合只有：
{ T R U E , F A L S E , U N K N O W N } . \{\mathrm{TRUE},\mathrm{FALSE},\mathrm{UNKNOWN}\}. { TRUE , FALSE , UNKNOWN } . MRSM 建議至少保留：
Σ = { U N V E R I F I E D , U N K N O W N , O P E N , C O N D I T I O N A L , B L O C K E D , C L O S E D + , C L O S E D − , S T A L E , R E O P E N E D , S U P E R S E D E D } . \Sigma=
\{
\mathrm{UNVERIFIED},
\mathrm{UNKNOWN},
\mathrm{OPEN},
\mathrm{CONDITIONAL},
\mathrm{BLOCKED},
\mathrm{CLOSED}^{+},
\mathrm{CLOSED}^{-},
\mathrm{STALE},
\mathrm{REOPENED},
\mathrm{SUPERSEDED}
\}. Σ = { UNVERIFIED , UNKNOWN , OPEN , CONDITIONAL , BLOCKED , CLOSED + , CLOSED − , STALE , REOPENED , SUPERSEDED } . 其中：
B L O C K E D ≠ C L O S E D − . \mathrm{BLOCKED}
\neq
\mathrm{CLOSED}^{-}. BLOCKED = CLOSED − . 因為 blocked 可能只是：
在目前假設、representation、scope 與 proof technique 下無法繼續。
而：
C L O S E D − \mathrm{CLOSED}^{-} CLOSED − 才表示具有適格證據的否定性閉包。
6. Scope 是證明的一部分，而不是附註
數學論文經常在自然語言中使用：
globally,
generally,
universally,
for arbitrary data.
但「global」本身必須被型別化。
定義：
S c o p e ( P ) = ⟨ S t , S x , S e q , S d a t a , S b d r y , S r e g , S r e p ⟩ . \mathsf{Scope}(P)
=
\langle
S_t,
S_x,
S_{\mathrm{eq}},
S_{\mathrm{data}},
S_{\mathrm{bdry}},
S_{\mathrm{reg}},
S_{\mathrm{rep}}
\rangle. Scope ( P ) = ⟨ S t , S x , S eq , S data , S bdry , S reg , S rep ⟩ . 因此：
Theorem Strengthening ≠ Scope Expansion . \boxed{
\text{Theorem Strengthening}
\neq
\text{Scope Expansion}.
} Theorem Strengthening = Scope Expansion . 一個在固定 representation、固定邊界或有限參數區間成立的 theorem，不得因語言上的「global」被升格到其他 domain。
7. Candidate 與 Native Mathematical State 必須分離
當大量自然語言論文進入研究空間時，最危險的操作是：
paper says PROVED ⇒ system status = PROVED . \text{paper says PROVED}
\Rightarrow
\text{system status = PROVED}. paper says PROVED ⇒ system status = PROVED . MRSM 要求：
Source Label → Candidate → Audit → Native Status . \boxed{
\text{Source Label}
\to
\text{Candidate}
\to
\text{Audit}
\to
\text{Native Status}.
} Source Label → Candidate → Audit → Native Status . 例如：
NO-GO → O b s t r u c t i o n C a n d i d a t e . \texttt{NO-GO}
\to
\mathsf{ObstructionCandidate}. NO-GO → ObstructionCandidate . 而不是：
NO-GO → P a r e n t R e f u t e d . \texttt{NO-GO}
\to
\mathsf{ParentRefuted}. NO-GO → ParentRefuted . 同樣：
SURVIVOR \texttt{SURVIVOR} SURVIVOR 只是 candidate role。
它首先表示：
在當前已知 obstruction 下仍未排除。
並不表示：
survivor is realizable . \text{survivor is realizable}. survivor is realizable . 8. Certificate-Carrying Mathematics
任何會改變高權限 mathematical state 的操作，都應附帶 certificate。
令：
C e r t ( P ) = ⟨ subject , scope , evidence , authority , version ⟩ . \mathsf{Cert}(P)
=
\langle
\text{subject},
\text{scope},
\text{evidence},
\text{authority},
\text{version}
\rangle. Cert ( P ) = ⟨ subject , scope , evidence , authority , version ⟩ . 於是：
Status Mutation ⇒ Certificate Requirement . \boxed{
\text{Status Mutation}
\Rightarrow
\text{Certificate Requirement}.
} Status Mutation ⇒ Certificate Requirement . 例如：
C l o s e P o s i t i v e ( P ) \mathsf{ClosePositive}(P) ClosePositive ( P ) 不能只接收：
status = proved
而必須要求適格 certificate。
因此研究 runtime 應 fail closed：
¬ V a l i d C e r t ⇒ N o M u t a t i o n . \neg\mathsf{ValidCert}
\Rightarrow
\mathsf{NoMutation}. ¬ ValidCert ⇒ NoMutation . 9. Authority 必須與 Status 分離
兩個都標為：
C L O S E D + \mathrm{CLOSED}^{+} CLOSED + 的 theorem 可能具有完全不同的 epistemic authority。
例如：
A u t h o r i t y = { D I S P L A Y , R E S E A R C H , A U D I T , P R O O F , F O R M A L _ P R O O F } . \mathsf{Authority}
=
\{
\mathrm{DISPLAY},
\mathrm{RESEARCH},
\mathrm{AUDIT},
\mathrm{PROOF},
\mathrm{FORMAL\_PROOF}
\}. Authority = { DISPLAY , RESEARCH , AUDIT , PROOF , FORMAL_PROOF } . 一個 source-internal theorem 可以是：
C L O S E D + + A U D I T . \mathrm{CLOSED}^{+}
+
\mathrm{AUDIT}. CLOSED + + AUDIT . 經獨立 verifier 後可以變成：
C L O S E D + + P R O O F . \mathrm{CLOSED}^{+}
+
\mathrm{PROOF}. CLOSED + + PROOF . 經 proof-assistant kernel 後可以再增加：
F O R M A L _ P R O O F . \mathrm{FORMAL\_PROOF}. FORMAL_PROOF . 但：
A u t h o r i t y U p g r a d e ≠ S c o p e E x p a n s i o n . \boxed{
\mathsf{AuthorityUpgrade}
\neq
\mathsf{ScopeExpansion}.
} AuthorityUpgrade = ScopeExpansion . 證明變得更可信，不表示它證明了更大的命題。
10. Closure 是 Research Space 的核心操作
傳統數學通常關心：
P 是否已證明？ P\text{ 是否已證明？} P 是否已證明？ MRSM 進一步關心：
相對於目前可容許研究空間，是否已經不存在未處理的合法逃逸路線？
令：
Ω D , Θ , A a d m ( Q ) \Omega^{\rm adm}_{D,\Theta,\mathcal A}(Q) Ω D , Θ , A adm ( Q ) 表示在：
domain (D)；
theory Θ \Theta Θ
admissibility rule A \mathcal A A
下的可容許研究空間。
則 relative closure 可以表示為：
C D , Θ , A r e l ( Q ) . \mathfrak C^{\rm rel}_{D,\Theta,\mathcal A}(Q). C D , Θ , A rel ( Q ) . 但必須保持：
Relative Closure ≠ Absolute Mathematical Completeness . \boxed{
\text{Relative Closure}
\neq
\text{Absolute Mathematical Completeness}.
} Relative Closure = Absolute Mathematical Completeness . 因為：
Ω o b s ≠ Ω a d m ≠ Ω m a t h . \Omega^{\rm obs}
\neq
\Omega^{\rm adm}
\neq
\Omega^{\rm math}. Ω obs = Ω adm = Ω math . 我們看到的研究空間不等於全部可容許路線；
全部可容許路線也不等於真正所有可能數學結構。
11. Frontier 比「尚未證明」更有資訊
令目前研究 frontier 為：
∂ ∗ M Q . \partial^\ast \mathfrak M_Q. ∂ ∗ M Q . 它不是所有 OPEN nodes。
而是：
目前尚未解決，且若其狀態改變，最可能實質改變整體 closure 結果的最小高價值集合。
因此研究方向可以從模糊的：
下一步再找新的方法。
改成：
compute current frontier → attack minimal unresolved cut . \boxed{
\text{compute current frontier}
\to
\text{attack minimal unresolved cut}.
} compute current frontier → attack minimal unresolved cut . 這使研究計畫本身開始具有算法性。
12. Proof Debt
每個尚未完成的 bridge、assumption、transfer、representation mapping 都可以形成：
d i ∈ D . d_i\in\mathcal D. d i ∈ D . 例如：
d s c o p e , d t r a n s f e r , d c o m p l e t e n e s s , d r e p r e s e n t a t i o n . d_{\rm scope},
\qquad
d_{\rm transfer},
\qquad
d_{\rm completeness},
\qquad
d_{\rm representation}. d scope , d transfer , d completeness , d representation . 因此：
Debt cannot disappear by description . \boxed{
\text{Debt cannot disappear by description}.
} Debt cannot disappear by description . 如果一個 proof route 從：
[
A
]
經過 transformation 到：
[
B,
]
未清償的 debt 要麼：
被 discharge；
被合法 transfer；
被 split；
但不能單純消失。
13. Reopening 是正常數學操作
傳統研究敘事常把 theorem landscape 想像成單調成長：
unknown → proved . \text{unknown}
\to
\text{proved}. unknown → proved . 但真實研究具有：
blocked → reopened , \text{blocked}
\to
\text{reopened}, blocked → reopened , 以及：
apparently closed → scope narrowed → open again . \text{apparently closed}
\to
\text{scope narrowed}
\to
\text{open again}. apparently closed → scope narrowed → open again . 因此 MRSM 使用事件式時間：
M t = R e p l a y ( L e d g e r ≤ t , P o l i c y t ) . \mathfrak M_t
=
\mathsf{Replay}
(
\mathsf{Ledger}_{\le t},
\mathsf{Policy}_t
). M t = Replay ( Ledger ≤ t , Policy t ) . 這意味著狀態不是不可解釋地「被改掉」；
任何 reopening 都具有歷史 lineage。
14. Event-Sourced Mathematical Research
研究空間可以採：
L 0 = Canonical Event Ledger \boxed{
L_0=\text{Canonical Event Ledger}
} L 0 = Canonical Event Ledger L 1 = Native Mathematical State \boxed{
L_1=\text{Native Mathematical State}
} L 1 = Native Mathematical State L 2 = Research Views \boxed{
L_2=\text{Research Views}
} L 2 = Research Views 任何狀態都由：
R e p l a y ( L 0 ) \mathsf{Replay}(L_0) Replay ( L 0 ) 重建。
因此：
R e p l a y ( L ) = S \boxed{
\mathsf{Replay}(L)
=
S
} Replay ( L ) = S 成為研究完整性的基本驗證。
如果 replay 後 state 不同：
R U N T I M E _ I N C O N S I S T E N T . \boxed{
\mathsf{RUNTIME\_INCONSISTENT}.
} RUNTIME_INCONSISTENT . 15. Projection 不等於 Native Research Space
人類不可能直接閱讀完整研究圖。
因此需要：
Π : M → V \Pi:
\mathfrak M
\to
\mathcal V Π : M → V 把 native mathematical state 投影成：
論文；
frontier map；
proof graph；
table；
dashboard；
AI context；
human-readable explanation。
但必須：
Π ( M ) ≠ M . \boxed{
\Pi(\mathfrak M)
\neq
\mathfrak M.
} Π ( M ) = M . 這一點對 AI 特別重要。
因為文字 context 本身也是一種投影。
如果 AI 把當前 context 誤認為完整 research state，就會出現：
context omission ⇒ false mathematical closure . \text{context omission}
\Rightarrow
\text{false mathematical closure}. context omission ⇒ false mathematical closure . 16. 為什麼以前沒有自然發展成這套方法
這並不是因為數學家沒有圖論概念。
真正的限制至少有四個。
16.1 人類認知容量
人類可以維持有限數量的 active proof states。
若研究空間包含：
10 3 ∼ 10 5 10^3
\sim
10^5 1 0 3 ∼ 1 0 5 個互相關聯節點，人類必須進行大量有損壓縮。
例如：
「這條路基本不行。」
在 MRSM 中應拆成：
Route R + Obstruction O + Scope S + Status BLOCKED . \text{Route }R
+
\text{Obstruction }O
+
\text{Scope }S
+
\text{Status BLOCKED}. Route R + Obstruction O + Scope S + Status BLOCKED . 16.2 傳統載體是線性的
紙本論文與 PDF 基本是：
linear sequence . \text{linear sequence}. linear sequence . 研究空間卻更接近：
typed hypergraph + state machine + ledger . \text{typed hypergraph}
+
\text{state machine}
+
\text{ledger}. typed hypergraph + state machine + ledger . 在沒有 database、version control、symbolic engine 與 formal runtime 時，維護此結構的成本過高。
16.3 知識密度不足
若一個問題只有少量結果，單一專家可以在腦中維護主要 landscape。
當研究累積成：
10 3 + 10^3+ 1 0 3 + 篇 paper、
大量不同 representation、
數百個 no-go 與 survivor，
才真正出現 machine-addressable research space 的需求。
16.4 「研究過程」未被視為數學物件
傳統形式數學主要研究：
Γ ⊢ P . \Gamma\vdash P. Γ ⊢ P . 但較少研究：
(P) 有多少合法 proof route？
哪些 route 已 blocked？
哪些 obstruction 只作用於 quotient class？
哪些 debt 尚未 discharge？
是否仍存在未觀察的 escape class？
也就是：
Proof 被形式化了， Proof Search Space 卻通常沒有。 \boxed{
\text{Proof}
\text{ 被形式化了，}
\quad
\text{Proof Search Space}
\text{ 卻通常沒有。}
} Proof 被形式化了， Proof Search Space 卻通常沒有。 MRSM 所做的正是補上這一層。
17. 為什麼 AI 改變了可行性
這套方法對人類而言管理成本極高。
但對：
AI + database + graph runtime + formal verifier \text{AI}
+
\text{database}
+
\text{graph runtime}
+
\text{formal verifier} AI + database + graph runtime + formal verifier 而言，恰好是天然適合的工作。
AI 可以維護：
幾萬個 nodes；
幾十萬條 edges；
不同 scope；
大量 proof debt；
historical reopenings；
certificate lineage。
因此 AI 的角色不必只是：
幫數學家寫下一行證明。
更重要的可能是：
維護整個數學研究空間。 \boxed{
\textbf{維護整個數學研究空間。}
} 維護整個數學研究空間。 人類研究者則可以集中於：
創造新 representation；
發現新 invariants；
建立關鍵 bridge；
選擇 frontier；
判斷值得投入的 route。
18. AI-Native Mathematical Research
在這種架構下，未來的 AI 數學系統可以執行：
O b s e r v e \mathsf{Observe} Observe 目前 research graph；
F r o n t i e r D e t e c t \mathsf{FrontierDetect} FrontierDetect 計算最小 unresolved frontier；
R o u t e G e n e r a t e \mathsf{RouteGenerate} RouteGenerate 提出新 proof route；
O b s t r u c t i o n S e a r c h \mathsf{ObstructionSearch} ObstructionSearch 搜尋 no-go；
C e r t i f i c a t e V e r i f y \mathsf{CertificateVerify} CertificateVerify 呼叫 symbolic、SMT、Lean、Coq；
R e o p e n \mathsf{Reopen} Reopen 在新證據出現時合法重新開啟舊 route；
以及：
C l o s u r e A u d i t . \mathsf{ClosureAudit}. ClosureAudit . 因此真正 AI-native mathematics 可能不是：
LLM → proof text . \text{LLM}\to\text{proof text}. LLM → proof text . 而是：
AI ↔ Dynamic Mathematical Research Space . \boxed{
\text{AI}
\leftrightarrow
\text{Dynamic Mathematical Research Space}.
} AI ↔ Dynamic Mathematical Research Space . 19. 與形式驗證的關係
形式驗證系統可以證明：
Γ ⊢ P . \Gamma\vdash P. Γ ⊢ P . MRSM 不取代它。
相反地：
MRSM 管理研究空間， proof assistant 驗證其中局部高權限節點。 \boxed{
\text{MRSM 管理研究空間，}
\quad
\text{proof assistant 驗證其中局部高權限節點。}
} MRSM 管理研究空間， proof assistant 驗證其中局部高權限節點。 因此：
Research Graph → Proof Asset → Formal Obligation → Kernel Proof → Certificate → Research Graph . \text{Research Graph}
\to
\text{Proof Asset}
\to
\text{Formal Obligation}
\to
\text{Kernel Proof}
\to
\text{Certificate}
\to
\text{Research Graph}. Research Graph → Proof Asset → Formal Obligation → Kernel Proof → Certificate → Research Graph . 這形成閉環。
20. 與知識圖譜的差異
一般 knowledge graph 主要回答：
哪些概念相關？
MRSM 需要回答：
這條關係是否具有 theorem authority？
它在哪個 scope 成立？
它是否 discharge 某個 proof debt？
它是否真的 block 一條 route？
它是否允許 parent closure？
因此：
MRSM ≠ Mathematical Knowledge Graph . \boxed{
\text{MRSM}
\neq
\text{Mathematical Knowledge Graph}.
} MRSM = Mathematical Knowledge Graph . 更精確地說：
MRSM = Executable Epistemic Research Graph . \boxed{
\text{MRSM}
=
\text{Executable Epistemic Research Graph}.
} MRSM = Executable Epistemic Research Graph . 21. Mathematical Research Space 的多數學結構
雖然最初 carrier 可以是 graph，但完整研究空間其實自然涉及多個數學領域。
Graph Theory
處理：
dependency；
branching；
cut；
reachability；
obstruction cover。
Topology
處理：
frontier；
closure；
connected component；
boundary；
neighborhood。
Order Theory
處理：
theorem strength；
scope inclusion；
authority hierarchy；
refinement preorder。
Type Theory
防止：
scope collapse；
authority collapse；
representation collapse；
domain confusion。
Dynamical Systems
處理：
reopening；
status evolution；
fixed point；
stabilization；
hysteresis。
Proof Theory
處理：
admissible inference；
certificate；
proof obligation；
formal derivation。
因此：
Mathematical Research Space \boxed{
\text{Mathematical Research Space}
} Mathematical Research Space 本身是一個跨結構數學對象。
22. 一個通用研究流程
MRSM 建議大型數學問題使用以下流程：
Stage 0 — Domain Fixing
固定真正 target。
Stage 1 — Corpus Ingestion
匯入 existing research。
Stage 2 — Candidate Extraction
抽取 claim、route、obstruction、survivor、frontier、nonclaim。
Stage 3 — Typed Graph Construction
建立 typed research graph。
Stage 4 — Candidate Review
防止自然語言 status inflation。
Stage 5 — Proof Authority Audit
檢查 statement、scope、assumptions、dependencies。
Stage 6 — Independent Verification
symbolic / numerical / independent implementation。
Stage 7 — Formalization
轉換為 theorem obligation。
Stage 8 — Kernel Verification
Lean / Coq / SMT。
Stage 9 — Frontier Reconstruction
重新計算剩餘研究 frontier。
Stage 10 — Closure Audit
判斷是否只得到：
local closure , \text{local closure}, local closure , relative closure , \text{relative closure}, relative closure , 或真正足以支持 parent theorem。
23. 研究空間的終極輸出不是只有論文
傳統研究輸出主要是：
Paper . \text{Paper}. Paper . MRSM 的完整研究輸出可以是：
Paper + Graph + Ledger + Certificates + Frontier + Runtime . \boxed{
\text{Paper}
+
\text{Graph}
+
\text{Ledger}
+
\text{Certificates}
+
\text{Frontier}
+
\text{Runtime}.
} Paper + Graph + Ledger + Certificates + Frontier + Runtime . 其中 paper 是：
Π h u m a n ( M ) , \Pi_{\rm human}(\mathfrak M), Π human ( M ) , 即給人類閱讀的一種投影。
而非唯一 canonical source。
24. 方法論的可證偽性
MRSM 本身不應被視為「使用後一定能解決數學問題」。
它可能失敗於：
corpus 不完整；
candidate extraction 錯誤；
graph ontology 不適當；
hidden proof route 未被表示；
scope encoding 錯誤；
formal translation 不忠實；
research space 過度膨脹；
closure policy 過強；
AI route generation 沒有真正的新數學內容。
因此：
Better Research Representation ≠ Guaranteed Mathematical Solution . \boxed{
\text{Better Research Representation}
\neq
\text{Guaranteed Mathematical Solution}.
} Better Research Representation = Guaranteed Mathematical Solution . MRSM 提升的是：
research observability , \text{research observability}, research observability , epistemic precision , \text{epistemic precision}, epistemic precision , search-space management , \text{search-space management}, search-space management , 與：
closure accountability . \text{closure accountability}. closure accountability . 它並不取代真正的新 theorem。
25. 結論
數學長期以來已成功形式化：
number , space , function , proof , program . \text{number},
\text{space},
\text{function},
\text{proof},
\text{program}. number , space , function , proof , program . 但「數學研究過程本身」仍多半存在於：
人類記憶；
論文敘事；
citation；
informal community consensus。
當問題規模、知識密度與研究歷史超過人類單體認知容量時，這種表示開始成為新的瓶頸。
本文提出：
Mathematical Research Space Methodology \boxed{
\textbf{Mathematical Research Space Methodology}
} Mathematical Research Space Methodology 其核心轉換為：
Research Process ⟶ Computable Mathematical Research Space . \boxed{
\textbf{Research Process}
\longrightarrow
\textbf{Computable Mathematical Research Space}.
} Research Process ⟶ Computable Mathematical Research Space . 在此空間中：
proof route , \text{proof route}, proof route , obstruction , \text{obstruction}, obstruction , survivor , \text{survivor}, survivor , frontier , \text{frontier}, frontier , certificate , \text{certificate}, certificate , debt , \text{debt}, debt , reopening , \text{reopening}, reopening , 與：
closure \text{closure} closure 皆具有明確語義。
這並不是單純「使用圖論做數學」。
更準確地說，它試圖建立：
數學研究本身的數學。 \boxed{
\textbf{數學研究本身的數學。}
} 數學研究本身的數學。 當 AI、圖資料庫、形式驗證器、符號計算系統與長期機器記憶開始同時存在時，過去因人類認知容量與資訊載體限制而難以操作的完整 proof space，第一次開始具有實際工程可行性。
未來的數學研究系統因此可能從：
Human → Paper \boxed{
\text{Human}
\to
\text{Paper}
} Human → Paper 轉變為：
Human + AI + Formal Systems ↔ Dynamic Mathematical Research Space . \boxed{
\text{Human}
+
\text{AI}
+
\text{Formal Systems}
\leftrightarrow
\text{Dynamic Mathematical Research Space}.
} Human + AI + Formal Systems ↔ Dynamic Mathematical Research Space . 真正的改變或許不是 AI 終於「會證明數學」。
而是：
人類第一次擁有足以維護整個證明空間的認知載體。 \boxed{
\textbf{人類第一次擁有足以維護整個證明空間的認知載體。}
} 人類第一次擁有足以維護整個證明空間的認知載體。 這使得過去只能被研究者模糊記憶、局部閱讀與口頭傳承的數學研究地形，開始可以成為一個可觀察、可運算、可驗證、可重播、可閉包的正式研究對象。