Black–Scholes model: normal CDF/PDF, $d_\pm$ , call and put prices

Definition

BlackScholesModel_Core

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

black-scholesmathematical-financeoption-pricing

Core definitions of the Black–Scholes model for a non-dividend-paying stock. Throughout, $K$ is the strike, $T$ the expiry, $r$ the risk-free rate, $\sigma$ the volatility, $S$ the spot price, $t$ the current time and $\tau=T-t$ the time to maturity.

Standard normal distribution and density functions:

N(x)=\frac1{\sqrt{2\pi}}\int_{-\infty}^x e^{-z^2/2}\,dz,\qquad N'(x)=\frac1{\sqrt{2\pi}}e^{-x^2/2}.

The Black–Scholes parameters

d_+=\frac{\ln(S/K)+(r+\sigma^2/2)\tau}{\sigma\sqrt\tau},\qquad d_-=d_+-\sigma\sqrt\tau .

The call and put prices

C(S,t)=N(d_+)S-N(d_-)Ke^{-r(T-t)},\qquad P(S,t)=N(-d_-)Ke^{-r(T-t)}-N(-d_+)S .

The alternative (Black '76) formulation with discount factor $D$ and forward price $F$ :

d_\pm=\frac{\ln(F/K)\pm\sigma^2\tau/2}{\sigma\sqrt\tau},\qquad C(F,\tau)=D\,[N(d_+)F-N(d_-)K],\qquad P(F,\tau)=D\,[N(-d_-)K-N(-d_+)F].

The risk-neutral terminal stock price driven by a standard normal sample $z$ :

S_T(z)=S\exp\Big(\big(r-\tfrac{\sigma^2}2\big)\tau+\sigma\sqrt\tau\,z\Big).

These definitions are shared by every theorem of the mission.

Formalization Note The functions are total: outside the model's domain ( $S\le0$ , $K\le0$ , $\sigma\le0$ or $\tau\le0$ ) the logarithm, square root and division take Lean's default values, so statements about them always carry the hypotheses $K>0$ , $\sigma>0$ , $S>0$ , $t<T$ where needed.

Definition code

import Mathlib

namespace BlackScholesModel

open Real MeasureTheory

/-- The standard normal cumulative distribution function
`N(x) = (1/√(2π)) ∫_{-∞}^x e^{-z²/2} dz`. -/
noncomputable def stdNormalCDF (x : ℝ) : ℝ :=
  (1 / Real.sqrt (2 * Real.pi)) * ∫ z in Set.Iic x, Real.exp (-z ^ 2 / 2)

/-- The standard normal probability density function `N'(x) = (1/√(2π)) e^{-x²/2}`. -/
noncomputable def stdNormalPDF (x : ℝ) : ℝ :=
  (1 / Real.sqrt (2 * Real.pi)) * Real.exp (-x ^ 2 / 2)

/-- `d₊ = (ln(S/K) + (r + σ²/2) τ) / (σ √τ)`, where `τ = T - t` is the time to maturity. -/
noncomputable def dPlus (S K r σ τ : ℝ) : ℝ :=
  (Real.log (S / K) + (r + σ ^ 2 / 2) * τ) / (σ * Real.sqrt τ)

/-- `d₋ = d₊ - σ √τ`. -/
noncomputable def dMinus (S K r σ τ : ℝ) : ℝ :=
  dPlus S K r σ τ - σ * Real.sqrt τ

/-- Black–Scholes price at time `t` of a European call with strike `K`, expiry `T`,
risk-free rate `r` and volatility `σ`, on a non-dividend-paying stock with spot price `S`:
`C(S, t) = N(d₊) S - N(d₋) K e^{-r(T-t)}`. -/
noncomputable def callPrice (K r σ T : ℝ) (S t : ℝ) : ℝ :=
  stdNormalCDF (dPlus S K r σ (T - t)) * S
    - stdNormalCDF (dMinus S K r σ (T - t)) * K * Real.exp (-r * (T - t))

/-- Black–Scholes price at time `t` of the corresponding European put:
`P(S, t) = N(-d₋) K e^{-r(T-t)} - N(-d₊) S`. -/
noncomputable def putPrice (K r σ T : ℝ) (S t : ℝ) : ℝ :=
  stdNormalCDF (-dMinus S K r σ (T - t)) * K * Real.exp (-r * (T - t))
    - stdNormalCDF (-dPlus S K r σ (T - t)) * S

/-- Forward-form `d₊ = (ln(F/K) + σ² τ / 2) / (σ √τ)` (Black '76 parameters). -/
noncomputable def dPlusFwd (F K σ τ : ℝ) : ℝ :=
  (Real.log (F / K) + σ ^ 2 * τ / 2) / (σ * Real.sqrt τ)

/-- Forward-form `d₋ = d₊ - σ √τ`. -/
noncomputable def dMinusFwd (F K σ τ : ℝ) : ℝ :=
  dPlusFwd F K σ τ - σ * Real.sqrt τ

/-- Call value in the alternative (Black '76) formulation:
`C(F, τ) = D [N(d₊) F - N(d₋) K]`, with discount factor `D` and forward price `F`. -/
noncomputable def callPriceFwd (D F K σ τ : ℝ) : ℝ :=
  D * (stdNormalCDF (dPlusFwd F K σ τ) * F - stdNormalCDF (dMinusFwd F K σ τ) * K)

/-- Put value in the alternative (Black '76) formulation:
`P(F, τ) = D [N(-d₋) K - N(-d₊) F]`. -/
noncomputable def putPriceFwd (D F K σ τ : ℝ) : ℝ :=
  D * (stdNormalCDF (-dMinusFwd F K σ τ) * K - stdNormalCDF (-dPlusFwd F K σ τ) * F)

/-- Risk-neutral terminal stock price, as a function of a standard normal sample `z`:
`S_T = S exp((r - σ²/2) τ + σ √τ z)`. -/
noncomputable def terminalPrice (S r σ τ : ℝ) (z : ℝ) : ℝ :=
  S * Real.exp ((r - σ ^ 2 / 2) * τ + σ * Real.sqrt τ * z)

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 (Notation), pp. 3–5 (Black–Scholes formula, Alternative formulation), p. 6 (risk-neutral stock price)

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.

The file defines, inside the namespace BlackScholesModel, the following real-valued functions of real arguments.

Normal distribution function. For real $x$ ,

N(x)=\frac{1}{\sqrt{2\pi}}\int_{(-\infty,x]} e^{-z^2/2}\,dz,

the integral being the Lebesgue (Bochner) integral over the closed half-line $(-\infty,x]$ . (The integrand is integrable, so this is the usual improper integral.)

Normal density. $N'(x)=\frac{1}{\sqrt{2\pi}}e^{-x^2/2}$ ; this is a separate closed-form definition, not defined as a derivative.
$d_+$ . For real $S,K,r,\sigma,\tau$ :

d_+(S,K,r,\sigma,\tau)=\frac{\ln(S/K)+(r+\sigma^2/2)\tau}{\sigma\sqrt{\tau}}.

Conventions of the formal system apply on degenerate inputs: $S/K=0$ when $K=0$ ; $\ln$ is extended by $\ln 0=0$ and $\ln x=\ln|x|$ for $x<0$ ; $\sqrt{\tau}=0$ for $\tau\le0$ ; and division by $0$ returns $0$ , so $d_+=0$ whenever $\sigma\sqrt\tau=0$ .

$d_-$ . $d_-(S,K,r,\sigma,\tau)=d_+(S,K,r,\sigma,\tau)-\sigma\sqrt{\tau}$ .
Call price. With arguments $(K,r,\sigma,T)$ followed by $(S,t)$ and writing $d_\pm$ for $d_\pm(S,K,r,\sigma,T-t)$ :

C(S,t)=N(d_+)\,S-N(d_-)\,K\,e^{-r(T-t)}.

Put price. Same arguments:

P(S,t)=N(-d_-)\,K\,e^{-r(T-t)}-N(-d_+)\,S.

Forward-form $d_\pm$ . For real $F,K,\sigma,\tau$ :

\tilde d_+(F,K,\sigma,\tau)=\frac{\ln(F/K)+\sigma^2\tau/2}{\sigma\sqrt\tau},\qquad \tilde d_-=\tilde d_+-\sigma\sqrt\tau,

with the same degenerate-input conventions.

Forward-form prices. For real $D,F,K,\sigma,\tau$ :

\tilde C(D,F,K,\sigma,\tau)=D\big(N(\tilde d_+)F-N(\tilde d_-)K\big),\qquad \tilde P(D,F,K,\sigma,\tau)=D\big(N(-\tilde d_-)K-N(-\tilde d_+)F\big).

Terminal price. For real $S,r,\sigma,\tau,z$ :

S_T(S,r,\sigma,\tau;z)=S\exp\big((r-\sigma^2/2)\tau+\sigma\sqrt\tau\,z\big).

No hypotheses are attached to any definition; all of them are defined for every real input.

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

Black–Scholes model: normal CDF/PDF, d±d_\pmd±​, call and put prices

Black–Scholes model: normal CDF/PDF, $d_\pm$ , call and put prices