A Formally Verified Library of Mathematical Finance in Lean 4
创建于 更新于
摘要
本文介绍在 Lean 4 框架下、基于 Mathlib 与 BrownianMotion 的形式化金融学库，覆盖连续时间随机微积分、无套利定价、风险中性测度推导、以及广泛的应用层次（期权定价、二项模型、固定收益、投资组合、风险度量等十一大领域），并实现了超过两百条无错假设的定理与严格的信度审计。核心贡献在于（1）构造连续的 Itô 积分并证明其为有界线性同构、（2）从静态 Girsanov 变换出发推导风险中性测度、（3）以可审核的分层分类确保每个定理的数学来源与依赖清晰可追溯，从而实现对经典金融学的“证据化统一”而非提出新金融定理。该库强调方法学与基础设施的可复用性，提供一个可扩展且可验证的金融理论基底。 [page::1]
