Формально верифицированная библиотека математических финансов на Lean 4

Аннотация

Мы описываем библиотеку математической финансов, построенную в ассистенте доказательств Lean 4 на основе Mathlib и пакета BrownianMotion. Она обширна: более двухсот теорем без пропусков, охватывающих одиннадцать областей — от теоретико-мерных основ стохастического исчисления в непрерывном времени через ценообразование деривативов до прикладной теории риска, портфельной теории и теории фиксированного дохода, — и, насколько нам известно, это самая всеобъемлющая машинно-проверенная разработка в области математической финансов на сегодняшний день. Широта — это контекст, а не суть. Две особенности делают её не просто каталогом. Она проникает в теорию непрерывных процессов достаточно далеко, чтобы построить интеграл Ито в 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.