资产定价基本定理：在Lean 4中的形式化证明

资产定价基本定理指出，一个市场无套利当且仅当它承认一个等价鞅测度。我们在Lean 4中基于Mathlib在三种设定下对其进行了形式化：有限状态市场（Harrison-Pliska）、任意概率空间上具有单一标量收益的单期市场（Follmer-Schied），以及具有有限数量资产的单期市场。有限情形是分离超平面的几何；标量单期情形是测度变换的初等应用。在$d$资产情形中，等价鞅测度被显式构造，作为光滑凸势$\mathbb{E}[\log(1+e^{\langle\theta,Y\rangle})]$的最小化器：无套利恰为该势的强制性，其一阶条件即鞅性质，最小化器的逻辑权重即为测度的密度。该构造不使用Hahn-Banach定理、$L^0$-闭性论证、可测选择或非冗余假设。据我们所知，这是在任何证明助手中首次机器校验的资产定价基本定理。其边界是明确的：一般的多期Dalang-Morton-Willinger定理不在该开发范围内。每个定理均无公理漏洞，每个主要结果的公理通过构建强制门固定到Mathlib的经典默认值，并且整个工作可从固定工具链重现。