论文页面 - Lean 4 中形式化验证的金融数学库

来源：https://huggingface.co/papers/2606.01356

摘要

我们描述了一个基于 Lean 4 证明助手构建的金融数学库，该库构建于 Mathlib 和布朗运动包之上。该库覆盖面广泛：涵盖从连续时间随机微积分的测度论基础，到衍生品定价，再到应用风险、投资组合和固定收益理论的十一个领域，包含超过两百个无漏洞定理——据我们所知，这是迄今为止最全面的机器验证的金融数学成果。广度只是背景，而非重点。有两件事使其不仅仅是一个目录：它深入到连续理论中，足以将 L2 Itô 积分构造为有界线性等距，并推导出（而非假设）风险中性定价测度；同时，它对自己的忠实性进行了审计：每个结果都根据其 Lean 语句与所声称的数学之间的关系进行分类，并且一个构建强制执行的关卡会锁定每个证明实际使用的公理，因此读者可以精确看到已被证明的内容，以及哪些内容仅是在补充假设下被证明的。最后，我们给出一个坦诚的发现：基于经典金融数学的形式化基础产生的是已知结果的认证统一，而非新的金融理论。因此，贡献在于方法论和基础设施层面：为金融数学提供了可重用的已验证基础，并附带了忠实性审计。

查看 arXiv 页面 (https://arxiv.org/abs/2606.01356)查看 PDF (https://arxiv.org/pdf/2606.01356)GitHub2 (https://github.com/raphaelrrcoelho/formal-mathfin)添加到收藏 (https://huggingface.co/login?next=%2Fpapers%2F2606.01356)

在你的代理中获取这篇论文：

hf papers read 2606.01356

没有最新版本的 CLI？curl -LsSf https://hf.co/cli/install.sh | bash

引用此论文的模型0

没有模型引用此论文

请在模型 README.md 中引用 arxiv.org/abs/2606.01356 以将其链接到此页面。

引用此论文的数据集1

raphaelrrcoelho/formal-mathfin-theorems 查看器• 更新于约4小时前 • 251 • 29 (https://huggingface.co/datasets/raphaelrrcoelho/formal-mathfin-theorems)

引用此论文的 Space0

没有 Space 引用此论文

请在 Space README.md 中引用 arxiv.org/abs/2606.01356 以将其链接到此页面。

包含此论文的收藏集0

没有收藏集包含此论文

将此论文添加到一个收藏集 (https://huggingface.co/new-collection) 以将其链接到此页面。