🔢 mathematics

Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case

Diese Arbeit präsentiert die formale Verifizierung der klassischen isoperimetrischen Ungleichung in der Ebene mit dem Lean-4-Beweisassistenten, indem sie Adolf Hurwitz' analytischen Ansatz unter Verwendung von Fourier-Analyse und Wirtingerscher Ungleichung vollständig formalisiert.

Ursprüngliche Autoren: Miraj Samarakkody

Veröffentlicht 2026-03-17

📖 4 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Miraj Samarakkody

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Das große Seil-Experiment: Wie ein Computer bewies, dass der Kreis der König ist

Stellen Sie sich vor, Sie haben ein Seil von genau 100 Metern Länge. Ihre Aufgabe ist es, dieses Seil auf einer Wiese so auszulegen, dass es eine geschlossene Form bildet und die größtmögliche Fläche darin einschließt.

Was würden Sie tun?

Ein langes, dünnes Rechteck? (Nein, das schließt wenig ein.)
Ein Dreieck? (Besser, aber immer noch nicht optimal.)
Ein perfekter Kreis? (Ja! Das ist die Antwort, die wir intuitiv kennen.)

Dieses Rätsel nennt man das isoperimetrische Problem. Die mathematische Regel dahinter ist die isoperimetrische Ungleichung: Egal wie krumm und schief Ihr Seil liegt, die Fläche ( $A$ ) ist immer kleiner oder gleich dem Quadrat der Seillänge ( $L$ ) geteilt durch $4\pi$ . Nur der Kreis erreicht das Maximum.

Das Paper von Miraj Samarakkody erzählt die Geschichte davon, wie ein Computer (genannt Lean 4) diesen Beweis Schritt für Schritt nachvollzogen und verifiziert hat. Es ist wie ein digitaler Richter, der jeden einzelnen logischen Schritt eines menschlichen Beweises überprüft, bis kein Fehler mehr möglich ist.

Hier ist die Reise, wie der Beweis funktioniert, erklärt mit einfachen Analogien:

1. Der Detektiv-Ansatz: Fourier-Reihen als Musik

Der Beweis, den der Autor formalisiert hat, stammt von Adolf Hurwitz (1902). Statt Geometrie zu zeichnen, nutzt er Musik.

Stellen Sie sich Ihre krumme Kurve (das Seil) als ein komplexes Musikstück vor. Hurwitz sagt: "Wir können jede beliebige Form in eine Summe von einfachen Wellen zerlegen, genau wie man einen Klang in einzelne Töne (Sinus- und Kosinus-Wellen) zerlegen kann."

Die Fourier-Reihe: Das ist die Partitur, die beschreibt, wie stark jeder "Ton" (jede Welle) in Ihrer Kurve vertreten ist.
Der Trick: Der Computer lernt zuerst, wie diese Wellen sich gegenseitig beeinflussen (Orthogonalität). Wenn Sie zwei verschiedene Töne mischen, heben sie sich in bestimmten Berechnungen auf – wie zwei Wellen, die sich gegenseitig auslöschen.

2. Die Waage: Parsevals Theorem

Nun kommt eine wichtige Waage ins Spiel, genannt Parsevals Theorem.
Stellen Sie sich vor, Sie wiegen nicht die Kurve selbst, sondern die "Energie" der Töne in Ihrer Partitur.

Das Theorem sagt: Das Gewicht der Kurve (die Fläche) ist direkt mit dem Gewicht der Töne (den Koeffizienten der Wellen) verknüpft.
Der Computer hat bewiesen, dass man die Fläche der Kurve berechnen kann, indem man einfach die Quadrate aller Töne addiert. Das ist wie das Umrechnen von Musiknoten in eine Zahl.

3. Der Vergleich: Wirtingers Ungleichung

Jetzt wird es spannend. Der Computer vergleicht zwei Dinge:

Die "Ruhe" der Kurve (die Fläche).
Die "Bewegung" der Kurve (wie schnell sie sich ändert).

Es gibt eine Regel, die Wirtingers Ungleichung heißt. Sie besagt im Grunde: "Wenn eine Welle keine Verschiebung hat (sie startet und endet auf Null), dann ist ihre 'Bewegung' immer mindestens so groß wie ihre 'Ruhe'."

Die Metapher: Stellen Sie sich vor, Sie laufen eine Runde. Wenn Sie nicht geradeaus laufen, sondern hin und her wackeln, legen Sie mehr Strecke zurück, um denselben Punkt zu erreichen. Das "Wackeln" kostet Energie. Der Kreis ist die einzige Form, die nicht "wackelt" – er ist perfekt effizient.

4. Der finale Trick: Das Seil spannen

Im letzten Schritt nutzt der Computer die Tatsache, dass unser Seil eine feste Länge hat (Bogenlängen-Parametrierung).

Er nimmt die Formel für die Fläche und wendet die oben genannten Regeln an.
Durch geschicktes Umformen (wie beim Lösen eines Rätsels) zeigt er: Die Fläche kann niemals größer sein als $L^2 / 4\pi$ .
Und wann ist sie genau so groß? Nur wenn alle "Wackel-Töne" außer dem Grundton verschwinden. Das passiert nur bei einem perfekten Kreis.

Warum ist das alles so wichtig?

Man könnte sagen: "Na und, wir wissen doch schon, dass der Kreis der Beste ist."
Aber in der Mathematik gibt es oft Lücken in den Beweisen. Ein menschlicher Mathematiker sagt vielleicht: "Und hier tauschen wir einfach Summe und Integral aus" oder "Hier differenzieren wir Term für Term". Das klingt logisch, aber es ist gefährlich, wenn man die genauen Bedingungen nicht prüft.

Lean 4 ist wie ein extrem pedantischer Assistent. Er lässt keine "etwas"-Aussagen zu. Er zwingt den Autor, jede einzelne Bedingung zu beweisen:

"Ist die Funktion wirklich glatt genug?"
"Dürfen wir wirklich die Reihenfolge der Summation ändern?"
"Stimmen die Indizes der Wellen überein?"

Das Paper zeigt, dass der Autor diese Hürden genommen hat. Er hat die gesamte Logik in eine Sprache übersetzt, die der Computer versteht. Das Ergebnis ist ein unwiderlegbarer Beweis, dass der Kreis tatsächlich die perfekte Form ist.

Zusammenfassung in einem Satz

Der Autor hat einem Computer beigebracht, die Musik der Geometrie zu hören, und damit bewiesen, dass unter allen möglichen Formen, die man mit einem Seil bilden kann, nur der Kreis die maximale Fläche einschließt – und zwar mit einer mathematischen Sicherheit, die kein menschlicher Fehler mehr zulässt.

Technische Zusammenfassung: Formalisierung der klassischen isoperimetrischen Ungleichung im zweidimensionalen Fall

Verfasser: Miraj Samarakkody
Datum: 17. März 2026
Werkzeuge: Lean 4, Mathlib (Mathematik-Bibliothek)

1. Problemstellung

Das Paper adressiert die isoperimetrische Ungleichung in der Ebene. Diese besagt, dass für jede einfache geschlossene Kurve $C$ mit dem Umfang $L$ und der eingeschlossenen Fläche $A$ die folgende Ungleichung gilt:
$L^2 \ge 4\pi A$
Gleichheit tritt genau dann ein, wenn die Kurve ein Kreis ist. Das Ziel der Arbeit ist die vollständige formale Verifikation dieses klassischen Satzes unter Verwendung des Beweisassistenten Lean 4. Im Gegensatz zu informellen mathematischen Beweisen, die oft technische Details (wie den Austausch von Summen und Integralen oder Regularitätsbedingungen) implizit lassen, erfordert die formale Verifikation, dass jeder logische Schritt explizit und maschinell überprüfbar ist.

2. Methodik und Beweisstrategie

Die Arbeit folgt dem analytischen Beweisansatz von Adolf Hurwitz (1902), der die geometrische Ungleichung auf eine rein analytische Aussage mittels Fourier-Reihen reduziert. Der Formalisierungsprozess gliedert sich in zwei Hauptphasen:

Phase 1: Fourier-Analytische Grundlagen

Bevor der eigentliche Beweis geführt werden kann, mussten die notwendigen analytischen Werkzeuge in Mathlib etabliert oder adaptiert werden:

Orthogonalität trigonometrischer Funktionen: Formale Beweise für die Orthogonalitätsrelationen von $\sin(nx)$ und $\cos(mx)$ über $[-\pi, \pi]$ .
Parsevals Theorem: Herleitung der Identität, die das Quadrat der $L^2$ -Norm einer Funktion mit der Summe der Quadrate ihrer Fourier-Koeffizienten verknüpft.
Gleichmäßige Konvergenz: Anwendung des Weierstraßschen M-Tests, um die gleichmäßige Konvergenz der Fourier-Reihen und ihrer partiellen Summen zu garantieren.
Gliederweise Differentiation: Beweis der Bedingung, unter der eine Fourier-Reihen differenziert werden darf (erfordert die Konvergenz der abgeleiteten Reihe).
Wirtingers Ungleichung: Herleitung dieser funktionalanalytischen Ungleichung, die die $L^2$ -Norm einer Funktion mit der ihrer Ableitung vergleicht, basierend auf Parsevals Theorem.

Phase 2: Der Beweis der isoperimetrischen Ungleichung

Aufbauend auf den Grundlagen wird Hurwitz' Beweis für eine einfache geschlossene $C^1$ -Kurve $\gamma$ (parametrisiert nach Bogenlänge) durchgeführt:

Reparametrisierung: Die Kurve wird von $[0, L]$ auf $[0, 2\pi]$ umparametrisiert, um Fourier-Methoden anwenden zu können.
Flächenformel (Shoelace-Formel): Die Fläche $A$ wird mittels des Satzes von Green als Integral ausgedrückt: $A = \int_0^{2\pi} f(\theta)g'(\theta) d\theta$ (nach partieller Integration).
AM-GM-Ungleichung: Anwendung der arithmetisch-geometrischen Mittel-Ungleichung ( $2uv \le u^2 + v^2$ ), um $A$ durch Integrale von $f^2$ und $(g')^2$ nach oben abzuschätzen.
Anwendung von Wirtingers Ungleichung: Unter der Annahme, dass der Schwerpunkt in $x$ -Richtung bei Null liegt (was durch Verschiebung erreicht werden kann), wird Wirtingers Ungleichung auf $f$ angewendet ( $\int f^2 \le \int (f')^2$ ).
Bogenlängen-Constraint: Da die Kurve nach Bogenlänge parametrisiert ist, gilt $(f')^2 + (g')^2 = (L/2\pi)^2$ .
Ergebnis: Einsetzen dieser Konstante führt direkt zu $A \le L^2/(4\pi)$ .

3. Schlüsselbeiträge und technische Herausforderungen

Die Arbeit ist nicht nur eine Verifikation, sondern auch eine Fallstudie für die Formalisierung fortgeschrittener Analysis in Lean 4.

Interaktion von Summen und Integralen: Ein zentrales Problem war die rechtmäßige Vertauschung von unendlichen Summen und Integralen. Dies erforderte die explizite Anwendung des Dominated Convergence Theorem (dominierter Konvergenzsatz) und die Formulierung strenger Summierbarkeits-Hypothesen ( $\sum (|a_n| + |b_n|) < \infty$ ).
Gliederweise Differentiation: Die Differentiation der Fourier-Reihe erforderte den Nachweis der gleichmäßigen Konvergenz der Ableitungsreihe. Eine technische Schwierigkeit bestand in der Verschiebung der Indizes (Fourier-Reihen sind oft über $\mathbb{N}^+$ indiziert, während die Lean-Theoreme für partielle Summen oft über $\mathbb{N}$ arbeiten).
Geometrische Modellierung: Die Kurven wurden als Struktur SimpleClosedC1Curve modelliert, die in EuclideanSpace R (Fin n) abbildet. Die Herausforderung bestand darin, die Ableitungen der Koordinatenfunktionen ( $x(t), y(t)$ ) korrekt mit der Fréchet-Ableitung des Vektorfeldes $\gamma(t)$ zu verknüpfen, unter Verwendung von Projektionen (PiLp.proj).
Index-Konventionen: Die Harmonisierung unterschiedlicher Indexierungs-Konventionen in Mathlib (natürliche Zahlen vs. positive natürliche Zahlen) erforderte sorgfältige Umformungen mittels Äquivalenzen (Equiv.pnatEquivNat).

4. Ergebnisse

Die Arbeit liefert einen vollständig formalisierten Beweis für die isoperimetrische Ungleichung in Lean 4. Die wichtigsten formal verifizierten Sätze umfassen:

Orthogonalitäts-Lemmas für trigonometrische Funktionen.
Parsevals Theorem für klassische Fourier-Reihen mit expliziten Koeffizientenfolgen.
Wirtingers Ungleichung (in ihrer Identitätsform und als Ungleichung).
Der Hauptsatz: Für jede einfache geschlossene $C^1$ -Kurve gilt $A \le L^2/(4\pi)$ .

Der vollständige Code ist unter https://github.com/mirajcs/IsoperimetricInequality verfügbar.

5. Bedeutung und Ausblick

Verlässlichkeit: Der Beweis eliminiert jegliche Unklarheit bezüglich der technischen Voraussetzungen (z. B. Regularität der Kurve, Konvergenzbedingungen), die in Lehrbuchbeweisen oft übersehen werden.
Mathlib-Beitrag: Die Arbeit erweitert die Fähigkeiten von Mathlib im Bereich der klassischen Fourier-Analyse und zeigt, wie komplexe analytische Beweise (Graduierten-Niveau) in einem abhängigen Typsystem formalisiert werden können.
Zukünftige Arbeiten:
- Herleitung der Hypothesen: Derzeit werden die Parseval- und Wirtinger-Identitäten als Hypothesen angenommen. Ein zukünftiges Ziel ist es, diese direkt aus der Definition der Kurve und ihren Fourier-Koeffizienten abzuleiten.
- Gleichheitsfall: Die Charakterisierung des Falls, in dem Gleichheit herrscht (d. h. die Kurve ist ein Kreis), steht noch aus.
- Verallgemeinerung: Die Erweiterung auf Kurven mit geringerer Regularität (z. B. beschränkte Variation) oder auf höhere Dimensionen ( $\mathbb{R}^n$ ).

Zusammenfassend demonstriert dieses Paper, wie moderne Beweisassistenten genutzt werden können, um klassische mathematische Theoreme mit einer Präzision zu verifizieren, die über menschliche Überprüfung hinausgeht, und liefert dabei wertvolle Erkenntnisse für die Entwicklung formaler Bibliotheken in der Analysis.