formal-applied-math

formal-applied-math/formal-mathfin

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

16 good first / help-wanted issues · Lean · last activity Aug 20, 2026

29 stars 9 forks 29 watchers Lean Apache License 2.0

black-scholes derivatives-pricing formal-methods formal-verification ito-calculus lean4 mathematical-finance mathlib option-pricing quantitative-finance stochastic-calculus theorem-proving

16 Open Issues Need Help Last updated: Aug 20, 2026

Open Issues Need Help

View All on GitHub

Formalize the Hull–White (extended-Vasicek) bond price P(0,T) = A(T)·exp(−B(T)·r₀) 1 day ago

help wanted area:fixed-income type:proof difficulty:medium status:ready

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Binomial barrier option prices from the reflection principle 1 day ago

good first issue area:binomial type:proof difficulty:small status:ready

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Relate numeraireDensity to Measure.rnDeriv 1 day ago

good first issue area:foundations type:proof difficulty:small status:ready

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Formalize key-rate (partial) duration and the sum = effective-duration identity 1 day ago

help wanted area:fixed-income type:proof difficulty:medium status:in-progress

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Covered & uncovered interest-rate parity F = S·e^((r_d−r_f)T) 1 day ago

help wanted good first issue type:proof difficulty:small status:ready area:fx

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Add the Uniswap v3 concentrated-liquidity position value 1 day ago

help wanted area:defi type:research difficulty:hard status:blocked-design

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Add the constant-product impermanent-loss formula IL(r) = 2√r/(1+r) − 1 1 day ago

help wanted area:defi type:proof difficulty:medium status:in-progress

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Add the Schwartz one-factor commodity futures closed form (OU log-spot) 1 day ago

help wanted area:futures type:proof difficulty:hard status:ready

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Verify the CIR affine loading B(T) solves the Riccati ODE B′ = 1 − κB − ½σ²B² 8 days ago

help wanted area:fixed-income type:proof difficulty:medium status:review

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Variable-coefficient Feynman–Kac: local-vol / Heston PDE on the SDE layer 20 days ago

help wanted area:foundations type:proof difficulty:hard status:blocked-design

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Add the constant-mean (Balancer) AMM invariant ∏ Bᵢ^{wᵢ} and spot price 30 days ago

help wanted area:defi type:proof difficulty:medium status:in-progress

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Add life insurance EPV A_x and the fundamental identity A_x = 1 − d·ä_x about 1 month ago

help wanted area:actuarial type:proof difficulty:medium status:in-progress

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Glosten–Milgrom adverse-selection bid–ask spread from Bayesian quotes about 2 months ago

help wanted type:proof difficulty:medium status:review area:execution

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Derive the APT exact-factor pricing relation E[Rᵢ]−r = Σₖ βᵢₖ λₖ from no-arbitrage 2 months ago

help wanted area:portfolio type:proof difficulty:medium status:in-progress

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Add the life-contingent annuity EPV ä_x:n = ∑ vᵏ·ₖpₓ (survival-weighted) 2 months ago

help wanted area:actuarial type:proof difficulty:medium status:in-progress

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Add the American-put early-exercise premium: European put < American put (strict) 2 months ago

help wanted area:binomial type:proof difficulty:medium status:in-progress

formal-applied-math/formal-mathfin

29

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving