Motivation

The Black–Scholes model (Black and Scholes, 1973; Merton, 1973) is the reference model for pricing European options. Its closed-form price, the Black–Scholes formula, is quoted daily by options markets, its partial derivatives (the Greeks) are the standard risk measures that trading desks limit and hedge, and the Black–Scholes equation is the prototype of the parabolic pricing PDEs that are solved numerically when no closed form exists. Merton and Scholes received the 1997 Nobel Memorial Prize in Economic Sciences for this work.

Timeline. Bachelier (1900) first applied Brownian motion to option pricing. In the 1960s Sprenkle, Boness, Samuelson and Merton refined the theory. Black and Scholes found the risk-neutral hedging argument in 1968 and published the formula in The Pricing of Options and Corporate Liabilities (Journal of Political Economy, 1973); Merton's paper of the same year extended the mathematical framework and coined the name.

Setting

Fix a strike $K>0$, an expiry $T$, a constant risk-free rate $r\in\mathbb R$ and a constant volatility $\sigma>0$. At time $t<T$ the time to maturity is $\tau=T-t>0$ and the spot price of the (non-dividend-paying) stock is $S>0$. Let

$$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}$$

be the standard normal distribution and density functions, and set

$$d_+=\frac{1}{\sigma\sqrt{\tau}}\Big[\ln\frac SK+\Big(r+\frac{\sigma^2}2\Big)\tau\Big],\qquad d_-=d_+-\sigma\sqrt\tau .$$

The Black–Scholes call and put prices are

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

In the alternative (Black '76) parametrisation one uses the discount factor $D=e^{-r\tau}$ and the forward price $F=e^{r\tau}S$, with $d_\pm=\frac1{\sigma\sqrt\tau}\big[\ln\frac FK\pm\frac12\sigma^2\tau\big]$, and $C=D[N(d_+)F-N(d_-)K]$. Under the risk-neutral measure the terminal price is $S_T=S\exp\big((r-\tfrac12\sigma^2)\tau+\sigma\sqrt\tau\,Z\big)$ with $Z$ standard normal.

Formalization targets

Goal: the formula solves the Black–Scholes equation

On the domain $\{S>0,\ t<T\}$ the call price $C$ is $C^\infty$ and satisfies

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

together with the boundary and terminal conditions $C(S,t)\to0$ as $S\to0^+$, $C(S,t)-(S-Ke^{-r(T-t)})\to0$ as $S\to\infty$, and $C(S,t)\to\max\{S-K,0\}$ as $t\to T^-$.

Milestones

1. The density $N'$ is the derivative of $N$.
2. The alternative (forward) formulation of the call and put prices.
3. Put–call parity, $P=Ke^{-r\tau}-S+C$, and its forward form $C-P=D(F-K)$.
4. The Greeks table: Delta, Gamma, Vega, Theta and Rho for calls and puts.
5. Risk-neutral pricing: $C=e^{-r\tau}\,\mathbb E[\max(S_T-K,0)]$.
6. Binary options: cash-or-nothing values $e^{-r\tau}N(\pm d_-)$ and asset-or-nothing values $SN(\pm d_+)$.

Significance

The result. The goal is the statement that ties the model's two faces together: the closed-form price is a classical solution of the pricing PDE with the payoff as terminal datum. The Greeks are what hedging strategies are built from (delta hedging is the core of the model's replication argument), put–call parity is the basic no-arbitrage relation, and the risk-neutral and binary-option identities are the probabilistic reading of the two terms in the formula.

Formalizing it. All results here are classical and proved in textbooks (e.g. Hull, Options, Futures, and Other Derivatives). The work is formalization: building a reusable, machine-checked library for the normal distribution function, the Black–Scholes price and its sensitivities, and Gaussian expectations of log-normal payoffs, on top of Mathlib's real analysis and its Gaussian measure gaussianReal.

Difficulty

Each identity is elementary on paper, but the calculus is long: every Greek requires differentiating $N\circ d_\pm$ through a logarithm, a square root and a quotient, and the simplifications rest on the identity $SN'(d_+)=Ke^{-r\tau}N'(d_-)$. The limits in the goal need Gaussian tail estimates (e.g. $SN(-d_+)\to0$ as $S\to\infty$, where $S$ grows while $N(-d_+)$ decays). The risk-neutral identities require computing Gaussian integrals over half-lines with an exponential weight, i.e. a change of variables shifting the mean of the normal distribution.

Formalization scope

All objects are real-valued and deterministic: $N$ is defined by the integral formula above (a Lebesgue integral over $(-\infty,x]$), $N'$ by its closed form, and prices by the formulas, as functions of $(S,t)$ with parameters $(K,r,\sigma,T)$. Partial derivatives are stated with HasDerivAt (genuine differentiability plus the value), except in the goal's PDE, where deriv is used together with an explicit $C^\infty$ clause on the open domain. Each theorem carries the standing assumptions $K>0$, $\sigma>0$, $S>0$, $t<T$ where they are needed; the parity identities hold without them and are stated unconditionally. At $S=0$ and $t=T$ the formula is undefined in the source, so the boundary and terminal conditions are stated as one-sided limits rather than values. Risk-neutral expectations are integrals against the standard Gaussian gaussianReal 0 1 of an explicit log-normal terminal price; no stochastic calculus (Itô integrals, SDEs, Girsanov, Feynman–Kac) is required or formalized. The dividend-paying extensions, American options and the perpetual put are out of scope; binary options are formalized for the non-dividend case $q=0$.

Contributions of reusable lemmas (derivative of $N$, symmetry $N(x)+N(-x)=1$, limits of $N$ at $\pm\infty$, Gaussian half-line integrals) are welcome.

Selected references

• F. Black, M. Scholes, The Pricing of Options and Corporate Liabilities, Journal of Political Economy 81(3), 1973. https://doi.org/10.1086/260062
• R. C. Merton, Theory of Rational Option Pricing, Bell Journal of Economics and Management Science 4(1), 1973. https://doi.org/10.2307/3003143
• J. C. Hull, Options, Futures, and Other Derivatives, Pearson.
• Wikipedia, Black–Scholes model. https://en.wikipedia.org/wiki/Black%E2%80%93Scholes_model