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