formal-applied-math/formal-mathfin - 4 Help Wanted Issues

Open Issues Need Help

Formalize key-rate (partial) duration and the sum = effective-duration identity about 4 hours ago

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

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 about 4 hours ago

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

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.

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) about 4 hours ago

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

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.

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) about 4 hours ago

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

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.

Lean

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