在 Lean 4 中形式化驗證的數學金融庫

摘要

我們描述了一個基於 Lean 4 證明助手、建構在 Mathlib 與 BrownianMotion 套件之上的數學金融函式庫。其涵蓋範圍廣泛，包含跨越十一個領域、超過兩百個無「抱歉」定理，從連續時間隨機微積分的測度論基礎，到衍生品定價、應用風險、投資組合及固定收益理論；據我們所知，這是迄今為止最全面的機器驗證數學金融發展成果。廣度是設定背景，而非重點。有兩項特點使其超越單純的目錄：它足夠深入連續理論，能夠將 L2 Itô 積分建構為有界線性等距，並推導出風險中性定價測度，而非僅是假設；同時，它對自身的忠實性進行審計：每個結果都根據其 Lean 陳述與其所聲稱的數學之間的關係進行分類，並透過建構強制閘門來限定每個證明實際使用的公理，讓讀者能準確看出哪些是已證明的結果，哪些只是在附加假設下才獲證明。最後，我們坦率地發現：在經典金融數學基礎上進行形式化驗證，所得出的是已知結果的認證統一，而非新的金融理論。因此，其貢獻在於方法論與基礎設施層面——為數學金融提供可重複使用的驗證基礎，並附帶忠實性審計。

English

We describe a library of mathematical finance built in the Lean 4 proof assistant, on top of Mathlib and the BrownianMotion package. It is broad: more than two hundred sorry-free theorems across eleven areas, from the measure-theoretic foundations of continuous-time stochastic calculus through derivative pricing to applied risk, portfolio, and fixed-income theory, and, to our knowledge, the most comprehensive machine-checked development of mathematical finance to date. Breadth is the setting, not the point. Two things make it more than a catalogue. It reaches into the continuous theory far enough to construct the L2 Itô integral as a bounded linear isometry and to derive, rather than assume, the risk-neutral pricing measure. And it audits its own faithfulness: every result is classified by how its Lean statement relates to the mathematics it claims, and a build-enforced gate pins the axioms each proof actually uses, so a reader can see precisely what has been proved and what has only been proved under added hypotheses. We close with a candid finding: a formal base over classical financial mathematics yields certified unification of known results rather than new financial theory. The contribution is therefore methodological and infrastructural, reusable verified foundations for mathematical finance, together with the faithfulness audit.