Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case

Miraj Samarakkody

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 Hurwi…