{"id":"arxiv/2603.14663","url":"https://arxiv.org/abs/2603.14663","tags":["math.MG","cs.LO"],"score":0,"title":"Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case","domain":"math.MG","source":"arxiv","authors":["Miraj Samarakkody"],"reviews":0,"subject":"math.MG","summary":"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 $[-π,π]$,…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-03-15","reactions":{}}