独立研究者用"数学验证工具"给金融公式盖章认证，这件事到底有多难？

这项由独立研究者完成的工作以预印本形式发表于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：短期内对普通投资者没有直接影响，金融市场的运作方式不会因此改变。但从更长远的视角看，这类工作建立了一套可检查的数学基础，未来当金融机构或监管机构需要核实某个定价模型或风险管理方法的数学是否正确时，可以借助这套工具做机器级别的验证，而不只是依赖人工审阅。这类似于给整个行业的数学基础做了一次权威的质量认证。