Eine formal verifizierte Bibliothek der Finanzmathematik in Lean 4

Zusammenfassung

Wir beschreiben eine Bibliothek für mathematische Finanzwirtschaft, die im Beweisassistenten Lean 4 auf Basis von Mathlib und dem BrownianMotion-Paket erstellt wurde. Sie ist breit gefächert: mehr als zweihundert sorgenfreie Theoreme aus elf Bereichen, von den maßtheoretischen Grundlagen der stochastischen Analysis in stetiger Zeit über die Derivatebewertung bis hin zur angewandten Risiko-, Portfolio- und Fixed-Income-Theorie, und unseres Wissens nach die umfassendste maschinengeprüfte Entwicklung der mathematischen Finanzwirtschaft bis heute. Die Breite bildet den Rahmen, nicht den Schwerpunkt. Zwei Dinge machen sie mehr als einen Katalog. Sie reicht weit genug in die stetige Theorie hinein, um das L2-Itô-Integral als beschränkte lineare Isometrie zu konstruieren und das risikoneutrale Bewertungsmaß abzuleiten, anstatt es anzunehmen. Und sie führt ein Treueaudit durch: jedes Ergebnis wird danach klassifiziert, wie seine Lean-Aussage mit der von ihm behaupteten Mathematik zusammenhängt, und eine bau-erzwungene Schranke legt die Axiome fest, die jeder Beweis tatsächlich verwendet, sodass ein Leser genau sehen kann, was bewiesen wurde und was nur unter zusätzlichen Hypothesen bewiesen wurde. Wir schließen mit einem ehrlichen Ergebnis: Eine formale Grundlage über der klassischen Finanzmathematik liefert zertifizierte Vereinheitlichung bekannter Ergebnisse und keine neue Finanztheorie. Der Beitrag ist daher methodologischer und infrastruktureller Art: wiederverwendbare verifizierte Grundlagen für die mathematische Finanzwirtschaft, zusammen mit dem Treueaudit.

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.