A domain-specific Lean 4 / Mathlib corpus centered on finance and market
mechanisms: 2,074 theorem records + 887 definitions, extracted from a
formalization pipeline and packaged for theorem-proving research (statement,
proof, tactics, premises, kernel-axiom status).
This is a mechanization of largely standard applied mathematics, not new
finance theory. Its value is breadth in under-formalized areas — market
microstructure… See the full description on the dataset page:
https://huggingface.co/datasets/seancollins/lean-quantfinance.
