這項由獨立研究者完成的工作以預印本形式發表於2026年5月，論文編號為arXiv:2606.01356，收錄於量化金融（q-fin.MF）方向，感興趣的讀者可通過該編號查詢完整論文。
**研究概要：當金融公式遇上"數學法庭"**
每天，全球金融市場上數以萬億計的交易背後，都有一套數學公式在默默運算。期權的價格怎麼定？投資組合的風險怎麼算？這些公式被寫在教科書里，被金融從業者奉為圭臬，但有一個問題幾乎從沒有人認真追問過：這些公式，真的被嚴格證明過嗎？
嚴格到什麼程度？嚴格到用電腦程序一步一步檢查每一個邏輯推導，確保沒有任何"跳步"、沒有任何"大家都知道所以省略"的地方。這種檢查方式叫做"形式化證明"，而承擔這項工作的電腦程序叫做"證明助手"——把它理解成一位極度挑剔的數學考官，你寫下的每一步推導它都要審查，一旦發現漏洞立刻拒絕通過。
這項研究做的，就是把兩百多條數學金融領域的核心結論，逐一送上這位考官的審查台，並且全部通過了。這是迄今為止規模最大、覆蓋最廣的數學金融形式化驗證工作。
---
**一、為什麼數學金融需要一位"極度挑剔的考官"**
金融數學的公式往往看起來優雅簡潔，但它們背後的推導過程卻如同一座精心搭建的積木塔——每一塊積木都依賴下面那塊，一旦某處有鬆動，整座塔都可能垮掉。問題在於，很多金融教科書在推導公式時，常常會用一句"顯然可以證明"或者"根據標準理論"略過那些最難的部分，就好像在搭積木時偷偷用了膠水，表面上看積木塔穩穩的，但膠水究竟有沒有粘牢，沒人認真檢查過。
證明助手的作用，就是強迫你把膠水的成分也寫清楚。這項研究選用的證明助手叫做Lean 4，它是目前數學界最流行的形式化工具之一，已經被用來驗證了大量純數學定理。在此之前，Lean 4上已經積累了一個叫Mathlib的龐大數學庫，裡面包含了測度論、概率論、條件期望、鞅論等大量數學基礎設施，還有一個專門處理布朗運動的BrownianMotion工具包。這項研究就是在這兩個基礎之上，搭建了一整套數學金融的形式化體系。
在此之前，形式化金融數學的工作非常零散。有人用另一個證明助手Isabelle/HOL驗證了離散版本的期權定價模型（Cox-Ross-Rubinstein模型），但只局限在那一個特定模型里。還有人驗證了去中心化交易所的數學原理。最近有研究者在Lean 4里走通了"從伊藤引理到Black-Scholes公式"這一條推導路徑，但按照作者自己的說法，連續時間版本的伊藤積分只是在結構上被確認，並沒有真正被構造出來。這些工作各自都很有價值，但都是點狀的，沒有人嘗試把整個數學金融的地圖畫出來。
這項研究就是那張地圖。
---
**二、這張地圖畫了什麼：十一個領域，兩百五十一條定理**
要理解這項工作的規模，可以把它想成一次對整個數學金融領域的"全面體檢"。體檢的範圍覆蓋了十一個大方向，涉及從最基礎的數學工具一直到實際應用中的各種金融產品和風險管理方法。
體檢的起點是連續時間隨機微積分的基礎層。這裡處理的是布朗運動——一種描述股票價格隨機漂移的數學對象，就像花粉在水面上的隨機遊走。圍繞布朗運動，研究驗證了維納積分和伊藤積分的L?等距性質、二次變差、連續伊藤積分本身，以及針對x?函數的L?伊藤公式（包括二維情況），還有連接隨機過程與偏微分方程的費曼-卡茨定理。
建立在這個基礎上的是無套利定價的理論框架，包括資產定價基本定理（簡單理解：如果市場上沒有"空手套白狼"的機會，那麼一定存在一種特殊的定價方式）、狀態價格、定價核、凸性定價泛函，以及靜態Girsanov變換。
再往上，是金融實踐中最常見的定價公式層：Black-Scholes模型（看漲期權和看跌期權的定價公式及其希臘字母風險指標、數字期權、冪式期權、交換期權、巴歇利爾期權、定價偏微分方程、Breeden-Litzenberger公式）；二叉樹模型（CRR定價與複製策略、二叉樹向Black-Scholes的收斂極限、美式期權通過Snell包絡的處理、反射原理）；期貨定價（Black-76模型、利率掉期期權）；固定收益（Vasicek利率模型、久期與凸性、免疫策略、簡化形式信用模型與結構性信用模型）；投資組合理論（Markowitz均值-方差優化、資本資產定價模型CAPM、Black-Litterman模型、風險平價）；績效測量；風險測量（一致性風險測量、譜風險測量、條件風險價值CVaR）；精算數學；以及去中心化金融（DeFi）。
兩百五十一條定理，全部無sorry通過——"sorry"在Lean里是一個特殊標記，意思是"這步先跳過，以後再證"，就像考試答卷時寫"此題留白，答案顯然成立"。這項研究里沒有任何一處用了這個標記。
---
**三、四個等級的"誠信檔案"：這項研究最聰明的地方**
形式化證明圈子裡有一個公開的秘密：很多聲稱"我們證明了X"的論文，其實證明的是一個加了額外假設的X，或者是一個比X弱得多的版本。但論文摘要里通常不會清楚說明這一點，讀者很難分辨。
這項研究引入了一套專門的分級系統來解決這個問題，可以把它理解成給每一條定理建立一份"誠信檔案"，檔案里記錄著這條定理到底被證明到了什麼程度。
檔案分四個等級。第一個等級叫"full"，意思是Lean里的陳述與數學原文完全一致，沒有任何打折扣的地方，這是最高級別。第二個等級叫"library_wrapper"，意思是這個結論在上游數學庫（Mathlib或BrownianMotion）里已經有了，這裡只是薄薄地包裝了一下引用進來，本質上也是完整的。第三個等級叫"reduced_core"，意思是結論本身是對的，但證明時加入了額外的假設，或者某個子步驟是直接聲明的而沒有推導，這是打了折扣的版本，但折扣被明確標註出來了。第四個等級叫"placeholder"，代表占位符，還沒有實質內容。
在這兩百五十一條定理里，屬於"full"的有204條，屬於"library_wrapper"的有19條，屬於"reduced_core"的有28條，"placeholder"為零。也就是說，有223條定理（占89%）是完整的、無折扣的證明。
更重要的是，這套分級不只是文檔上的標註。研究者設計了一個叫做AxiomAudit.lean的文件，它會強制檢查每一條被標註為完整的定理，到底依賴了哪些公理。Lean本身有三個標準公理，所有數學都最終追溯到這三個基礎假設，這是完全可接受的。但如果某條定理悄悄用了"sorry"（相當於偷偷貼了一塊補丁），AxiomAudit.lean就會讓整個項目編譯失敗，像報警器一樣響起來。這意味著，任何試圖"渾水摸魚"的證明，都會被自動抓出來。
---
**四、兩個真正難的地方：連續伊藤積分與風險中性測度**
這項研究的深度，集中體現在兩個技術核心上。
**連續L?伊藤積分的真正構造**
伊藤積分是隨機微積分的心臟。普通的積分，是把一條曲線切成無數小段加總起來。但如果被積函數本身也是隨機的（比如股票價格），這種"切段加總"就需要極為小心地處理，因為隨機函數的波動方式和普通函數很不一樣。
最早的版本叫維納積分，處理的是確定性（非隨機）被積函數，這相對容易，可以證明它是一個L?等距映射——意思是積分前後"能量"（方差意義下的大小）保持不變，就像一個不失真的音頻放大器。
真正難的是處理隨機的、適應的被積函數。"適應"這個詞的意思是，被積函數在每個時刻只能依賴到那個時刻為止的資訊，不能"預知未來"。這正是金融里股票價格滿足的條件。這項研究從簡單的離散逐步適應過程出發，證明了伊藤等距性——數學上的關鍵在於，當你把積分拆成一小塊一小塊時，不同時刻的乘積項的期望值會消失，這依賴於布朗運動增量的弱馬爾可夫性質（簡單說：布朗運動的每一步增量與過去無關）。這一點是伊藤積分和維納積分真正不同的地方。
從這個等距性出發，通過一個叫"π-λ稠密性論證"和範數保持延拓的技術步驟，最終把連續伊藤積分構造為定義在L?([0,T])上的有界線性映射。這個對象在形式化證明里叫做itoIntegralCLM_T，它的"鎮庫之寶"是一個具體的計算結果：∫?? B dB = 1/2 (B?_T - B?_0 - T)。這個等式左邊是布朗運動對自身的積分，右邊多出來的那個"-T"正是伊藤積分與普通微積分最著名的區別之處（在普通微積分里，x對自身積分只會得到 1/2 x?，不會有額外的修正項）。這個修正項，就是金融數學裡無數結果的根源。
**風險中性測度的推導而非假設**
Black-Scholes公式的推導，通常從一個假設出發：存在一個"特殊的概率測度Q"，在這個測度下，折現後的資產價格是鞅（簡單理解：未來的期望值等於現在的值，沒有系統性偏差）。有了這個Q，期權的價格就等於在Q下對期權到期收益的期望值，再折現回來。
但這個Q是哪裡來的？大多數教科書和之前的形式化工作都直接把它作為假設給定，就好像說"假設有一位神奇的廚師會做這道菜"，然後從這個假設出發推導菜譜，卻從不解釋這位廚師是怎麼學會這道菜的。
這項研究在GaussianGirsanov.lean里，通過一個叫做"靜態Girsanov變換"（也稱Esscher變換）的方法，從物理世界的概率測度出發，真正推導出了這個Q。具體說：從資產價格在真實世界（物理測度）下的高斯分布出發，通過一個精心設計的密度函數（Esscher密度）來"重新分配"概率，使得變換後的測度Q下，資產的終值恰好滿足Black-Scholes公式所需要的對數正態分布，同時折現後的資產價格在Q下確實是鞅。
這樣做的好處是巨大的。原來Black-Scholes的假設前提BSCallHyp（"終值在Q下是對數正態的"），現在變成了一個可以從更基礎的假設推導出來的定理，寫作BSCallHyp.exists_of_physical。不僅如此，Margrabe的交換期權公式也可以用同樣的"換計價單位"思路（換numéraire，就是換一下"用什麼來作為價值的參照物"）自然推出來，不需要再單獨推導一遍。
---
**五、讓整個體系不散架的四根支柱**
兩百五十一條定理、十一個領域，要讓它們構成一個有機的整體而不是一堆散沙，需要一套聰明的架構設計。這項研究用了四根支柱來支撐整個體系。
第一根支柱是線性無套利定價泛函。所有的定價，都被抽象為一個對收益的非負線性函數。線性性意味著兩份資產加在一起的價格，等於兩份資產分別的價格之和。非負性意味著永遠不可能為負收益付出正價格。僅憑這兩個性質，買賣平價（put-call parity）、遠期價格、期權價格對執行價格的凸性，就全都可以作為推論直接得出，而不需要在每種金融產品上單獨重新推導。
第二根支柱是Garman標準形式。Black-Scholes家族裡的所有期權定價公式，都可以統一寫成A·Φ(d?) - K·DF·Φ(d?)這個形狀，其中Φ是標準正態分布的累積分布函數，A、K、DF和有效波動率隨具體期權類型的不同而取不同值。看漲期權、看跌期權、數字期權、冪式期權、交換期權、含股息版本、外匯期權，全都是這個模板的特例。Margrabe的交換期權公式也是其中一個實例，而不是需要單獨證明的獨立結論。
第三根支柱是布朗運動基礎橋接。定價假設被寫成一個很簡潔的邊緣條件——只要求資產在Q下的終值服從對數正態分布，不對整條路徑做要求。但另外有兩個專門的橋接模組（BSCallHypFromBrownian.lean和PricingFromBrownian.lean）證明，這個邊緣條件可以從BrownianMotion工具包里的預布朗運動對象推導出來。這樣，定價層面的公式就通過橋接與連續時間的隨機過程基礎設施連接在一起。
第四根支柱就是前面講的誠信檔案系統，確保整個體系的每一條聲明都有明確的邏輯地位。
這四根支柱共同工作的結果是一個"信任核心很小"的體系：接受線性定價泛函、Garman標準形式和布朗運動橋接這三個原則，絕大多數的定價結論都自動成為推論，不需要再引入新的假設。
---
**六、形式化驗證帶來的意外收穫：兩件事竟然是同一件事**
當你把一大堆獨立建造的數學模組都用同一套形式化語言寫出來之後，有時候會發現一個令人驚喜的現象：兩個看起來毫不相干的概念，竟然在數學上完全等同。
這項研究在Bridges/目錄下專門收錄了這類"跨領域橋接"結果，而它們恰恰是形式化方法給數學金融帶來的獨特禮物。
一個例子是投資組合集中度與多樣化方差的統一。Markowitz投資組合理論里有一個公式，計算N個資產組成的投資組合在對角協方差矩陣（簡單理解：各資產之間沒有相關性）下的總方差。經濟學裡還有一個叫"赫芬達爾指數"的東西，原本是用來衡量市場集中度的——如果一個市場裡有很多小企業，赫芬達爾指數很低；如果一個企業壟斷整個市場，指數為1。這項研究的形式化驗證揭示，這兩個東西在數學上是完全等同的（差一個共同方差的係數），寫作定理portfolioVarN_diag_eq_herfindahl。換句話說，投資組合的集中度，在數學上就是可分散化的方差——越分散的投資組合，其赫芬達爾指數越低，可分散的風險也越低。這不是一個新的金融洞見，但它是一個被機器檢查過的、嚴格的數學等同關係。
另一個例子是精算生存函數與信用風險中違約概率的統一。精算學裡用一個函數來描述一個人在給定時刻仍然存活的概率，這個函數從死亡力（hazard rate）積分得到。信用風險里的簡化形式模型，用類似的方式描述一家公司到某個時刻尚未違約的概率。這項研究的形式化驗證發現，這兩個函數在定義上完全一致，Lean的rfl（reflexivity，自反性——最簡單的證明，意思是兩邊本來就是同一個東西）就能直接證明，寫作定理survivalFromForce_eq_hazardSurvival。一個人"活下去"的數學，和一家公司"活下去"的數學，是同一個數學。
這類發現是形式化驗證特有的副產品：當你被迫把所有概念都寫成精確的符號語言時，原來被不同名詞掩蓋的相同數學結構就會自然浮現出來。
---
**七、這項工作的邊界：哪些地方還沒做到**
研究者在論文裡非常坦率地畫出了工作的邊界，這本身也是誠信檔案精神的體現。
那28條被標註為"reduced_core"的定理，主要集中在連續時間和離散過程的基準測試里，而不在定價層面。這意味著，連續時間隨機過程的某些最困難的部分，目前還是在額外假設下或者通過聲明（而非推導）某些子步驟來處理的。定價層面的公式則幾乎全部是完整的證明。
更具體地說，連續伊藤積分雖然被構造了出來，但目前金融定價模組連接到連續時間對象的方式，是通過"邊緣條件橋接"（只要求終值的分布性質滿足條件），而不是真正從itoIntegralCLM_T這個積分對象出發逐步積分推導Black-Scholes公式。這個完整的路徑——密度論證、延拓步驟、適應等距性的細節——將在一篇配套論文裡詳細給出。
同樣地，靜態Girsanov推導的完整細節（Esscher傾斜、換測度的簿記工作、鞅性質的證明）也將在另一篇配套論文裡展開。
二叉樹向Black-Scholes的收斂極限雖然被端到端地驗證了，但用的是繞道put-call平價的特徵函數/Lévy連續性論證，這樣做是為了繞開均勻可積性的技術障礙。一個非漸近的、帶顯式常數的精細化版本——研究者認為這是整個項目里唯一真正新的數學結果——將作為一篇針對計算金融方向的獨立論文發表。
還有一些技術基礎設施（隨機時間區間的API）已經作為PR提交給BrownianMotion上游項目，撰寫論文時還在審查中（PR #446）。高斯尾部和完全平方積分引理這些Mathlib原本缺少的工具，也在這個庫里被開發出來，適合合併到Mathlib主庫。
---
**八、這項工作的真正意義：驗證的是體系，而非發現了新事物**
論文的結論部分有一段極為坦誠的話，值得在這裡完整地傳達給讀者。
研究者明確指出：這項工作里沒有任何一條數學定理是新的。數學金融的所有這些結論，早在幾十年前就已經被證明，被寫進了無數教科書和論文。形式化證明並沒有發現新的金融規律，也沒有推翻任何已知結論。
那它做了什麼？它做了兩件有價值的事。
第一，它把連續時間隨機微積分的基礎設施真正構造了出來，而不只是在結構上確認它存在。之前的形式化工作（包括被這項研究直接引用和改進的那些）或者局限在離散模型，或者在到達連續伊藤積分時選擇"假設它存在"而不是"構造它"。現在，這個基礎對象是真實存在於Lean代碼里的，任何未來想要在此之上構建連續時間金融數學的工作，都可以直接使用。
第二，它建立了一套"誠信檔案"機制，讓形式化證明的忠實程度變得可檢查、可機器驗證。這個機制是完全可以被其他項目移植採用的——不管那個項目研究的是什麼數學領域。
因此，這項工作的貢獻是方法論上的和基礎設施上的。它是數學金融的一個經過認證的統一性驗證，而不是新的金融理論。研究者把這個判斷明確寫在論文裡，而不是把它當作局限性來道歉——這種態度本身，就是這套誠信檔案精神的最好示範。
說到底，數學金融需要的這類工作，就像給一座老建築做一次徹底的結構安全鑑定。建築本身已經在那裡站了幾十年，大家也都覺得它很穩固。做鑑定的人並沒有重新設計這座建築，也沒有添加新的樓層，他們做的是拿著專業設備把每一根梁、每一塊磚都檢查一遍，然後出具一份寫明每處檢查結果的報告。這份報告不會讓建築變得更高，但它讓所有人都能知道這座建築究竟穩到什麼程度、哪裡還存在隱患。而且，它留下了一套可以被後來者沿用的檢查方法——這才是最持久的價值所在。
---
Q&A
Q1：形式化證明和普通數學證明有什麼區別？
A：普通數學證明是人寫給人看的，允許跳過"顯然"的步驟，讀者靠數學直覺補全漏洞。形式化證明則要用電腦程序（證明助手）逐步檢查每一個推導，任何跳步都會被拒絕。這就像普通簽名和經過公證的簽名的區別——兩者都能證明你簽了字，但公證版本有第三方強制核查，不可能造假。
Q2：Black-Scholes公式到底是什麼，為什麼需要被"重新驗證"？
A：Black-Scholes公式是計算期權（一種給你權利但不強制你買賣資產的合同）價格的數學公式，1973年提出後成為金融行業的基石。它沒有被"推翻"，而是被更嚴格地重新檢查了一遍。以前的證明依賴很多"顯然的"跳步，這次驗證是第一次用電腦把整個推導鏈條完整走通，並且連風險中性測度（公式里必須假設存在的特殊概率）也從更基礎的原理推導了出來，而不再只是假設它存在。
Q3：數學金融形式化驗證對普通投資者有什麼影響？
A：短期內對普通投資者沒有直接影響，金融市場的運作方式不會因此改變。但從更長遠的視角看，這類工作建立了一套可檢查的數學基礎，未來當金融機構或監管機構需要核實某個定價模型或風險管理方法的數學是否正確時，可以藉助這套工具做機器級別的驗證，而不只是依賴人工審閱。這類似於給整個行業的數學基礎做了一次權威的質量認證。
