Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case
Miraj Samarakkody
math.MG
Mar 15, 2026 · v1
TL;DR
Formally verifies the planar isoperimetric inequality via Hurwitz's Fourier-analytic approach in Lean 4 and Mathlib.
Abstract
We present a formal verification of the classical isoperimetric inequality in the plane using the Lean 4 proof assistant and its mathematical library Mathlib. We follow Adolf Hurwitz's analytic approach to establish the inequality $L^2 \ge 4πA$, which states that among all simple closed curves of a given perimeter $L$, the circle uniquely maximizes the enclosed area $A$. The formalization proceeds in two phases. In the first phase, we establish the Fourier-analytic foundations required by Hurwitz's approach: we formalize orthogonality relations for trigonometric functions over $[-π,π]$, Parseval's theorem for classical Fourier series, uniform convergence of Fourier partial sums via the Weierstrass M-test, term-by-term differentiability, and Wirtinger's inequality. In the second phase, we carry out Hurwitz's proof itself: working with simple closed $C^1$ curves given in arc-length parametrization, we reparametrize over $[0,2π]$, establish the shoelace area formula, apply integration by parts, invoke the AM--GM inequality, apply Wirtinger's inequality, and use the arc-length constraint to derive the bound $A \le L^2/(4π)$. We discuss the key formalization challenges encountered, including the interchange of infinite sums and integrals, term-by-term differentiation, and the coordination of different indexing conventions within Mathlib. The complete formalization is available at
https://github.com/mirajcs/IsoperimetricInequalityProblem
The classical isoperimetric inequality (L^2 >= 4piA) has not previously been formally verified in a proof assistant, despite its fundamental status in geometry.
Approach
The authors formalize Hurwitz's analytic proof in Lean 4 with Mathlib. The formalization proceeds in two phases: first establishing Fourier-analytic foundations (orthogonality of trigonometric functions, Parseval's theorem, Wirtinger's inequality), then formalizing simple closed curves with arc-length parametrization and deriving the inequality from the Fourier-analytic machinery.
Results
A complete formal verification of the 2D isoperimetric inequality is achieved in Lean 4, including Parseval's theorem and Wirtinger's inequality as intermediate results. The formalization demonstrates that Hurwitz's classical analytic approach can be carried through in dependent type theory.
