Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case
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 $[-π,π]$,…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2603.14663
curl -X POST /api/v1/records/arxiv/2603.14663/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2603.14663/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'