Een formeel geverifieerde bibliotheek voor financiële wiskunde in Lean 4

Samenvatting

Wij beschrijven een bibliotheek voor wiskundige financiën, gebouwd in de Lean 4-bewijsassistent, bovenop Mathlib en het BrownianMotion-pakket. Deze bibliotheek is breed: meer dan tweehonderd sorry-vrije stellingen in elf deelgebieden, van de maattheoretische grondslagen van de continue-tijd stochastische calculus via afgeleide prijsbepaling tot toegepaste risico-, portefeuille- en vastrentende theorie, en naar onze kennis de meest omvattende machine-gecontroleerde ontwikkeling van wiskundige financiën tot nu toe. Breedte vormt de context, niet het doel. Twee zaken maken het meer dan een catalogus. Het reikt ver genoeg in de continue theorie om de L2 Itô-integraal te construeren als een begrensde lineaire isometrie en om de risiconeutrale prijsmaat af te leiden in plaats van aan te nemen. En het controleert zijn eigen getrouwheid: elk resultaat wordt geclassificeerd naar hoe de Lean-formulering zich verhoudt tot de wiskunde die het beweert te zijn; een bouw-afgedwongen poort pint de axioma's vast die elk bewijs werkelijk gebruikt, zodat een lezer precies kan zien wat is bewezen en wat alleen is bewezen onder toegevoegde hypothesen. Wij sluiten af met een eerlijke constatering: een formele basis bovenop klassieke financiële wiskunde levert gecertificeerde unificatie van bekende resultaten op, geen nieuwe financiële theorie. De bijdrage is daarom methodologisch en infrastructureel: herbruikbare geverifieerde grondslagen voor wiskundige financiën, samen met de getrouwheidscontrole.

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.