Uma Biblioteca Formalmente Verificada de Finanças Matemáticas em Lean 4

Resumo

Descrevemos uma biblioteca de finanças matemáticas construída no assistente de prova Lean 4, sobre o Mathlib e o pacote BrownianMotion. Ela é ampla: mais de duzentos teoremas livres de 'sorry' em onze áreas, desde os fundamentos da teoria da medida do cálculo estocástico em tempo contínuo até a precificação de derivativos, passando pela teoria aplicada de risco, portfólio e renda fixa, e, até onde sabemos, o desenvolvimento verificado por máquina mais abrangente de finanças matemáticas até o momento. A abrangência é o contexto, não o foco. Dois aspectos a tornam mais do que um catálogo. Ela adentra a teoria contínua o suficiente para construir a integral de Itô L² como uma isometria linear limitada e para derivar, em vez de assumir, a medida de precificação neutra ao risco. E audita sua própria fidelidade: todo resultado é classificado pela forma como sua declaração em Lean se relaciona com a matemática que afirma, e um mecanismo de verificação imposto pela compilação fixa os axiomas que cada prova realmente utiliza, de modo que o leitor possa ver precisamente o que foi provado e o que foi provado apenas sob hipóteses adicionais. Concluímos com uma constatação sincera: uma base formal sobre as finanças matemáticas clássicas produz uma unificação certificada de resultados conhecidos, em vez de uma nova teoria financeira. A contribuição é, portanto, metodológica e infraestrutural: fundamentos verificados reutilizáveis para finanças matemáticas, juntamente com a auditoria de fidelidade.

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.