Gamma: $\partial^2 V/\partial S^2 = N'(d_+)/(S\sigma\sqrt{T-t})$ for calls and puts

Proved

BlackScholesModel.gamma

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

black-scholesmathematical-financeoption-pricing

Let $K>0$ , $\sigma>0$ , $S>0$ , $t<T$ and $r\in\mathbb R$ . Then the Delta of the call and the Delta of the put are both differentiable in the spot price at $S$ , and

\frac{\partial^2 C}{\partial S^2}(S,t)=\frac{\partial^2 P}{\partial S^2}(S,t)=\frac{N'(d_+)}{S\sigma\sqrt{T-t}}.

As the source remarks, Gamma is the same for calls and puts.

Formalization Note The second derivative is stated as: the function $S'\mapsto\partial_S V(S',t)$ has derivative $N'(d_+)/(S\sigma\sqrt{T-t})$ at $S$ .

Preamble

import Mathlib
import Definitions.Def_BlackScholesModel_Core

open Real MeasureTheory ProbabilityTheory Filter Topology
open scoped ContDiff

Formal statement

namespace BlackScholesModel

theorem gamma (K r σ T S t : ℝ) (hK : 0 < K) (hσ : 0 < σ) (hS : 0 < S) (ht : t < T) :
    HasDerivAt (fun S' => deriv (fun S'' => callPrice K r σ T S'' t) S')
      (stdNormalPDF (dPlus S K r σ (T - t)) / (S * σ * Real.sqrt (T - t))) S ∧
    HasDerivAt (fun S' => deriv (fun S'' => putPrice K r σ T S'' t) S')
      (stdNormalPDF (dPlus S K r σ (T - t)) / (S * σ * Real.sqrt (T - t))) S := 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. 7 (The Options Greeks, table: Gamma)

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.

Here $K,r,\sigma,T,S,t$ are arbitrary real numbers subject to the hypotheses $K>0$ , $\sigma>0$ , $S>0$ and $t<T$ (so $\tau:=T-t>0$ ); $r$ is unrestricted (it may be zero or negative). $N$ , $N'$ , $d_\pm$ , $C$ , $P$ are the functions of the companion definition file (normal distribution function given by its integral, normal density in closed form, $d_\pm=d_\pm(S,K,r,\sigma,T-t)$ , call price $C(S,t)=N(d_+)S-N(d_-)Ke^{-r(T-t)}$ , put price $P(S,t)=N(-d_-)Ke^{-r(T-t)}-N(-d_+)S$ ).

For $V\in\{C,P\}$ let $g_V(S')$ denote the derivative at $S'$ of $S''\mapsto V(S'',t)$ (using the "derivative-or-zero" operator: the true derivative where it exists, $0$ otherwise). The theorem asserts that $g_C$ is differentiable at $S$ with derivative

\frac{N'(d_+)}{S\,\sigma\,\sqrt{T-t}},\qquad N'(x)=\tfrac{1}{\sqrt{2\pi}}e^{-x^2/2},\ d_+=d_+(S,K,r,\sigma,T-t),

and that $g_P$ is differentiable at $S$ with the same derivative.

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

Gamma: ∂2V/∂S2=N′(d+)/(SσT−t)\partial^2 V/\partial S^2 = N'(d_+)/(S\sigma\sqrt{T-t})∂2V/∂S2=N′(d+​)/(SσT−t​) for calls and puts

Gamma: $\partial^2 V/\partial S^2 = N'(d_+)/(S\sigma\sqrt{T-t})$ for calls and puts