🔢 mathematics

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

Dieser Beitrag präsentiert eine umfassende, ohne Entschuldigungen formulierte Lean-4-Formalisierung des Satzes von Stokes für glatte singuläre Würfel unter Verwendung echter Pullbacks von Differentialformen, während er Brücken zu mathlib4 schlägt, Eigenschaften auf Kettenebene wie $d^2=0$ verifiziert und die Implementierung mit Harrisons HOL-Light-Formalisierung vergleicht.

Ursprüngliche Autoren: David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

Veröffentlicht 2026-05-05

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

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

Stellen Sie sich eine sehr komplexe, mehrdimensionale Form vor, wie ein zerknittertes Blatt Papier oder ein im Raum schwebendes verdrehtes Band. In der Mathematik gibt es eine berühmte Regel namens Satz von Stokes. Betrachten Sie ihn als eine universelle „Buchführungsregel" für Formen. Er besagt, dass Sie, wenn Sie die gesamte „Aktivität" im Inneren einer Form wissen möchten (wie den gesamten Wind, der in einem Tornado wirbelt), nicht jeden einzelnen Punkt im Inneren messen müssen. Stattdessen müssen Sie nur den „Rand" oder die „Grenze" dieser Form messen. Die Summe aller Aktivitäten am Rand entspricht genau der gesamten Aktivität im Inneren.

Lange Zeit waren Computer (speziell ein Programm namens Lean 4) nicht in der Lage, diese Regel für jede mögliche Form zu beweisen, insbesondere für die seltsamen, zerknitterten, die Mathematiker „singuläre Würfel" nennen.

Dieser Bericht handelt davon, wie drei Forscher dem Computer schließlich beibrachten, diese Regel für diese kniffligen Formen zu beweisen, ohne Fehler zu machen oder Schritte auszulassen.

Hier ist eine Aufschlüsselung dessen, was sie taten, unter Verwendung einfacher Analogien:

1. Das Ziel: Die „Rand vs. Innen"-Regel

Stellen Sie sich vor, Sie streichen einen Raum. Der Satz von Stokes ist wie ein Zaubertrick, der besagt: „Wenn Sie genau wissen, wie viel Farbe von den Wänden abgelaufen ist (der Rand), wissen Sie automatisch genau, wie viel Farbe verwendet wurde, um den ganzen Raum zu bedecken (das Innere)."

Die Forscher wollten beweisen, dass dieser Trick auch funktioniert, wenn der „Raum" eine seltsame, gestreckte Form ist, die durch eine glatte, verdrehende Abbildung definiert wird (wie ein Gummiblatt, das gezogen und verdreht wird).

2. Der dreistufige Zaubertrick

Der Computer konnte die gesamte Form nicht auf einmal „sehen", also zerlegten die Forscher den Beweis in drei logische Schritte, wie ein Rezept:

Schritt 1: Die „Übersetzung" (Pullback)
Stellen Sie sich eine Stadtkarte vor, aber die Stadt ist verzerrt. Die Forscher schufen ein Werkzeug, um die Mathematik von der verzerrten Form zurück auf einen perfekten, Standardwürfel zu „übersetzen" (wie einen perfekten Würfel). Sie verwendeten ein spezifisches mathematisches Werkzeug namens „Pullback" (was wie ein High-Tech-Kopierer ist, der die Regeln der Form auf ein Standardgitter kopiert).
Schritt 2: Die „Standard-Box"-Regel
Sobald die Form auf einen perfekten Würfel übersetzt war, konnten sie eine einfachere, bereits bekannte Regel verwenden, die für perfekte Boxen gilt. Sie bewiesen, dass die „Aktivität im Inneren" auf diesem perfekten Würfel der „Aktivität am Rand" auf dem perfekten Würfel entspricht.
Schritt 3: Das „Flächen-Matching"
Schließlich mussten sie beweisen, dass die Ränder des perfekten Würfels (die übersetzte Version) perfekt mit den Rändern der ursprünglichen, seltsamen Form übereinstimmen. Sie zeigten, dass, wenn man die Ränder der seltsamen Form addiert, sie sich aufheben und exakt mit den Rändern des perfekten Würfels ausrichten.

3. Die „Ketten"-Verbindung

Die Forscher bewiesen dies nicht nur für eine Form. Sie bewiesen es für eine ganze „Kette" von Formen, die aneinander kleben.

Die Analogie: Stellen Sie sich vor, Sie bauen eine Mauer aus Ziegeln. Wenn Sie zwei Ziegel zusammenfügen, verschwindet die Kante, an der sie sich berühren, weil sie innerhalb der Mauer liegt. Die Forscher bewiesen, dass, wenn Sie eine Kette dieser Formen haben, die „inneren" Ränder sich immer gegenseitig aufheben, sodass nur der äußere Rand übrig bleibt. Dies ist eine fundamentale Regel in der Mathematik namens $\partial^2 = 0$ (der Rand eines Randes ist nichts). Sie bewiesen dies, indem sie zeigten, dass jedes Mal, wenn eine Kante erscheint, sie zweimal mit entgegengesetzten Vorzeichen erscheint und sich effektiv auslöscht.

4. Warum dies wichtig ist (in der Welt des Computers)

Kein „Sorry" erlaubt: In Computersystemen zum Beweisen schreiben Programmierer manchmal „sorry", um zu sagen: „Ich weiß, dass dies wahr ist, aber ich habe es noch nicht bewiesen." Dieser Bericht ist besonders, weil er null „sorry"-Aussagen enthält. Der Computer überprüfte jeden einzelnen Schritt und fand keine Fehler.
Die Brücke: Die Forscher bauten eine „Brücke" zwischen zwei verschiedenen Arten, Mathematik im Computer zu betreiben. Eine Methode verwendet einfache Koordinaten (wie eine Tabellenkalkulation), die andere verwendet abstrakte, ausgefeilte Definitionen. Sie bewiesen, dass beide Methoden zum exakt gleichen Ergebnis führen und sicherstellen, dass der Computer nicht nur rät.
Echte Glattheit: Sie verlangten, dass die Formen „global glatt" sind, was bedeutet, dass sie überall perfekt glatt sind, nicht nur in der Mitte. Dies machte die Mathematik für den Computer leichter zu handhaben, auch wenn es eine strengere Regel ist als das, was Menschen normalerweise benötigen.

5. Was es NICHT ist

Der Bericht ist sehr ehrlich über seine Grenzen:

Er beweist dies nicht für jede mögliche Form im Universum (wie eine Form mit einer scharfen Ecke oder einem Loch, das seine Größe ändert).
Er befasst sich nicht mit „Mannigfaltigkeiten" (gekrümmte Oberflächen wie die Oberfläche einer Kugel) auf die vollständige, komplexe Weise, wie Mathematiker es normalerweise tun. Er hält sich an Formen, die von einem Standardwürfel abgebildet werden können.
Es ist ein mathematischer Beweis, kein Physikexperiment. Er sagt kein Wetter voraus und entwirft keine Brücken; er beweist einfach, dass die logischen Regeln der Analysis standhalten, wenn sie von einem Computer überprüft werden.

Zusammenfassung

Kurz gesagt ist dieser Bericht ein Sieg für mathematische Präzision. Die Forscher brachten einem Computer bei, eine 200 Jahre alte Regel der Analysis für eine Vielzahl von verdrehten, mehrdimensionalen Formen zu verifizieren. Sie taten dies, indem sie das Problem in eine Standardbox übersetzten, die Regel dort bewiesen und dann zeigten, dass die Übersetzung perfekt war. Das Ergebnis ist ein „fehlerfreier" Beweis, dass die Regel „Innen gleich Rand" funktioniert, selbst für die kompliziertesten glatten Formen, die wir uns vorstellen können.

Technisches Fazit: Stokes-Theorem für glatte singuläre Würfel in Lean 4

Problemstellung
Stand April 2026 fehlte im Lean-4-Ökosystem (speziell mathlib4) eine vollständige Formalisierung des Stokes-Theorems für Differentialformen auf glatten Mannigfaltigkeiten mit Rand oder für singuläre Ketten. Zwar verfügte mathlib4 über den Divergenzsatz für achsenparallele Boxen und einen abstrakten äußeren Differentialoperator (extDeriv), bot jedoch noch keinen Satz, der das Integral des Pullbacks einer Differentialform über einen glatten singulären Würfel (eine glatte Abbildung von einem Einheitswürfel in einen beliebigen euklidischen Raum) integriert und ihn mit der alternierenden Summe der Integrale über die Randflächen gleichsetzt. Bestehende Formalisierungen, wie Harrisons Arbeit in HOL Light, behandelten konvexe und polyedrische Bereiche, adressierten jedoch weder glatte singuläre Parametrisierungen noch die spezifische Infrastruktur der abstrakten äußeren Algebra von mathlib4.

Methodik
Die Autoren präsentieren eine „sorry-freie" Formalisierung (null unbewiesene Annahmen), die die Lücke zwischen koordinatenbasierter Integration und abstrakter Differentialgeometrie schließt. Die Entwicklung stützt sich auf drei methodische Hauptpfeiler:

Echter Pullback via Fréchet-Ableitung: Die Kernkonstruktion definiert den Pullback einer Differentialform $\sigma^*\omega$ unter Verwendung der Fréchet-Ableitung ($fderiv$) einer global $C^\infty$ -Abbildung $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$ . Im Gegensatz zur einfachen Präkomposition von Koeffizienten wendet diese Definition die Form am Bildpunkt $\sigma(x)$ auf Vektoren an, die durch $D\sigma(x)$ vorwärts geschoben wurden, und hält sich dabei an die Standarddefinitionen der Differentialgeometrie.
Reduktion auf Box-Stokes: Die Beweisstrategie reduziert den singulären Fall auf den Fall der achsenparallelen Box. Durch Ausnutzung des extDeriv_pullback-Theorems von mathlib4 etablieren die Autoren die Natürlichkeitsidentität $d(\sigma^*\omega) = \sigma^*(d\omega)$ . Dies ermöglicht die Anwendung des bestehenden Box-Stokes-Theorems (abgeleitet vom Divergenzsatz von mathlib4) auf die zurückgezogene Form $\sigma^*\omega$ über den Parameterraum $[0,1]^{n+1}$ .
Flächen-Matching und Ketten-Level-Algebra: Ein kritischer technischer Bestandteil ist die „Flächen-Matching-Identität", die beweist, dass das Integral der zurückgezogenen Form über eine Box-Randfläche exakt dem Integral der Form über die entsprechende singuläre Fläche entspricht. Darüber hinaus formalisieren die Autoren die Kettenkomplex-Identität $\partial(\partial\sigma) = 0$ für singuläre Ketten. Dies wird nicht durch die Definition eines Randhomomorphismus auf ungeschmückten Boxen erreicht, sondern durch die Konstruktion einer vorzeichenumkehrenden, fixpunktfreien Involution auf der Indexmenge der Doppelrandflächen, wobei bewiesen wird, dass gepaarte Terme algebraisch sich aufheben.

Hauptbeiträge
Die Arbeit liefert eine umfassende Formalisierung bestehend aus 44 Lean-Modulen (ca. 4.000 Zeilen) mit 205 benannten Deklarationen. Die spezifischen Beiträge umfassen:

Singuläres Stokes-Theorem: Ein Satz, der besagt, dass für jede global $C^\infty$ -Abbildung $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$ und jede $C^\infty$ - $n$ -Form $\omega$ das Integral von $\sigma^*(d\omega)$ über den Einheitswürfel gleich der alternierenden Summe der Integrale von $\sigma^*\omega$ über die $2(n+1)$ Flächen ist.
Brücken-Theorem: Ein formaler Beweis, der validiert, dass die koordinatenbasierte äußere Ableitung der Autoren (extDerivCoord) konsistent mit dem abstrakten extDeriv von mathlib4 ist, wenn sie auf Standardbasisvektoren ausgewertet wird. Dies stellt sicher, dass die koordinatenbasierte Implementierung mathematisch fundiert ist im Verhältnis zur abstrakten API der Bibliothek.
Erweiterungen auf Ketten-Ebene: Die Erweiterung des Stokes-Theorems auf formale $\mathbb{Z}$ -lineare Kombinationen von singulären Würfeln (singuläre Ketten) mittels Linearität.
$\partial^2 = 0$ -Beweis: Ein formaler Beweis der Kettenkomplex-Identität $\partial(\partial\sigma) = 0$ für singuläre Ketten unter Verwendung einer kombinatorischen Involution auf der Indexmenge der Doppelränder.
Dimensions-Spezialisierungen: Direkte Instanziierungen des Hauptsatzes, die den Fundamentalsatz der Analysis (FTC), den Satz von Green, den Divergenzsatz und den 3D-Gaußschen Satz sowie die partielle Integration und die Leibniz-Regel wiederherstellen.
Axiom-Prüfung: Verifizierung, dass die gesamte Entwicklung nur von den drei Standard-Lean-4-Axiomen (propext, Classical.choice, Quot.sound) abhängt, bestätigt durch 79 systematische #print axioms-Prüfungen.

Ergebnisse und Umfang
Die Formalisierung beweist das Stokes-Theorem erfolgreich für:

Glatte singuläre Würfel: Abbildungen $\sigma$ , die auf $\mathbb{R}^{n+1}$ global glatt sind, integriert über den Parameterwürfel $[0,1]^{n+1}$ .
Achsenparallele Boxen: Koordinaten- $n$ -Formen auf Boxen $[a,b] \subset \mathbb{R}^{n+1}$ .

Die Arbeit weist ausdrücklich folgende Einschränkungen und Umfangsgrenzen aus:

Keine Mannigfaltigkeitstheorie: Der Integrationsbereich ist strikt der Parameterwürfel oder eine Box. Die Arbeit formalisiert keine Integration über allgemeine glatte Mannigfaltigkeiten und verwendet weder Partitionen der Eins, Karten noch Atlanten.
Globale Glattheit: Die singulären Abbildungen müssen auf ganz $\mathbb{R}^{n+1}$ $C^\infty$ sein, eine stärkere Bedingung als Glattheit auf dem abgeschlossenen Würfel allein. Diese Wahl wurde getroffen, um die Formalisierung zu vereinfachen, indem Randregularitätsargumente vermieden werden und sichergestellt wird, dass die Fréchet-Ableitung überall wohldefiniert ist.
Keine Bildbereich-Semantik: Der Satz behandelt das Integral als Operation über dem Parameterraum. Er beweist nicht, dass das Bild von $\sigma$ eine Untermannigfaltigkeit oder eine orientierte geometrische Kette im Zielraum darstellt.

Bedeutung und Ansprüche
Die Autoren behaupten, dass diese Arbeit die erste vollständige Lean-4-Formalisierung des Stokes-Theorems für glatte singuläre Würfel mit einem „echten" Pullback von Differentialformen liefert. Ihre Bedeutung liegt in:

Überbrückung von Konkretem und Abstraktem: Das „Brücken-Theorem"-Muster validiert eine konkrete koordinatenbasierte Implementierung gegen den abstrakten äußeren Differentialoperator von mathlib4 und bietet eine wiederverwendbare Methodik für zukünftige Formalisierungen.
Wiederverwendung von Infrastruktur: Die Entwicklung stützt sich stark auf bestehende mathlib4-Infrastruktur (Divergenzsatz, extDeriv_pullback) und demonstriert, wie hochrangige Bibliothekskomponenten kombiniert werden können, um komplexe geometrische Sätze zu beweisen, ohne fundamentale Analysis neu zu erfinden.
Komplementarität: Die Arbeit ergänzt Harrisons HOL-Light-Formalisierung. Während Harrison konvexe/polyedrische Bereiche mit Gauß-Integration behandelt, deckt diese Arbeit glatte singuläre Parametrisierungen unter Verwendung der Bochner-Integration und der Differentialgeometrie-API von mathlib4 ab.
Grundlagen-Reife: Durch den Beweis von $\partial^2=0$ und die Etablierung des Stokes-Theorems auf Ketten-Ebene bieten die Autoren einen notwendigen lokalen Baustein für eine zukünftige vollständige Formalisierung des Stokes-Theorems auf glatten Mannigfaltigkeiten mit Rand, sobald die Mannigfaltigkeits-Integrations- und Orientierungs-APIs von mathlib4 ausgereift sind.

Die Arbeit schließt damit, dass sie zwar das Problem der Integration auf allgemeinen Mannigfaltigkeiten nicht löst, aber die kritische „würfelkettige" Schicht mit echten Pullbacks etabliert und als verifizierte Grundlage für zukünftige Erweiterungen dient.