🔢 mathematics

The continuous functional calculus in Lean

Dieses Paper dokumentiert die erste Formalisierung der kontinuierlichen Funktionalrechnung in einem beliebigen Beweisassistenten und beschreibt detailliert deren Implementierung in der Mathlib-Bibliothek von Lean, die zugrunde liegende mathematische Theorie sowie die entscheidenden Designentscheidungen, die die Nutzbarkeit für die mathematische Fachwelt gewährleisteten.

Ursprüngliche Autoren: Anatole Dedecker, Jireh Loreaux

Veröffentlicht 2026-06-08

📖 6 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Anatole Dedecker, Jireh Loreaux

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 vor, Sie sind ein Chefkoch, der in einer sehr komplexen, hochtechnologischen Küche arbeitet. Diese Küche repräsentiert die Welt der C-Algebren*, einen Zweig der Mathematik, der sich mit Operatoren (wie Maschinen, die Daten transformieren) beschäftigt, die unglaublich schwierig direkt zu verstehen sind.

Das Papier, das Sie lesen, ist ein Bericht von zwei Köchen, Anatole und Jireh, die gerade ein neues, revolutionäres Küchenwerkzeug namens Kontinuierliche Funktionalkalkül gebaut haben. Sie haben auch ein digitales Rezeptbuch (in einer Programmiersprache namens Lean) erstellt, das Computern beibringt, dieses Werkzeug perfekt zu benutzen.

Hier ist die Geschichte dessen, was sie getan haben, einfach erklärt.

1. Das Problem: Die „Black Box“-Maschine

In dieser mathematischen Küche hat man oft eine spezielle Maschine (ein Element $a$ ), die etwas Kompliziertes tut. Man möchte etwas Neues mit ihr machen, wie zum Beispiel ihre Quadratwurzel zu ziehen oder eine komplexe Kurve auf sie anzuwenden.

In den alten Tagen musste man dafür die Maschine auseinandernehmen, ihr Inneres (ihren „Spektrum“) verstehen und sie dann wieder zusammenbauen. Es war, als wollte man den Geschmack einer Suppe ändern, indem man den Topf zerlegt, die Chemie jedes einzelnen Moleküls analysiert und ihn dann wieder zusammensetzt. Das war langsam, fehleranfällig und erforderte einen PhD in Chemie, um eine einfache Änderung vorzunehmen.

2. Die Lösung: Das „Magische Etikett“

Das Kontinuierliche Funktionalkalkül ist ein magisches Etikett. Anstatt die Maschine auseinanderzunehmen, kleben Sie einfach ein Etikett darauf, das sagt: „Wende diese Funktion $f$ auf mich an.“

Der alte Weg: „Ich brauche die Quadratwurzel dieser Maschine. Ich muss zuerst beweisen, dass die Maschine normal ist, ihr internes Spektrum finden, beweisen, dass die Quadratwurzelfunktion auf diesem Spektrum stetig ist, und die Maschine dann rekonstruieren.“
Der neue Weg: „Ich habe eine Maschine $a$ . Ich möchte die Funktion $f(x) = \sqrt{x}$ anwenden. Ich schreibe einfach $f(a)$ .“

Das Papier erklärt, wie die Autoren eine digitale Version dieses „magischen Etikett“-Systems in Lean aufgebaut haben, einem Beweisassistenten, der mathematische Fehler prüft. Sie haben nicht nur die Mathematik geschrieben; sie haben die Schnittstelle so gestaltet, dass ein Mensch (oder ein Computer) dieses Werkzeug problemlos nutzen kann, ohne an technischen Details hängen zu bleiben.

3. Das Design: „Erst schreiben, dann denken“

Eine der größten Herausforderungen bei der Programmierung von Mathematik ist, dass Computer sehr streng sind. Wenn Sie einen Computer bitten, $1/0$ zu berechnen, stürzt er ab. Wenn Sie ihn bitten, eine Funktion auf eine Maschine anzuwenden, die nicht „normal“ ist, könnte er abstürzen.

Die Autoren entschieden sich für eine Strategie, die sie „Junk Values“ (Müllwerte) nennen.

Die Analogie: Stellen Sie sich einen Verkaufsautomaten vor. Wenn Sie eine Münze einwerfen und „Cola“ drücken, gibt er Ihnen eine Cola. Wenn Sie „Cola“ drücken, aber der Automat defekt ist, könnte ein normaler Verkaufsautomat explodieren oder eine Fehlermeldung ausgeben.
Der Lean-Ansatz: Die Autoren haben ihre Maschine so programmiert, dass sie, wenn Sie „Cola“ auf einer defekten Maschine drücken, einfach eine Dummy-Cola (einen „Junk Value“, wie 0) ausgibt. Er stürzt nicht ab. Er sagt einfach: „Hier ist eine Cola, aber sie ist nur ein Platzhalter.“
Warum das hilft: Dies ermöglicht es Mathematikern, lange, komplexe Rezepte (Gleichungen) aufzuschreiben, ohne bei jedem einzelnen Schritt prüfen zu müssen, ob dieser gerade gültig ist. Sie können zuerst das ganze Rezept schreiben und erst dann die Gültigkeit der spezifischen Schritte überprüfen, wenn sie das Endergebnis korrekt beweisen wollen. Dies macht die Arbeit viel schneller und weniger frustrierend.

4. Der „Universaladapter“ (Klassen)

Die Autoren erkannten, dass dieses „magische Etikett“-Werkzeug in verschiedenen Küchen funktionieren muss:

Komplexe Zahlen (die Standardküche).
Reelle Zahlen (eine einfachere Küche).
Nicht-negative Zahlen (eine Küche, in der man keine negativen Zutaten haben darf).

Anstatt drei separate, inkompatible Werkzeuge zu bauen, entwickelten sie einen Universaladapter (eine sogenannte „Class“ in Lean). Dieser Adapter weiß, wie er in jede dieser Küchen passt. Wenn Sie mit reellen Zahlen arbeiten, schaltet er automatisch in den Modus für reelle Zahlen. Wenn Sie mit Matrizen arbeiten, schaltet er in den Matrizen-Modus.

5. Die „Nicht-Einheitliche Herausforderung“ (Die Küche ohne Hauptschalter)

Die meisten mathematischen Werkzeuge setzen voraus, dass es einen „Hauptschalter“ (ein Einselement) in der Küche gibt. Aber einige mathematische Küchen (nicht-einheitliche Algebren) haben keinen solchen Schalter.

Die Analogie: Stellen Sie sich einen Lichtschalter vor, der den ganzen Raum steuert. In einer „einheitlichen“ Küche existiert dieser Schalter. In einer „nicht-einheitlichen“ Küche fehlt der Schalter.
Die Lösung: Die Autoren haben herausgefunden, wie sie ihr Werkzeug so bauen können, dass es auch funktioniert, wenn der Hauptschalter fehlt. Sie haben dies erreicht, indem sie so taten, als hätte die Küche kurzzeitig einen Schalter, führten die Arbeit aus und entfernten den Schalter dann wieder. Dies ermöglicht es dem Werkzeug, in jeder Küche zu funktionieren, unabhängig davon, ob ein Schalter vorhanden ist oder nicht.

6. Warum das wichtig ist

Bevor dieses Papier erschien, mussten Mathematiker, die dieses Werkzeug in einem Computerbeweis verwenden wollten, so viele Hürden nehmen (Stetigkeit beweisen, Normalität beweisen, verschiedene Zahlentypen handhaben), dass es oft einfacher war, die Mathematik einfach auf dem Papier zu machen und den Computer zu ignorieren.

Das Ziel der Autoren war es, die Computerschnittstelle so einfach wie das Schreiben auf Papier zu gestalten.

Vorher: Man musste für jeden einzelnen Schritt einen schweren Rucksack voller Beweis-Zertifikate mit sich herumtragen.
Nachher: Der Computer hat einen „intelligenten Assistenten“ (genannt autoParam), der diese Zertifikate automatisch für einen findet. Wenn Sie sqrt(a) schreiben, prüft der Computer automatisch, ob a ein gültiger Kandidat für eine Quadratwurzel ist. Wenn ja, großartig! Wenn nicht, sagt er es Ihnen.

Zusammenfassung

Das Papier dokumentiert die Konstruktion eines benutzerfreundlichen, universellen und robusten digitalen Werkzeugs zur Manipulation komplexer mathematischer Maschinen.

Sie ersetzten starre, absturzgefährdete Definitionen durch flexible Definitionen, die „Junk Values“ nutzen, um den Fluss aufrechtzuerhalten.
Sie bauten einen Universaladapter, um verschiedene Zahlentypen (Reell, Komplex, Nicht-negativ) zu handhaben.
Sie stellten sicher, dass es selbst in „kaputten“ Küchen (nicht-einheitlichen Algebren) funktioniert.
Sie fügten Automatisierung hinzu, damit Nutzer nicht jedes winzige Detail manuell beweisen müssen.

Das Ergebnis ist ein System, bei dem sich Mathematiker auf die Ideen (das Rezept) konzentrieren können, anstatt auf die Syntax (das Gemüse schneiden), was die Formalisierung der fortgeschrittenen Operatorentheorie erstmals in einem Beweisassistenten möglich macht.

Technische Zusammenfassung: Der kontinuierliche Funktionalcalculus in Lean

Problemstellung
Der kontinuierliche Funktionalcalculus ist ein fundamentales Werkzeug in der Theorie der $C^*$ -Algebren, das die Identifizierung kommutativer $C^*$ -Unteralgebren mit Algebren stetiger Funktionen auf kompakten Hausdorff-Räumen ermöglicht. Obwohl er mathematisch gut verstanden ist, stellt seine Formalisierung in Beweisassistenten wie Lean erhebliche Herausforderungen dar. Die primäre Schwierigkeit liegt darin, ein Gleichgewicht zwischen mathematischer Treue und Anwendbarkeit (Usability) zu finden. Eine „natürliche“ mathematische Definition beruht oft auf abhängigen Typen (z. B. Funktionen, die nur auf dem Spektrum eines Elements definiert sind) und gebündelten Strukturen (z. B. stetige Abbildungen als ein spezifischer Typ). Während diese rigoros sind, erzeugen sie Reibungsverluste bei formalen Beweisen: Das Umschreiben von Gleichheiten wird schwierig, da die Typen von spezifischen Elementen abhängen, und das Komponieren von Funktionen erfordert das Management komplexer Subtyp-Kohäsionen und Stetigkeitsbeweise. Die Autoren stellten fest, dass ein Design, das eine strikte mathematische Einfachheit priorisiert, oft die „Litmus-Tests“ der praktischen Anwendbarkeit, die für eine Bibliothek wie Mathlib erforderlich sind, nicht besteht.

Methodik und Designentscheidungen
Die Autoren entwickelten eine Formalisierung des kontinuierlichen Funktionalcalculus in Lean 4, die in die Mathlib-Bibliothek integriert wurde. Ihre Methodik beinhaltete einen iterativen Designprozess, der von einer mathematisch „reinen“ Definition zu einer „utilitären“ Schnittstelle führte. Zentrale Designentscheidungen waren:

Unbundling und „Junk-Werte“ (Junk Values):
Anstatt den Funktionalcalculus als eine Abbildung vom Typ der stetigen Funktionen auf dem Spektrum $C(\sigma(a), \mathbb{C})$ zur Algebra zu definieren, definierten die Autoren eine Funktion cfc, die jede Funktion $f: \mathbb{C} \to \mathbb{C}$ und jedes Element $a$ akzeptiert. Wenn $a$ nicht normal oder $f$ nicht stetig auf dem Spektrum ist, gibt die Funktion einen „Junk-Wert“ zurück (typischerweise 0).
- Begründung: Dies ermöglicht es Benutzern, Ausdrücke wie $f(a)$ zu schreiben, ohne zuerst beweisen zu müssen, dass $a$ normal oder $f$ stetig ist. Dies ahmt den „Erst schreiben, dann denken“-Ansatz der informellen Mathematik nach, indem die Beweislast auf einen späteren Zeitpunkt verschiebt, wenn eine nicht-triviale Eigenschaft benötigt wird. Dies ermöglicht auch ein nahtloses Umschreiben (rw), da die Typen der Argumente nicht mehr von den spezifischen Eigenschaften von $a$ abhängen.
Klassenbasierte Abstraktion:
Um verschiedene Skalarringe ( $\mathbb{C}$ , $\mathbb{R}$ und $\mathbb{R}_{\ge 0}$ ) und unterschiedliche Elementtypen (normal, selbstadjunkt, nicht-negativ) zu handhaben, implementierten die Autoren den Calculus als Typklasse ContinuousFunctionalCalculus.
- Prädikat-Generalisierung: Die Klasse ist durch ein Prädikat $p$ auf den Algebra-Elementen parametrisiert (z. B. IsStarNormal, IsSelfAdjoint, 0 ≤ a). Dies ermöglicht es einer einzigen Schnittstelle, verschiedene Fälle ohne Code-Duplikation abzudecken.
- Prop-Werte vs. Daten: Frühere Versionen enthielten den $*$ -Homomorphismus als Daten. Um jedoch Probleme mit der definitorischen Gleichheit (wo zwei verschiedene Konstruktionen derselben Abbildung nicht definitorisch gleich sein könnten) zu vermeiden, macht das endgültige Design die Klasse zu einem Prop. Sie behauptet die Existenz eines eindeutigen $*$ -Homomorphismus mit spezifischen Eigenschaften, anstatt die Abbildung selbst zu speichern.
Handhabung nicht-unitärer Algebren:
Die Formalisierung erstreckt sich auf nicht-unitäre $C^*$ -Algebren. Anstatt sich für jede Definition auf extrinsische Konstruktionen wie die minimale Unitarisierung zu verlassen, führten die Autoren eine intrinsische Definition des Quasispektrums ein. Der nicht-unitäre Funktionalcalculus wird auf Funktionen definiert, die bei 0 verschwinden (oder 0 auf 0 abbilden), wodurch der ständige Wechsel zwischen unitären und nicht-unitären Kontexten vermieden wird.
Automatisierung via autoParam:
Um die Verbosität der manuellen Übergabe von Stetigkeits- und Normalitätsbeweisen zu mildern, nutzten die Autoren das autoParam-Feature von Lean. Hypothesen wie „ $f$ ist stetig auf dem Spektrum“ sind mit Standard-Taktiken ausgestattet. Wenn der Benutzer keinen Beweis liefert, versucht Lean, diesen automatisch unter Verwendung existierender Lemmata (z. B. aesop, fun_prop) zu synthetisieren.
Eindeutigkeit als separate Klasse:
Die Kompositionseigenschaft ( $g(f(a)) = (g \circ f)(a)$ ) ist zentral für die Theorie. Die Autoren bewiesen dies mittels eines Eindeutigkeitsarguments anstatt des Satzes von Stone-Weierstrass (der für $\mathbb{R}_{\ge 0}$ fehlschlägt). Sie kapselten die Eindeutigkeit von $*$ -Homomorphismen in einer separaten Klasse ContinuousMap.UniqueHom, wodurch die Kompositionseigenschaft generisch über verschiedene Skalarringe hinweg abgeleitet werden konnte.

Wesentliche Beiträge und Ergebnisse

Erste Formalisierung: Diese Arbeit stellt die erste Formalisierung des kontinuierlichen Funktionalcalculus in einem beliebigen Beweisassistenten dar.
Mathlib-Integration: Die Implementierung wurde in Mathlib zusammengeführt und bietet eine einheitliche Schnittstelle für komplexe, reelle und nicht-negative reelle Funktionalcalculi.
Verifizierung der Anwendbarkeit: Das Design wurde gegen spezifische „Litmus-Tests“ validiert, darunter:
- Definition von Inversen ( $f(a^{-1})$ ) unter Verwendung von Funktionen, die nicht überall stetig sind (z. B. $x \mapsto x^{-1}$ ).
- Konstruktion von positiven/negativen Teilen und Quadratwurzeln für selbstadjungte und nicht-negative Elemente.
- Anwendung des Calculus auf Matrizen über $\mathbb{R}$ (die in Mathlib keine globale metrische Struktur besitzen).
Automatisierung: Die Schnittstelle unterstützt High-Level-Automatisierung, was es Benutzern ermöglicht, Eigenschaften wie $f(-a) = (x \mapsto f(-x))(a)$ mit minimalem manuellem Aufwand zu beweisen.
Anwendungen: Die Schnittstelle wurde bereits zur Formalisierung fortgeschrittener Resultate verwendet, darunter:
- Die Existenz von approximativen Einheiten in nicht-unitären $C^*$ -Algebren.
- Die Stetigkeit des Funktionalcalculus in beiden Variablen.
- Eigenschaften von Abbildungen $a \mapsto |a|$ , $a \mapsto a^p$ und $a \mapsto \log(a)$ .
- Ergebnisse bezüglich unitärer Elemente und Projektionen.

Bedeutung und Limitationen
Das Paper beansprucht seine Bedeutung primär durch seine Designphilosophie: Es zeigt auf, dass für ein Werkzeug, das in einer groß angelegten formalen Bibliothek effektiv sein soll, die Ergonomie für den Endbenutzer (Usability) Vorrang vor der strikten mathematischen Reinheit in der Definition haben muss. Durch die Akzeptanz von „Junk-Werten“ und das Unbundling von Typen schufen die Autoren eine Schnittstelle, die für Mathematiker intuitiv funktioniert und komplexe Manipulationen (wie Komposition und Umschreiben) ermöglicht, die mit einem strikt abhängigen Typ-Ansatz prohibitiv schwierig wären.

Die Autoren äußern sich bescheiden über den aktuellen Stand und räumen auch einige Limitationen ein:

Simp-Lemmata: Aufgrund der Notwendigkeit expliziter Argumente, um autoParam zu triggern, können viele Lemmata nicht ohne manuelles Eingreifen als simp-Regeln verwendet werden, was einige Beweise unerwünscht wortreich macht.
Komplikationen bei $\mathbb{R}_{\ge 0}$ : Die Verwendung der nicht-negativen reellen Zahlen als Skalarring führt spezifische technische Hürden ein (z. B. trunkierte Subtraktion, mangelnde Ringstruktur), die separate Theorem-Aussagen erfordern.
Reelle $C^*$ -Algebren: Obwohl das Framework darauf ausgelegt ist, reelle $C^*$ -Algebren zu unterstützen, ist der spezifische Fall des Funktionalcalculus über $\mathbb{C}$ für reelle Algebren (der einen anderen Funktionsbereich erfordert) noch nicht vollständig integriert und ist für zukünftige Arbeiten geplant.

Zusammenfassend dokumentiert das Paper eine erfolgreiche Übersetzung einer tiefen Operatorenalgebra-Theorie in ein anwendbares formales System und hebt die Abwägung zwischen mathematischer Eleganz und praktischem Nutzen im Kontext des interaktiven Theorembeweisens hervor.