Lean 4 中一个经过形式化验证的数理金融库

摘要

我们描述了一个构建在Lean 4证明助手之上的数学金融库，该库基于Mathlib和BrownianMotion包。其涵盖范围广泛：包含11个领域、超过200个无"sorry"的定理，从连续时间随机微积分的测度论基础到衍生品定价，再到应用风险、投资组合和固定收益理论——据我们所知，这是迄今为止最全面的机器验证的数学金融发展成果。广度是背景，而非重点所在。有两方面使其超越了单纯的目录汇编：它深入连续理论，足以将L²伊藤积分构造为有界线性等距，并推导（而非假设）风险中性定价测度；同时，它审查自身的忠实性——每个结果都根据其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.