Une bibliothèque de mathématiques financières formellement vérifiée en Lean 4

Résumé

Nous décrivons une bibliothèque de finance mathématique construite dans l’assistant de preuve Lean 4, sur la base de Mathlib et du paquet BrownianMotion. Elle est vaste : plus de deux cents théorèmes sans « sorry » répartis dans onze domaines, des fondements de la théorie de la mesure pour le calcul stochastique en temps continu à l’évaluation des produits dérivés, en passant par la théorie appliquée du risque, du portefeuille et des taux, et constitue, à notre connaissance, le développement vérifié par machine le plus complet de la finance mathématique à ce jour. L’ampleur en est le cadre, non l’objet. Deux aspects font qu’elle dépasse un simple catalogue. Elle s’enfonce assez loin dans la théorie continue pour construire l’intégrale d’Itô L² comme isométrie linéaire bornée et pour dériver, plutôt que supposer, la mesure de pricing neutre au risque. Et elle audite sa propre fidélité : chaque résultat est classé selon la relation entre son énoncé en Lean et les mathématiques qu’il revendique, et une barrière imposée par la compilation fixe les axiomes effectivement utilisés par chaque preuve, de sorte qu’un lecteur puisse voir précisément ce qui a été prouvé et ce qui ne l’a été que sous des hypothèses supplémentaires. Nous concluons par un constat franc : une base formelle de la finance mathématique classique produit une unification certifiée de résultats connus plutôt qu’une nouvelle théorie financière. La contribution est donc méthodologique et infrastructurelle : des fondations vérifiées réutilisables pour la finance mathématique, accompagnées de l’audit de fidélité.

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.