🔢 mathematics

Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case

Dit artikel beschrijft de formele verificatie van de klassieke isoperimetrische ongelijkheid in het tweedimensionale vlak met behulp van de Lean 4-bewijshulp en Mathlib, waarbij het analytische bewijs van Adolf Hurwitz via Fourier-analyse volledig is geïmplementeerd.

Oorspronkelijke auteurs: Miraj Samarakkody

Gepubliceerd 2026-03-17

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Miraj Samarakkody

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een stuk touw hebt van een vaste lengte. Je mag dit touw op de grond leggen om een vorm te maken. De vraag is: welke vorm sluit het grootste gebied in?

Het antwoord is eeuwenoud: een cirkel. Als je een vierkant, een driehoek of een willekeurige kromme maakt met hetzelfde touw, is de cirkel altijd de winnaar. Dit heet de isoperimetrische ongelijkheid.

Deze paper vertelt het verhaal van hoe een onderzoeker, Miraj Samarakkody, dit bewijs niet alleen op papier heeft geschreven, maar het helemaal heeft laten controleren door een computer. Hij gebruikte een speciaal computerprogramma genaamd Lean 4.

Hier is een uitleg in simpele taal, met een paar creatieve vergelijkingen:

1. Waarom een computer? (De "Super-Grondwet")

In de wiskunde schrijven mensen bewijzen op. Maar mensen kunnen kleine foutjes maken, of dingen over het hoofd zien die ze als "zelfsprekend" beschouwen.
Stel je voor dat je een wetboek schrijft. Als je zegt "en dan gebeurt er vanzelf dit...", en je vergeet een belangrijke regel, kan dat later problemen geven.

Lean 4 is als een super-strengere rechter of een computer die geen enkele stap accepteert tenzij die stap logisch 100% klopt. Het is alsof je een bouwwerk bouwt en elke steen, elke mortel en elke hoek door een robot laat controleren op perfectie. Als de robot zegt "Goed", dan is het bewijs onfeilbaar.

2. De Oplossing: De "Muzikale" Benadering

De paper gebruikt een bewijs van een wiskundige uit 1902, Adolf Hurwitz. Hij deed iets heel slimme: hij keek niet naar de vorm van het touw als een tekening, maar als muziek.

De Analogie: Stel je voor dat de vorm van je touw een liedje is. Elke vorm kan worden opgebouwd uit verschillende "toonhoogtes" (golven), net zoals een symfonie uit verschillende instrumenten bestaat.
In wiskundetaal noemen we dit Fourier-series. Het is alsof je een ingewikkelde kromme ontleden in simpele golven (zoals een gitaarsnaar die trilt).

Hurwitz bewees dat als je deze "muziek" analyseert, de cirkel de enige vorm is die de "energie" (het gebied) maximaliseert.

3. De Twee Delen van het Avontuur

De paper beschrijft twee grote fases in dit computerbewijs:

Fase 1: De Muziektheorie (De Basis)

Voordat je het liedje kunt analyseren, moet je de regels van de muziektheorie op de computer zetten.

Orkestratie: De computer leerde hoe de verschillende golven (sinus en cosinus) met elkaar interageren. Ze "luisteren" niet naar elkaar als ze verschillende tonen zijn (orthogonaliteit).
De M-test: Dit is een regel die zegt: "Als de geluidssterkte van alle instrumenten samen niet te hard wordt, dan is het hele orkest veilig en stabiel." Dit zorgt ervoor dat de computer de oneindige som van golven veilig kan berekenen.
Parseval's Theorema: Dit is een soort "rekenregel" die zegt: "De totale energie van het liedje (het gebied) is gelijk aan de som van de energie van alle losse instrumenten."

Fase 2: Het Bewijs (De Daad)

Nu de computer de muziektheorie kent, kan hij Hurwitz's bewijs volgen:

Het Gebied Berekenen: De computer gebruikt een formule (de "schoenriem-formule") om het gebied binnen het touw te meten.
De Wisselwerking: Hij gebruikt een slimme truc (integratie door delen) om de formule te vereenvoudigen.
De Vergelijking: Hij vergelijkt het gebied met de lengte van het touw.
De Cirkel: Uiteindelijk toont de computer aan dat voor elke andere vorm dan een cirkel, de "energie" van de golven er voor zorgt dat het gebied kleiner is dan het maximum. Alleen bij een perfecte cirkel is alles in balans.

4. De Uitdagingen (Waarom was dit moeilijk?)

Het was niet zomaar "typen en klaar". De auteur stuitte op valkuilen die in een normaal boekje vaak worden overgeslagen:

Oneindigheid: Computers houden niet van "oneindig". Ze moeten precies weten hoe je een oneindige som en een integraal (een oppervlakte) mag verwisselen. De auteur moest de computer uitleggen dat het veilig is om dit te doen (net als het voorzichtig verwisselen van blokken in een toren zonder dat hij instort).
Aandelen: Soms moet je een formule "term voor term" afleiden. De computer moest precies weten welke regels hier gelden, anders zou het resultaat fout zijn.
Taalproblemen: De wiskundige notatie in boeken en de "taal" van de computer (Lean) spreken soms een beetje anders. De auteur moest een vertaler zijn om de concepten van Hurwitz naar de computer te vertalen.

Conclusie: Waarom is dit belangrijk?

Je zou kunnen vragen: "Waarom moeten we iets dat al 2000 jaar bekend is, opnieuw bewijzen met een computer?"

Zekerheid: Het geeft ons 100% zekerheid dat er geen verborgen fouten in de logica zitten.
Leren: Het dwingt ons om elke stap, hoe klein ook, expliciet te maken. Vaak zien we pas tijdens het programmeren dat we iets als "zelfsprekend" hadden beschouwd, terwijl het eigenlijk heel complex is.
De Toekomst: Dit is een stap in de richting van een wereld waar computers ons helpen de meest complexe wetenschappelijke ontdekkingen te verifiëren.

Kortom: Deze paper is als het bouwen van een onbreekbaar glazen huis rondom een klassiek wiskundig meesterwerk. Het laat zien dat de cirkel echt de koning is van de vormen, en dat zelfs een computer het niet kan weerleggen.

Titel: Formalisering van de Klassieke Isoperimetrische Ongelijkheid in het Tweedimensionale Geval

Auteur: Miraj Samarakkody
Datum: 17 maart 2026
Context: Formele verificatie met Lean 4 en Mathlib.

1. Het Probleem

De isoperimetrische ongelijkheid is een fundamenteel resultaat in de meetkunde en analyse. Het stelt dat voor elke eenvoudige gesloten kromme in het vlak met een omtrek $L$ en een ingesloten oppervlakte $A$ , de volgende ongelijkheid geldt:
$L^2 \ge 4\pi A$
Gelijkheid treedt op dan en slechts dan als de kromme een cirkel is. Hoewel dit resultaat bekend is sinds de oudheid en in de 19e en 20e eeuw rigoureus is bewezen (o.a. door Steiner, Weierstrass en Hurwitz), bevat de klassieke bewijsvoering vaak technische stappen die in handmatige bewijzen vaak over het hoofd worden gezien of impliciet worden aangenomen. Deze stappen omvatten:

Het verwisselen van oneindige sommen en integralen.
Term-voor-term differentiatie van Fourier-reeksen.
De exacte regulariteitsvoorwaarden (differentieerbaarheid) die nodig zijn voor de geldigheid van de stellingen.

Het doel van dit artikel is om een volledig machine-verifieerbaar bewijs te leveren van deze ongelijkheid voor $C^1$ -krommen, gebruikmakend van de bewijshulp Lean 4.

2. Methodologie

De auteur volgt de analytische aanpak van Adolf Hurwitz (1902), die het probleem reduceert tot een vergelijking van Fourier-coëfficiënten via Parseval's identiteit, in plaats van variatierekening te gebruiken. De formalisatie verloopt in twee hoofdfasen:

Fase 1: Fourier-analytische Fundamenten

De eerste fase richt zich op het opbouwen van de benodigde theorie binnen de Mathlib-bibliotheek van Lean 4:

Orthogonaliteit: Formele bewijzen van de orthogonaliteitsrelaties voor trigonometrische functies ( $\sin, \cos$ ) over het interval $[-\pi, \pi]$ .
Convergentie: Toepassing van de Weierstrass M-toets om uniforme convergentie van de Fourier-partiële sommen te garanderen onder de voorwaarde dat de som van de absolute coëfficiënten convergeert ( $\sum (|a_n| + |b_n|) < \infty$ ).
Differentiatie: Bewijs van term-voor-term differentieerbaarheid van de Fourier-reeks, wat een sterkere convergentievoorwaarde vereist ( $\sum n(|a_n| + |b_n|) < \infty$ ).
Parseval's Stelling: Formalisering van de identiteit die de $L^2$ -norm van een functie relateert aan de som van de kwadraten van haar Fourier-coëfficiënten.
Wirtinger's Ongelijkheid: Een ongelijkheid die de $L^2$ -norm van een periodieke functie met gemiddelde nul relateert aan de $L^2$ -norm van haar afgeleide.

Fase 2: Het Bewijs van Hurwitz

In de tweede fase wordt de ongelijkheid zelf bewezen voor een eenvoudige gesloten $C^1$ -kromme $\gamma$ met booglengte $L$ :

Reparametrisatie: De kromme wordt gereparametriserd over het interval $[0, 2\pi]$ via $f(\theta)$ en $g(\theta)$ .
Oppervlakteformule: De oppervlakte $A$ wordt uitgedrukt met de "shoelace"-formule (Green's stelling) en vereenvoudigd via partiële integratie tot $A = \int_0^{2\pi} f(\theta)g'(\theta) d\theta$ .
AM-GM Ongelijkheid: Toepassing van $2fg' \le f^2 + (g')^2$ om een bovengrens voor $A$ te vinden.
Toepassing van Wirtinger: Onder de aanname dat het zwaartepunt in de $x$ -richting op de oorsprong ligt (wat een translatie mogelijk maakt), wordt Wirtinger's ongelijkheid toegepast: $\int f^2 \le \int (f')^2$ .
Booglengte-beperking: Omdat de kromme geparametriseerd is naar booglengte, geldt $(f')^2 + (g')^2 = (L/2\pi)^2$ .
Conclusie: Door deze stappen te combineren wordt afgeleid dat $A \le L^2/(4\pi)$ .

3. Belangrijkste Bijdragen en Technische Uitdagingen

De paper documenteert niet alleen het bewijs, maar ook de specifieke uitdagingen bij het vertalen van wiskundige intuïtie naar strikte code in Lean 4:

Verwisselen van Sommen en Integralen: In handmatige bewijzen wordt dit vaak kort afgedaan. In Lean vereist dit expliciete vermelding van de Gedomineerde Convergentiestelling (Dominated Convergence Theorem) en het aantonen van de $L^1$ -sommeerbaarheid van de termen.
Indexering en Notatie: Er was sprake van een mismatch tussen de wiskundige notatie (waarbij Fourier-coëfficiënten vaak geïndexeerd zijn op $\mathbb{N}^+$ ) en de standaardbibliotheken van Mathlib (die vaak werken met $\mathbb{N}$ ). De auteur moest complexe herschikkingen (via Equiv.pnatEquivNat) implementeren om deze conventies te verenigen.
Differentiatie van Reeksen: Het bewijs van term-voor-term differentiatie vereiste het combineren van uniforme convergentie van de afgeleide reeks met de convergentie van de oorspronkelijke reeks, waarbij specifieke lemmas over TendstoUniformly en HasDerivAt moesten worden gekoppeld.
EuclideanSpace en Projecties: Het werken met coördinaatfuncties in $\mathbb{R}^2$ (gemodelleerd als EuclideanSpace R (Fin 2)) vereiste zorgvuldig gebruik van projectiemappingen en het combineren van Frechet-afgeleiden met de klassieke afgeleiden van de coördinaatfuncties.
Hypothese-structuur: In de uiteindelijke hoofdstelling worden de Parseval- en Wirtinger-identiteiten voor de specifieke functie $fParm$ als hypothesen aangenomen, omdat het volledig afleiden hiervan vanuit de definitie van de kromme (via integraalformules voor coëfficiënten) buiten de scope van dit specifieke bewijs valt en een toekomstige uitbreiding vereist.

4. Resultaten

De paper presenteert een volledig geformaliseerd bewijs dat de volgende resultaten bevat:

Een correcte formalisatie van de orthogonaliteit van trigonometrische functies.
Een bewijs van Parseval's stelling en Wirtinger's ongelijkheid binnen de context van klassieke Fourier-reeksen.
Een rigoureus bewijs van de isoperimetrische ongelijkheid $A \le L^2/(4\pi)$ voor $C^1$ -krommen met continue afgeleiden.
De volledige code is beschikbaar op GitHub (https://github.com/mirajcs/IsoperimetricInequality).

5. Betekenis en Toekomstperspectief

Deze formalisatie is significant omdat:

Zekerheid: Het biedt een machine-verifieerde garantie dat het klassieke bewijs van Hurwitz logisch waterdicht is, inclusief de vaak verwaarloosde technische details.
Case Study voor Mathlib: Het dient als een voorbeeld van hoe geavanceerde analyse (Fourier-theorie, variatierekening, integraalrekening) kan worden geïmplementeerd in Lean 4, en identificeert waar de huidige bibliotheek nog beperkingen heeft (bijv. het automatisch verbinden van functies met hun Fourier-coëfficiënten).
Toekomstige Werk: De auteur identificeert openstaande problemen, zoals het bewijzen van het gelijkheidsteken (karakterisering van de cirkel), het generaliseren naar krommen met lagere regulariteit (bv. $W^{1,2}$ ), en het uitbreiden naar hogere dimensies ( $\mathbb{R}^n$ ).

Samenvattend levert dit werk een cruciale bijdrage aan het veld van de formele wiskunde door een klassiek, elegant analytisch bewijs volledig te vertalen naar een machine-verifieerbare vorm, waarbij de complexiteit van de onderliggende analyse blootlegt en oplost.