cff-version: 1.2.0
message: "If you use this library, please cite it as below."
title: >-
  formal-mathfin: A Formally Verified Library of Mathematical
  Finance in Lean 4
authors:
  - family-names: Coelho
    given-names: Raphael
    orcid: "https://orcid.org/0009-0001-6601-1023"
type: software
license: Apache-2.0
repository-code: "https://github.com/raphaelrrcoelho/formal-mathfin"
url: "https://github.com/raphaelrrcoelho/formal-mathfin"
doi: 10.5281/zenodo.20477782
version: "1.0.0"
date-released: "2026-05-31"
keywords:
  - Lean 4
  - formal verification
  - interactive theorem proving
  - mathematical finance
  - Mathlib
  - stochastic calculus
abstract: >-
  A Lean 4 library of machine-checked mathematical-finance theorems
  (257 delivery-ready theorems across eleven areas), built on Mathlib and
  Rémy Degenne's BrownianMotion package. Every result is classified by
  how faithfully its Lean statement matches the mathematical claim, and
  a build-enforced axiom audit pins the axioms each proof depends on.
preferred-citation:
  type: article
  title: A Formally Verified Library of Mathematical Finance in Lean 4
  authors:
    - family-names: Coelho
      given-names: Raphael
      orcid: "https://orcid.org/0009-0001-6601-1023"
  doi: 10.48550/arXiv.2606.01356
  url: "https://arxiv.org/abs/2606.01356"
  journal: arXiv
  year: 2026