🔢 mathematics

Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case

Cet article présente une vérification formelle de l'inégalité isopérimétrique classique dans le plan à l'aide de l'assistant de preuve Lean 4, en suivant l'approche analytique d'Adolf Hurwitz qui repose sur l'analyse de Fourier et l'inégalité de Wirtinger.

Auteurs originaux : Miraj Samarakkody

Publié 2026-03-17

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Miraj Samarakkody

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

🌟 Le Défi de la Reine Didon : Une Histoire de Formes et de Limites

Imaginez que vous êtes la reine Didon, il y a des milliers d'années. Vous avez reçu une peau de taureau et on vous dit : « Prends autant de terre que tu peux entourer avec cette peau. »

Si vous posez la peau en un seul bloc, vous obtenez un petit carré. Mais si vous coupez la peau en fines lanières, que vous les liez bout à bout pour former une longue corde, et que vous tracez un cercle parfait sur la plage... vous obtiendrez une surface énorme !

C'est le cœur du problème isopérimétrique : parmi toutes les formes possibles que l'on peut dessiner avec une corde de longueur fixe, laquelle enferme le plus grand espace ? La réponse intuitive est : le cercle.

Ce papier est une aventure moderne où l'auteur, Miraj, ne se contente pas de dire « c'est évident ». Il utilise un ordinateur très intelligent (appelé Lean 4) pour prouver mathématiquement, pas à pas, que le cercle est bien le champion incontesté.

🤖 L'Avocat Robot : Pourquoi un ordinateur ?

En mathématiques, on écrit souvent des preuves avec des mots. Parfois, on saute des étapes en disant « c'est facile à voir » ou « on peut faire ça ». Mais un ordinateur, lui, ne croit à rien tant qu'on ne lui a pas donné la recette exacte, ingrédient par ingrédient.

Miraj a demandé à son robot mathématicien de vérifier la preuve d'Adolf Hurwitz (un génie du début du XXe siècle). Ce n'est pas juste une vérification de routine ; c'est comme transformer une recette de cuisine vague en un mode d'emploi pour un robot de cuisine qui ne tolère aucune erreur. Si le robot dit « OK », alors la preuve est absolument infaillible.

🎻 La Méthode de Hurwitz : La Symphonie des Ondes

Pour prouver que le cercle est le meilleur, Hurwitz n'a pas utilisé de géométrie classique (comme mesurer des angles). Il a utilisé la musique des mathématiques : les séries de Fourier.

Imaginez que votre courbe (votre corde) est une note de musique complexe.

Décomposition : Hurwitz dit : « Décomposons cette courbe complexe en une somme de notes simples (des vagues sinusoïdales). »
L'Analyse : Il utilise une règle magique appelée Parseval (comme un compteur d'énergie) pour comparer la taille de la courbe à la somme de ses notes.
La Règle de l'Or : Il applique une autre règle, l'inégalité de Wirtinger, qui dit essentiellement : « Plus une vague oscille vite, plus elle consomme d'énergie. »

Le résultat de cette symphonie mathématique est une équation simple :

La surface (A) est toujours inférieure ou égale à (Longueur²) / (4 × Pi).

Et devinez quoi ? L'égalité n'est atteinte que si la courbe est un cercle parfait. Si vous déformez le cercle, la surface diminue.

🧱 Les Briques du Construction (Les Défis)

Le papier explique aussi les difficultés rencontrées par Miraj pour convaincre l'ordinateur. C'est comme essayer de construire un château de cartes avec des règles très strictes :

Le problème des infinis : La preuve utilise des sommes infinies de notes. L'ordinateur doit être convaincu qu'on peut échanger l'ordre du calcul (sommer avant d'intégrer, ou vice-versa) sans faire exploser le résultat. C'est comme essayer de compter les grains de sable d'une plage tout en les mélangeant : il faut des règles précises pour ne pas en perdre un seul.
La déformation de la corde : Pour faire les calculs, il faut redéfinir la façon dont on mesure la corde (paramétrisation par la longueur d'arc). C'est comme si on devait s'assurer que votre corde est toujours tendue à la même vitesse, peu importe où vous êtes dessus.
Le langage de l'ordinateur : L'ordinateur parle un langage très technique (type dépendant). Il faut traduire les concepts géométriques (courbes, aires) en ce langage rigide. Parfois, l'ordinateur s'arrête parce qu'on a utilisé une virgule au lieu d'un point, ou parce qu'on a oublié de préciser que la courbe est lisse.

🏆 Le Résultat Final

À la fin de l'histoire, Miraj a réussi à faire dire à l'ordinateur : « C'est prouvé. »

Il a créé une bibliothèque de code (disponible sur internet) qui contient cette preuve. C'est une victoire double :

On sait avec une certitude absolue que le cercle est la forme la plus efficace.
On a appris à l'ordinateur à comprendre des concepts mathématiques avancés, ce qui ouvre la porte à de futures découvertes où les machines aideront les humains à résoudre des problèmes encore plus complexes.

En résumé : C'est l'histoire d'un humain qui a pris un vieux problème de géométrie, l'a démonté en notes de musique, et a demandé à un robot de vérifier chaque note pour s'assurer que le cercle est bien le roi incontesté des formes.

1. Problématique et Contexte

Le papier traite de la formalisation complète de la preuve de l'inégalité isopérimétrique classique en dimension deux à l'aide de l'assistant de preuves Lean 4 et de sa bibliothèque mathématique Mathlib.

L'inégalité isopérimétrique stipule que pour toute courbe fermée simple de périmètre $L$ et d'aire $A$ dans le plan, la relation suivante est vérifiée :
$L^2 \ge 4\pi A$
L'égalité est atteinte si et seulement si la courbe est un cercle. Bien que ce résultat soit bien connu et possède plusieurs preuves historiques (Steiner, Weierstrass), l'auteur choisit de formaliser la preuve analytique d'Adolf Hurwitz (1902). Cette approche est privilégiée car elle évite le calcul des variations et repose sur l'analyse de Fourier, ce qui se prête particulièrement bien à une vérification formelle rigoureuse.

2. Méthodologie et Stratégie de Preuve

La formalisation suit une approche structurée en deux phases principales, s'appuyant sur la théorie des séries de Fourier classiques.

Phase 1 : Fondations de l'analyse de Fourier

Avant d'attaquer la preuve géométrique, l'auteur développe les outils analytiques nécessaires dans Mathlib :

Orthogonalité trigonométrique : Preuve des relations d'orthogonalité des fonctions $\cos(nx)$ et $\sin(nx)$ sur l'intervalle $[-\pi, \pi]$ .
Convergence uniforme : Utilisation du critère M de Weierstrass pour établir la convergence uniforme des sommes partielles des séries de Fourier sous des hypothèses de sommabilité des coefficients.
Différentiation terme à terme : Démonstration que la série dérivée converge uniformément vers la dérivée de la fonction, sous des conditions de régularité plus strictes (sommabilité de $n(|a_n| + |b_n|)$ ).
Théorème de Parseval : Formalisation de l'identité reliant la norme $L^2$ d'une fonction à la somme des carrés de ses coefficients de Fourier.
Inégalité de Wirtinger : Preuve de cette inégalité fonctionnelle (cas particulier de l'inégalité de Poincaré) en utilisant le théorème de Parseval. Elle établit que pour une fonction périodique de moyenne nulle, $\int f^2 \le \int (f')^2$ .

Phase 2 : La preuve de Hurwitz

L'auteur applique ensuite ces outils à une courbe fermée simple $C^1$ , notée $\gamma$ , paramétrée par la longueur d'arc sur $[0, L]$ .

Reparamétrisation : La courbe est reparamétrée sur l'intervalle $[0, 2\pi]$ via des fonctions $f(\theta)$ et $g(\theta)$ représentant les coordonnées $x$ et $y$ .
Formule de l'aire : L'aire $A$ est exprimée via la formule du « shoelace » (Green) : $A = \int_0^{2\pi} f(\theta)g'(\theta) d\theta$ (après intégration par parties).
Inégalité AM-GM : Application de l'inégalité arithmético-géométrique $2fg' \le f^2 + (g')^2$ pour majorer l'aire.
Application de Wirtinger : En supposant que le centroïde est à l'origine (ce qui permet de rendre la moyenne de $f$ nulle), l'inégalité de Wirtinger permet de remplacer $\int f^2$ par $\int (f')^2$ .
Contrainte de longueur d'arc : L'hypothèse de paramétrisation par la longueur d'arc implique que $(f')^2 + (g')^2 = (L/2\pi)^2$ .
Conclusion : En combinant ces étapes, on obtient $A \le \frac{1}{2} \int_0^{2\pi} (L/2\pi)^2 d\theta = \frac{L^2}{4\pi}$ .

3. Contributions Techniques Clés et Défis de Formalisation

L'article met en lumière plusieurs défis techniques rencontrés lors de l'implémentation dans Lean 4, offrant des leçons pour la formalisation de l'analyse classique :

Échange sommes-intégrales : La justification rigoureuse de l'échange entre la somme infinie et l'intégrale (nécessaire pour Parseval) a requis l'utilisation explicite du théorème de convergence dominée (Dominated Convergence Theorem) de Mathlib, avec des hypothèses de sommabilité $L^1$ soigneusement formulées.
Différentiation terme à terme : La preuve de la dérivabilité terme à terme a nécessité la gestion subtile de la convergence uniforme des séries dérivées et la résolution d'un décalage d'indexation entre les sommes indexées sur $\mathbb{N}^+$ (naturelles positives) et les théorèmes de dérivée de Mathlib indexés sur $\mathbb{N}$ .
Espaces Euclidiens et Projections : La modélisation des courbes dans $\mathbb{R}^2$ utilise le type EuclideanSpace R (Fin 2). L'auteur a dû gérer soigneusement les projections sur les coordonnées et leur différentiation (composition de la dérivée de Fréchet de la projection avec la dérivée de la courbe).
Intégration par parties : La preuve de l'intégration par parties pour les fonctions périodiques a nécessité l'établissement préalable de la continuité des dérivées reparamétrisées via la règle de la chaîne.
Hypothèses de Parseval et Wirtinger : Une limitation notée est que les identités de Parseval et Wirtinger pour la fonction reparamétrisée spécifique sont prises comme hypothèses dans le théorème principal, car la dérivation complète de ces coefficients à partir de la définition de la courbe (nécessitant des résultats d'intégrabilité supplémentaires) reste un travail ouvert.

4. Résultats Principaux

Le papier présente une bibliothèque Lean 4 complète contenant :

Des lemmes d'orthogonalité trigonométrique.
Une preuve formelle du théorème de Parseval pour les séries de Fourier réelles.
La preuve de l'inégalité de Wirtinger via Parseval.
La définition formelle des courbes fermées simples $C^1$ et de leur paramétrisation par la longueur d'arc.
La preuve complète de l'inégalité isopérimétrique $A \le L^2/(4\pi)$ selon la méthode de Hurwitz.

Le code source est disponible publiquement sur GitHub.

5. Signification et Impact

Ce travail est significatif à plusieurs égards :

Rigueur Mathématique : Il fournit un enregistrement définitif et vérifié par machine de la preuve de Hurwitz, éliminant les ambiguïtés souvent présentes dans les preuves manuscrites (notamment sur les conditions de régularité et les échanges limites/intégrales).
Avancement de Mathlib : Il démontre la capacité de Lean 4 et de Mathlib à gérer des preuves d'analyse réelle de niveau master, en particulier l'analyse harmonique classique.
Étude de Cas : Il sert de référence pour les futurs projets de formalisation en analyse, documentant les stratégies pour gérer la convergence uniforme, les séries infinies et les espaces euclidiens.
Complémentarité : Il s'ajoute à d'autres grandes preuves formelles (comme l'expérience du tenseur liquide ou l'éversion de la sphère), enrichissant le corpus de mathématiques formelles dans le domaine de l'analyse géométrique.

En résumé, ce papier réussit à traduire une preuve élégante mais technique du début du XXe siècle dans un langage formel moderne, validant non seulement le théorème, mais aussi la robustesse de l'infrastructure de preuve Lean 4 pour l'analyse complexe.