Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case

TL;DR

This paper formalizes the classical isoperimetric inequality in the plane using Lean 4, providing a rigorous proof based on Fourier analysis and calculus, and discusses the formalization challenges encountered.

Contribution

It is the first formal proof of the classical isoperimetric inequality in the plane using Lean 4 and Mathlib, following Hurwitz's analytic approach.

Findings

Formal proof of the isoperimetric inequality in Lean 4

Formalization of Fourier-analytic foundations

Discussion of key formalization challenges

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\pi 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 $[-\pi,\pi]$, 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\pi]$, 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\pi)$. 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/IsoperimetricInequality