Lean 4による形式的に検証された数理ファイナンスのライブラリ

要旨

我々は、Lean 4 証明支援系において、Mathlib および BrownianMotion パッケージの上に構築された数理ファイナンスのライブラリを解説する。このライブラリは広範であり、連続時間確率解析の測度論的基礎からデリバティブ価格評価、さらには応用リスク理論、ポートフォリオ理論、債券理論に至る11の分野にわたる200以上の未完成箇所（sorry）のない定理を含み、我々の知る限り、これまでで最も包括的な数理ファイナンスの機械検証による開発である。広範さは前提であり、要点ではない。このライブラリが単なるカタログ以上のものとなっている点は二つある。まず、連続理論に十分深く踏み込み、L2伊藤積分を有界線形等長写像として構成し、リスク中立価格評価測度を仮定するのではなく導出している。第二に、自己の忠実性を監査している。すなわち、各結果は、Lean の文が主張する数学とどのように関連しているかによって分類され、ビルドによって強制されるゲートが各証明が実際に使用する公理を固定するため、読者は何が証明されたのか、何が追加の仮定の下でのみ証明されたのかを正確に確認できる。最後に、率直な知見を述べる。古典的な数理ファイナンスの上に形式化された基盤は、新たな金融理論ではなく、既知の結果の証明済みの統合をもたらす。したがって、本貢献は方法論的および基盤的なものであり、再利用可能な検証済みの数理ファイナンスの基礎と、忠実性監査を提供するものである。

English

We describe a library of mathematical finance built in the Lean 4 proof assistant, on top of Mathlib and the BrownianMotion package. It is broad: more than two hundred sorry-free theorems across eleven areas, from the measure-theoretic foundations of continuous-time stochastic calculus through derivative pricing to applied risk, portfolio, and fixed-income theory, and, to our knowledge, the most comprehensive machine-checked development of mathematical finance to date. Breadth is the setting, not the point. Two things make it more than a catalogue. It reaches into the continuous theory far enough to construct the L2 Itô integral as a bounded linear isometry and to derive, rather than assume, the risk-neutral pricing measure. And it audits its own faithfulness: every result is classified by how its Lean statement relates to the mathematics it claims, and a build-enforced gate pins the axioms each proof actually uses, so a reader can see precisely what has been proved and what has only been proved under added hypotheses. We close with a candid finding: a formal base over classical financial mathematics yields certified unification of known results rather than new financial theory. The contribution is therefore methodological and infrastructural, reusable verified foundations for mathematical finance, together with the faithfulness audit.