Among all closed curves with a given perimeter, the circle encloses the most area. This is the isoperimetric inequality: L² ≥ 4πA, with equality only for circles. Known for millennia, proved rigorously in the 19th century, now formalized in Lean 4.
The formalization follows Hurwitz's 1902 proof, which uses Fourier analysis. Parametrize the curve by arc length, expand the coordinates as Fourier series, and apply Wirtinger's inequality to the derivative terms. The isoperimetric inequality falls out as a consequence of the Fourier coefficients satisfying a sum constraint that only the circle saturates.
Each step is elementary in a textbook but demanding in a proof assistant. Parseval's theorem requires formalizing the interchange of infinite sums and integrals. Wirtinger's inequality requires term-by-term differentiation of Fourier series. The shoelace formula for area requires integration by parts for the specific parametrization. The AM-GM inequality closes the gap between the Fourier representation and the geometric statement.
The challenges reveal the distance between “obviously true” and “formally proved.” Different parts of the Lean library (Mathlib) use different indexing conventions for Fourier series; coordinating them required adapter lemmas with no mathematical content but essential formal role. The Weierstrass M-test provides uniform convergence, which licenses the interchanges — without it, every swap of sum and integral is a logical gap.
A 2,300-year-old theorem meeting a 21st-century proof checker. The circle is still optimal; now a computer agrees.