Black–Scholes formula solves the Black–Scholes equation

Proved

BlackScholesModel.callPrice_solves_black_scholes_equation

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

black-scholesmathematical-financeoption-pricing

Let $K>0$ be the strike, $T$ the expiry, $r\in\mathbb R$ the risk-free rate and $\sigma>0$ the volatility, and let $C(S,t)=N(d_+)S-N(d_-)Ke^{-r(T-t)}$ be the Black–Scholes call price. Then on the open domain $\{(S,t):S>0,\ t<T\}$ :

$C$ is infinitely differentiable in $(S,t)$ ;
$C$ satisfies the Black–Scholes equation

\frac{\partial C}{\partial t}+\frac12\sigma^2S^2\frac{\partial^2C}{\partial S^2}+rS\frac{\partial C}{\partial S}-rC=0;

for each $t<T$ , $C(S,t)\to0$ as $S\to0^+$ ;
for each $t<T$ , $C(S,t)-\big(S-Ke^{-r(T-t)}\big)\to0$ as $S\to\infty$ ;
for each $S>0$ , $C(S,t)\to\max\{S-K,0\}$ as $t\to T^-$ .

This is the statement that the Black–Scholes formula is the solution of the Black–Scholes equation with the call's terminal and boundary conditions.

Formalization Note The source writes the conditions as $C(0,t)=0$ , $C(S,t)\sim S-Ke^{-r(T-t)}$ as $S\to\infty$ and $C(S,T)=\max\{S-K,0\}$ . Since the formula is undefined at $S=0$ and $t=T$ , these are stated as one-sided limits; the condition at infinity is stated in the (stronger) form that the difference tends to $0$ . The PDE uses deriv, made meaningful by the smoothness clause 1.

Preamble

import Mathlib
import Definitions.Def_BlackScholesModel_Core

open Real MeasureTheory ProbabilityTheory Filter Topology
open scoped ContDiff

Formal statement

namespace BlackScholesModel

theorem callPrice_solves_black_scholes_equation (K r σ T : ℝ) (hK : 0 < K) (hσ : 0 < σ) :
    ContDiffOn ℝ ∞ (fun p : ℝ × ℝ => callPrice K r σ T p.1 p.2)
        {p : ℝ × ℝ | 0 < p.1 ∧ p.2 < T} ∧
    (∀ S t : ℝ, 0 < S → t < T →
      deriv (fun t' => callPrice K r σ T S t') t
        + 1 / 2 * σ ^ 2 * S ^ 2
            * deriv (fun S' => deriv (fun S'' => callPrice K r σ T S'' t) S') S
        + r * S * deriv (fun S' => callPrice K r σ T S' t) S
        - r * callPrice K r σ T S t = 0) ∧
    (∀ t : ℝ, t < T → Tendsto (fun S => callPrice K r σ T S t) (𝓝[>] 0) (𝓝 0)) ∧
    (∀ t : ℝ, t < T →
      Tendsto (fun S => callPrice K r σ T S t - (S - K * Real.exp (-r * (T - t)))) atTop (𝓝 0)) ∧
    (∀ S : ℝ, 0 < S →
      Tendsto (fun t => callPrice K r σ T S t) (𝓝[<] T) (𝓝 (max (S - K) 0))) := by sorry

end BlackScholesModel

Source

Wikipedia, "Black–Scholes model" (snapshot supplied as Black–Scholes_model.pdf, 22 pp.), https://en.wikipedia.org/wiki/Black%E2%80%93Scholes_model; p. 3 (Black–Scholes equation; Black–Scholes formula with terminal and boundary conditions), p. 4 (call formula)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statement (at the explicit instruction of the proposal owner), not by an independent blind auditor. It is not independent testimony; reviewers should compare it against the Lean code themselves.

Let $K,r,\sigma,T$ be real numbers with $K>0$ and $\sigma>0$ ( $r$ and $T$ unrestricted). Let $C(S,t)=N(d_+)S-N(d_-)Ke^{-r(T-t)}$ be the call-price function of the definition file, with $d_\pm=d_\pm(S,K,r,\sigma,T-t)$ , $d_+=\frac{\ln(S/K)+(r+\sigma^2/2)(T-t)}{\sigma\sqrt{T-t}}$ , $d_-=d_+-\sigma\sqrt{T-t}$ , and $N$ the standard normal distribution function defined by its integral. The theorem asserts the conjunction of five statements.

The map $(S,t)\mapsto C(S,t)$ from $\mathbb R^2$ to $\mathbb R$ is $C^\infty$ (continuously differentiable of every finite order) on the open set $U=\{(S,t): S>0,\ t<T\}$ .
For every $S>0$ and every $t<T$ ,

\partial_t C(S,t)+\tfrac12\sigma^2S^2\,\partial_S\big(\partial_S C\big)(S,t)+rS\,\partial_S C(S,t)-r\,C(S,t)=0,

where $\partial_t C(S,t)$ is the derivative at $t$ of $t'\mapsto C(S,t')$ , $\partial_S C(S,t)$ the derivative at $S$ of $S'\mapsto C(S',t)$ , and the second term uses the derivative at $S$ of the function $S'\mapsto(\text{derivative at }S'\text{ of }S''\mapsto C(S'',t))$ . These derivatives are the formal system's "derivative-or-zero" operator: each is the true derivative where one exists and $0$ otherwise.

For every $t<T$ : $C(S,t)\to0$ as $S\to0$ from the right ( $S>0$ ).
For every $t<T$ : $C(S,t)-\big(S-Ke^{-r(T-t)}\big)\to0$ as $S\to+\infty$ .
For every $S>0$ : $C(S,t)\to\max\{S-K,0\}$ as $t\to T$ from the left ( $t<T$ ).

No statement is made at $S\le0$ or $t\ge T$ ; the value $C(0,t)$ itself and $C(S,T)$ are not mentioned.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph