formal-mathfin-theorems

Formally Verified Mathematical Finance (Lean 4)

This dataset comprises 446 machine-checked theorems in mathematical finance, formalized using Lean 4 atop Mathlib and Rémy Degenne's BrownianMotion package. Each entry includes a theorem's formal statement, its proof, subject area, and a "faithfulness tier" indicating alignment between the mathematical and formal claims.

Sourced from the formal-mathfin library, this collection serves as training and evaluation material for autoformalization and automated theorem proving focused on quantitative finance — a domain underrepresented in existing mathematical benchmarks.

Data Structure

The dataset provides these fields for each theorem:

• id: theorem identifier
• name: human-readable title
• domain: subject classification
• formalization_status: faithfulness category
• description: the theorem as this entry proves it. Where an entry delivers less than the source theorem it is named after, the description says so — it describes the Lean, not the textbook target. The citation for the target is in the source text referenced by id.
• formalization_scope: per-entry disclosure — what was derived, from which primitives, by what method, and what is explicitly out of scope
• lean_code: compilable Lean 4 implementation
• source_file: benchmark origin

Faithfulness Classifications

Results are categorized by how faithfully the formal statement captures the mathematical claim: "full" (415 theorems), "library_wrapper" (18), and "reduced_core" (13). The first two categories comprise the delivery-ready collection (433 of 446).

Dependencies

Compilation requires Lean v4.33.0-rc1, specific Mathlib and BrownianMotion commits, accessible via the reproducible Docker image — see the source repository for pins and instructions.

Attribution

Licensed under Apache-2.0. Users should cite the underlying library (DOI: 10.5281/zenodo.20477781, which resolves to the latest release) and associated paper (arXiv:2606.01356).

(This card and the data file are regenerated by the source repository's CI on every push that changes the benchmark corpus — counts are computed, not hand-maintained.)