BrownianMotion

Lean 4 库提供已验证的金融数学定理

研究人员使用 Lean 4 证明助手开发了一个全面的金融数学定理库。该库基于 Mathlib 和 BrownianMotion 包，包含二百多个定理，涵盖了从随机微积分到投资组合理论的广泛主题。一个关键特性是其忠实性审计，它精确记录了每个证明所使用的公理，确保了透明度和可验证性。该项目的贡献主要是方法论上的，提供了可重用的、已验证的金融数学基础，而不是新的金融理论。