🔢 mathematics

Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0

Cet article présente une formalisation complète et sans excuse de la formule de Stokes pour les cubes singuliers lisses en Lean 4, utilisant de véritables pullbacks de formes différentielles, tout en établissant des ponts vers mathlib4, en vérifiant des propriétés au niveau des chaînes comme $d^2=0$ , et en comparant la mise en œuvre avec la formalisation de Harrison dans HOL Light.

Auteurs originaux : David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

Publié 2026-05-05

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

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

Imaginez que vous avez une forme très complexe et multidimensionnelle, comme un morceau de papier froissé ou un ruban tordu flottant dans l'espace. En mathématiques, il existe une règle célèbre appelée théorème de Stokes. Considérez-la comme une « règle comptable » universelle pour les formes. Elle énonce que si vous voulez connaître l'« activité » totale se produisant à l'intérieur d'une forme (comme le vent total tourbillonnant dans une tornade), vous n'avez pas besoin de mesurer chaque point individuel à l'intérieur. Au lieu de cela, vous n'avez besoin de mesurer que le « bord » ou la « frontière » de cette forme. La somme de toute l'activité sur le bord égale parfaitement l'activité totale à l'intérieur.

Pendant longtemps, les ordinateurs (plus précisément un programme appelé Lean 4) n'avaient pas été capables de prouver cette règle pour chaque forme possible, en particulier les formes étranges et froissées que les mathématiciens appellent « cubes singuliers ».

Ce document est un rapport sur la manière dont trois chercheurs ont finalement enseigné à l'ordinateur à prouver cette règle pour ces formes délicates, sans commettre d'erreurs ni sauter d'étapes.

Voici une décomposition de ce qu'ils ont fait, en utilisant des analogies simples :

1. L'Objectif : La Règle « Bord vs Intérieur »

Imaginez que vous peignez une pièce. Le théorème de Stokes est comme un tour de magie qui dit : « Si vous savez exactement combien de peinture a coulé des murs (la frontière), vous savez automatiquement exactement combien de peinture a été utilisée pour couvrir toute la pièce (l'intérieur). »

Les chercheurs voulaient prouver que ce tour de magie fonctionne même si la « pièce » est une forme étrange et étirée définie par une application lisse et torsadée (comme une feuille de caoutchouc étant tirée et tordue).

2. Le Tour de Magie en Trois Étapes

L'ordinateur ne pouvait pas simplement « voir » la forme entière d'un coup, alors les chercheurs ont décomposé la preuve en trois étapes logiques, comme une recette :

Étape 1 : La « Traduction » (Récupération)
Imaginez que vous avez une carte d'une ville, mais que la ville est déformée. Les chercheurs ont créé un outil pour « traduire » les mathématiques de la forme déformée vers un cube parfait et standard (comme un dé parfait). Ils ont utilisé un outil mathématique spécifique appelé « récupération » (qui est comme un photocopieur haute technologie qui copie les règles de la forme sur une grille standard).
Étape 2 : La Règle de la « Boîte Standard »
Une fois la forme traduite sur un cube parfait, ils ont pu utiliser une règle plus simple, déjà connue, qui fonctionne pour les boîtes parfaites. Ils ont prouvé que l'« activité intérieure » sur ce cube parfait égale l'« activité de bord » sur le cube parfait.
Étape 3 : L'« Adéquation des Faces »
Enfin, ils ont dû prouver que les bords du cube parfait (la version traduite) correspondaient parfaitement aux bords de la forme originale et étrange. Ils ont montré que lorsque l'on additionne les bords de la forme étrange, ils s'annulent et s'alignent exactement avec les bords du cube parfait.

3. La Connexion « Chaîne »

Les chercheurs ne l'ont pas prouvé pour une seule forme. Ils l'ont prouvé pour toute une « chaîne » de formes collées ensemble.

L'Analogie : Imaginez construire un mur avec des briques. Si vous posez deux briques ensemble, le bord où elles se touchent disparaît car il est à l'intérieur du mur. Les chercheurs ont prouvé que si vous avez une chaîne de ces formes, les bords « intérieurs » s'annulent toujours mutuellement, ne laissant que la frontière extérieure. C'est une règle fondamentale en mathématiques appelée $\partial^2 = 0$ (la frontière d'une frontière est rien). Ils l'ont prouvé en montrant que chaque fois qu'un bord apparaît, il apparaît deux fois avec des signes opposés, s'effaçant ainsi lui-même.

4. Pourquoi Cela Compte (Dans le Monde de l'Ordinateur)

Aucun « Désolé » Toléré : Dans les systèmes de preuve informatique, les programmeurs écrivent parfois « désolé » pour dire : « Je sais que c'est vrai, mais je ne l'ai pas encore prouvé. » Ce document est spécial car il contient zéro déclaration « désolé ». L'ordinateur a vérifié chaque étape et n'a trouvé aucune erreur.
Le Pont : Les chercheurs ont construit un « pont » entre deux manières différentes de faire des mathématiques dans l'ordinateur. L'une utilise des coordonnées simples (comme un tableur), et l'autre utilise des définitions abstraites et sophistiquées. Ils ont prouvé que les deux méthodes conduisent à exactement la même réponse, garantissant que l'ordinateur ne fait pas que deviner.
Lissage Réel : Ils ont exigé que les formes soient « lisses globalement », ce qui signifie qu'elles sont parfaitement lisses partout, pas seulement au milieu. Cela a rendu les mathématiques plus faciles à gérer pour l'ordinateur, même si c'est une règle plus stricte que ce dont les humains ont généralement besoin.

5. Ce Que Ce N'Est PAS

Le document est très honnête sur ses limites :

Il ne prouve pas cela pour chaque forme possible dans l'univers (comme une forme avec un coin pointu ou un trou qui change de taille).
Il ne traite pas des « variétés » (surfaces courbes comme la surface d'une sphère) de la manière complète et complexe habituelle des mathématiciens. Il s'en tient aux formes qui peuvent être mappées à partir d'un cube standard.
C'est une preuve mathématique, pas une expérience de physique. Il ne prédit pas la météo ni ne conçoit de ponts ; il prouve simplement que les règles logiques du calcul tiennent bon lorsqu'elles sont vérifiées par un ordinateur.

Résumé

En bref, ce document est une victoire pour la précision mathématique. Les chercheurs ont enseigné à un ordinateur à vérifier une règle de calcul vieille de 200 ans pour une grande variété de formes torsadées et multidimensionnelles. Ils l'ont fait en traduisant le problème dans une boîte standard, en prouvant la règle là-bas, puis en montrant que la traduction était parfaite. Le résultat est une preuve « sans erreur » que la règle « l'intérieur égale le bord » fonctionne, même pour les formes lisses les plus complexes que nous puissions imaginer.

Résumé technique : Théorème de Stokes pour les cubes singuliers lisses dans Lean 4

Énoncé du problème
À partir d'avril 2026, l'écosystème Lean 4 (spécifiquement mathlib4) manquait d'une formalisation complète du théorème de Stokes pour les formes différentielles sur les variétés lisses à bord ou pour les chaînes singulières. Bien que mathlib4 dispose du théorème de la divergence pour les boîtes alignées sur les axes et d'une dérivée extérieure abstraite (extDeriv), il ne fournissait pas encore de théorème intégrant le tiré en arrière d'une forme différentielle sur un cube singulier lisse (une application lisse d'un cube unité vers un espace euclidien arbitraire) et l'égalisant à la somme alternée des intégrales sur les faces du bord. Les formalisations existantes, telles que les travaux de Harrison dans HOL Light, couvraient des domaines convexes et polyédriques mais ne traitaient pas des paramétrisations singulières lisses ni de l'infrastructure spécifique de l'algèbre extérieure abstraite de mathlib4.

Méthodologie
Les auteurs présentent une formalisation « sans excuse » (zéro hypothèse non prouvée) qui comble le fossé entre l'intégration basée sur les coordonnées et la géométrie différentielle abstraite. Le développement repose sur trois piliers méthodologiques principaux :

Vrai tiré en arrière via la dérivée de Fréchet : La construction centrale définit le tiré en arrière d'une forme différentielle $\sigma^*\omega$ en utilisant la dérivée de Fréchet ($fderiv$) d'une application globalement $C^\infty$ $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$ . Contrairement à une simple précomposition de coefficients, cette définition applique la forme au point image $\sigma(x)$ aux vecteurs poussés en avant par $D\sigma(x)$ , adhérant aux définitions standard de la géométrie différentielle.
Réduction au Stokes pour boîte : La stratégie de preuve réduit le cas singulier au cas de la boîte alignée sur les axes. En exploitant le théorème extDeriv_pullback de mathlib4, les auteurs établissent l'identité de naturalité $d(\sigma^*\omega) = \sigma^*(d\omega)$ . Cela permet d'appliquer le théorème de Stokes pour boîte existant (dérivé du théorème de la divergence de mathlib4) à la forme tirée en arrière $\sigma^*\omega$ sur le domaine paramétrique $[0,1]^{n+1}$ .
Correspondance des faces et algèbre au niveau des chaînes : Un composant technique critique est l'« identité de correspondance des faces », qui prouve que l'intégrale de la forme tirée en arrière sur une face du bord d'une boîte correspond exactement à l'intégrale de la forme sur la face singulière correspondante. De plus, les auteurs formalisent l'identité de complexe de chaînes $\partial(\partial\sigma) = 0$ pour les chaînes singulières. Cela est réalisé non pas en définissant un homomorphisme de bord sur des boîtes non décorées, mais en construisant une involution sans point fixe et à signe inversé sur l'ensemble des indices de double bord, prouvant que les termes appariés s'annulent algébriquement.

Contributions clés
L'article livre une formalisation complète comprenant 44 modules Lean (environ 4 000 lignes) avec 205 déclarations nommées. Les contributions spécifiques incluent :

Théorème de Stokes singulier : Un théorème stipulant que pour toute application globalement $C^\infty$ $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$ et toute $n$ -forme $C^\infty$ $\omega$ , l'intégrale de $\sigma^*(d\omega)$ sur le cube unité est égale à la somme alternée des intégrales de $\sigma^*\omega$ sur les $2(n+1)$ faces.
Théorème de pont : Une preuve formelle validant que la dérivée extérieure basée sur les coordonnées des auteurs (extDerivCoord) est cohérente avec la extDeriv abstraite de mathlib4 lorsqu'elle est évaluée sur les vecteurs de base standards. Cela garantit que l'implémentation basée sur les coordonnées est mathématiquement solide par rapport à l'API abstraite de la bibliothèque.
Extensions au niveau des chaînes : L'extension du théorème de Stokes aux combinaisons linéaires formelles $\mathbb{Z}$ de cubes singuliers (chaînes singulières) via la linéarité.
Preuve de $\partial^2 = 0$ : Une preuve formelle de l'identité de complexe de chaînes $\partial(\partial\sigma) = 0$ pour les chaînes singulières, utilisant une involution combinatoire sur l'ensemble des indices des doubles faces.
Spécialisations dimensionnelles : Des instanciations directes du théorème principal retrouvant le théorème fondamental du calcul (TFC), le théorème de Green, le théorème de la divergence et le théorème de Gauss en 3D, ainsi que l'intégration par parties et la règle de Leibniz.
Audit des axiomes : Vérification que l'ensemble du développement dépend uniquement des trois axiomes standards de Lean 4 (propext, Classical.choice, Quot.sound), confirmé par 79 vérifications systématiques via #print axioms.

Résultats et portée
La formalisation prouve avec succès le théorème de Stokes pour :

Cubes singuliers lisses : Applications $\sigma$ globalement lisses sur $\mathbb{R}^{n+1}$ , intégrées sur le cube paramétrique $[0,1]^{n+1}$ .
Boîtes alignées sur les axes : $n$ -formes coordonnées sur des boîtes $[a,b] \subset \mathbb{R}^{n+1}$ .

L'article note explicitement les limitations et les limites de portée suivantes :

Pas de théorie des variétés : Le domaine d'intégration est strictement le cube paramétrique ou une boîte. Le travail ne formalise pas l'intégration sur des variétés lisses générales, ni n'utilise de partitions de l'unité, de cartes ou d'atlas.
Lissage global : Les applications singulières sont requises pour être $C^\infty$ sur tout $\mathbb{R}^{n+1}$ , une condition plus forte que la lissité sur le cube fermé seul. Ce choix a été fait pour simplifier la formalisation en évitant les arguments de régularité au bord et en assurant que la dérivée de Fréchet est bien définie partout.
Pas de sémantique de domaine-image : Le théorème traite l'intégrale comme une opération sur le domaine paramétrique. Il ne prouve pas que l'image de $\sigma$ constitue une sous-variété ou une chaîne géométrique orientée dans l'espace cible.

Signification et affirmations
Les auteurs affirment que ce travail fournit la première formalisation complète Lean 4 du théorème de Stokes pour les cubes singuliers lisses avec un vrai tiré en arrière de forme différentielle. Sa signification réside dans :

Pont entre concret et abstrait : Le modèle du « théorème de pont » valide une implémentation concrète basée sur les coordonnées contre la dérivée extérieure abstraite de mathlib4, offrant une méthodologie réutilisable pour les futures formalisations.
Réutilisation de l'infrastructure : Le développement repose fortement sur l'infrastructure existante de mathlib4 (théorème de la divergence, extDeriv_pullback), démontrant comment des composants de bibliothèque de haut niveau peuvent être composés pour prouver des théorèmes géométriques complexes sans réinventer l'analyse fondamentale.
Complémentarité : Le travail est complémentaire à la formalisation HOL Light de Harrison. Alors que Harrison couvre les domaines convexes/polyédriques avec l'intégration de jauge, ce travail couvre les paramétrisations singulières lisses en utilisant l'intégration de Bochner et l'API de géométrie différentielle de mathlib4.
Préparation fondamentale : En prouvant $\partial^2=0$ et en établissant le théorème de Stokes au niveau des chaînes, les auteurs fournissent un bloc de construction local nécessaire pour une future formalisation complète du théorème de Stokes sur les variétés lisses à bord, une fois que les API d'intégration et d'orientation des variétés de mathlib4 seront matures.

L'article conclut que bien qu'il ne résolve pas le problème de l'intégration sur des variétés générales, il établit la couche critique « chaîne cubique » avec de vrais tirés en arrière, servant de fondation vérifiée pour les extensions futures.