Una biblioteca formalmente verificada de finanzas matemáticas en Lean 4

Resumen

Describimos una biblioteca de finanzas matemáticas construida en el asistente de demostraciones Lean 4, sobre Mathlib y el paquete BrownianMotion. Es amplia: más de doscientos teoremas libres de "sorry" en once áreas, desde los fundamentos de la teoría de la medida del cálculo estocástico en tiempo continuo hasta la valoración de derivados financieros, pasando por la teoría aplicada de riesgo, carteras y renta fija, y, hasta donde sabemos, el desarrollo más completo verificado por ordenador de finanzas matemáticas hasta la fecha. La amplitud es el contexto, no el objetivo. Dos cosas lo convierten en algo más que un catálogo. Se adentra en la teoría continua lo suficiente como para construir la integral de Itô en L2 como una isometría lineal acotada y para derivar, en lugar de asumir, la medida de valoración neutral al riesgo. Y audita su propia fidelidad: cada resultado se clasifica según cómo su enunciado en Lean se relaciona con las matemáticas que afirma, y una puerta impuesta por la compilación fija los axiomas que cada demostración utiliza realmente, para que el lector pueda ver con precisión qué se ha demostrado y qué solo se ha demostrado bajo hipótesis adicionales. Concluimos con un hallazgo sincero: una base formal sobre las finanzas matemáticas clásicas produce una unificación certificada de resultados conocidos, en lugar de una nueva teoría financiera. La contribución es, por lo tanto, metodológica e infraestructural: fundamentos verificados reutilizables para las finanzas matemáticas, junto con la auditoría de fidelidad.

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.