Prove2Me

N′=dN/dxN' = dN/dx: the normal density is the derivative of the normal distribution function

Proved
BlackScholesModel.stdNormalCDF_hasDerivAt

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

black-scholesmathematical-financeoption-pricing

Let N(x)=12π∫−∞xe−z2/2 dzN(x)=\frac1{\sqrt{2\pi}}\int_{-\infty}^x e^{-z^2/2}\,dz be the standard normal distribution function and N′(x)=12πe−x2/2N'(x)=\frac1{\sqrt{2\pi}}e^{-x^2/2} the standard normal density. Then for every real xx, NN is differentiable at xx and

dNdx(x)=12πe−x2/2.\frac{dN}{dx}(x)=\frac1{\sqrt{2\pi}}e^{-x^2/2}.

This justifies the notation N′N' used throughout the Black–Scholes formulas, in particular in the Greeks.

Preamble
import Mathlib
import Definitions.Def_BlackScholesModel_Core

open Real MeasureTheory ProbabilityTheory Filter Topology
open scoped ContDiff
Formal statement
namespace BlackScholesModel

theorem stdNormalCDF_hasDerivAt (x : ℝ) :
    HasDerivAt stdNormalCDF (stdNormalPDF x) x := 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 (Notation: N(x) and N'(x) = dN(x)/dx)
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.

For every real number xx: the function N(y)=12π∫(−∞,y]e−z2/2 dzN(y)=\frac{1}{\sqrt{2\pi}}\int_{(-\infty,y]}e^{-z^2/2}\,dz (defined in the definition file) is differentiable at xx, and its derivative there equals 12πe−x2/2\frac{1}{\sqrt{2\pi}}e^{-x^2/2}, the closed-form expression that the definition file calls the normal density N′(x)N'(x). There are no hypotheses.

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