💻 computer science

ZFLean: a framework for set-level mathematics in Lean

Das Papier stellt ZFLean vor, eine Lean-4-Bibliothek, die die Kern-ZFC-Mengenlehre in das Mathlib-Ökosystem integriert und dabei verbesserte Ergonomie, kanonische Konstruktionen sowie Brücken zu nativen Typen bietet, um gemischte Beweise auf Mengen- und Typenebene zu erleichtern.

Ursprüngliche Autoren: Vincent Trélat

Veröffentlicht 2026-04-28

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Vincent Trélat

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 versuchen, ein Haus zu bauen. Sie haben zwei verschiedene Sätze von Bauplänen und Werkzeugen:

Die „typisierten" Werkzeuge (Leans natives System): Diese sind wie hochtechnologische, lasergeführte Roboterarme. Sie sind unglaublich präzise, funktionieren aber nur, wenn jeder Ziegel perfekt mit seinem spezifischen Typ gekennzeichnet ist (z. B. „Roter Ziegel", „Blauer Ziegel"). Wenn Sie versuchen, einen „Roten Ziegel" dort zu verwenden, wo ein „Blauer Ziegel" erforderlich ist, stoppt der Roboter und weigert sich zu arbeiten. Das ist großartig für die Sicherheit, aber manchmal fühlt sich die Mathematik so an, als müsste sie flexibler sein.
Die „Mengen"-Werkzeuge (ZFC): Diese sind wie ein riesiger, unordentlicher Haufen rohen Tons. In dieser Welt ist alles einfach nur „Sache". Sie können ein Stück Ton zu einer Tasse, einem Ball oder einem Quadrat formen, und es ist alles nur „Ton". So denken traditionelle Mathematiker oft über Mengen: Alles ist ein Element einer Sammlung, und man kann frei mischen und kombinieren.

Das Problem:
Lange Zeit war es ein Albtraum, wenn man Mathematik mit den „Mengen"-Werkzeugen innerhalb der „typisierten" Roboterwerkstatt betreiben wollte. Man musste ständig seine Tonformen in roboterfreundliche Etiketten übersetzen, beweisen, dass die Übersetzung korrekt war, und die Ergebnisse dann zurückübersetzen. Es war langsam, langweilig und fehleranfällig. Die meisten Menschen mieden den Tonhaufen ganz einfach und blieben bei den Robotern.

Die Lösung: ZFLean
Vincent Trélat hat ZFLean geschaffen, was wie der Bau eines universellen Übersetzers und eines Satzes benutzerdefinierter Werkzeuge direkt innerhalb der Roboterwerkstatt ist.

So funktioniert es, unter Verwendung einfacher Analogien:

1. Die „Ton"-Werkstatt (Das ZFC-Modell)

ZFLean richtet eine spezielle Zone innerhalb der Roboterwerkstatt ein, in der die „Ton"-Regeln gelten. Hier können Sie Mengen, Relationen und Funktionen definieren, genau wie ein traditioneller Mathematiker, ohne sich um die strengen „Typen" sorgen zu müssen, die der Roboter normalerweise verlangt. Es ist ein sicherer Raum, in dem Sie sagen können: „Das ist eine Menge von Zahlen", ohne dass der Roboter fragt: „Ist es ein Nat oder ein Int?"

2. Der „smarte Übersetzer" (Der relationale Kalkül)

Das größte Ärgernis in den alten Tagen war der „Standardaufwand" – die wiederholende, langweilige Bürokratie, die erforderlich war, um zu beweisen, dass Ihre Tonformen tatsächlich gültig waren.

Der alte Weg: Sie mussten manuell beweisen: „Ja, diese Relation ist eine Funktion" und „Ja, diese Domäne ist gültig", für jeden einzelnen Schritt.
Der ZFLean-Weg: Das Framework kommt mit kleinen smarten Assistenten (genannt Taktiken wie zrel, zpfun und zfun). Denken Sie an diese wie an automatische Ausfüllformulare. Wenn Sie einen Beweis schreiben, prüfen diese Assistenten automatisch die langweiligen Details und füllen die Bürokratie für Sie aus. Sie schreiben die Mathematik; die Assistenten übernehmen die administrative Last.

3. Die „Brücke" (Interoperabilität)

Dies ist der magische Teil. Normalerweise waren die „Ton"-Welt und die „Roboter"-Welt getrennt. ZFLean baut Brücken zwischen ihnen.

Wenn Sie eine Menge natürlicher Zahlen in der Tonwelt bauen, kann ZFLean sofort sagen: „Hey, das ist tatsächlich dasselbe wie der Roboter-Typ Nat."
Das bedeutet, Sie können Ihre chaotische, flexible mengentheoretische Mathematik betreiben und dann nahtlos die Brücke überqueren, um die leistungsstarken, vorgefertigten Werkzeuge des Roboters (wie Algebra-Löser) zu nutzen, um die Arbeit zu beenden. Sie müssen sich nicht für das eine oder das andere entscheiden; Sie können beides im selben Beweis verwenden.

4. Das „Lego-Set" (Kanonsche Konstruktionen)

Um das Leben zu erleichtern, kommt ZFLean mit einem vorgefertigten Set aus Standard-Lego-Steinen.

Benötigen Sie eine Menge von Wahr/Falsch-Werten? Hier ist eine Boolesche Menge.
Benötigen Sie eine Menge von Zählzahlen? Hier ist eine natürliche Zahlen-Menge.
Benötigen Sie eine Möglichkeit, „vielleicht"-Werte zu behandeln (wie eine Option)? Hier ist eine Option-Menge.
Dies sind nicht nur roher Ton; sie sind vorgeformt, getestet und kommen mit Anweisungen zur Verwendung (wie „wie man zwei Zahlen addiert" oder „wie man einen Schalter umlegt").

5. Die „Probefahrt" (Die Fallstudie)

Um zu beweisen, dass dieses System funktioniert, testete der Autor es mit einem klassischen mathematischen Rätsel namens Currying-Isomorphismus.

Stellen Sie sich vor: Sie haben eine Maschine, die zwei Eingaben gleichzeitig nimmt (wie ein Sandwichmacher, der Brot und Fleisch nimmt). „Currying" ist der Prozess, diese in eine Maschine umzuwandeln, die eine Eingabe (Brot) nimmt und dann Ihnen eine neue Maschine gibt, die die zweite Eingabe (Fleisch) nimmt.
Der Autor verwendete ZFLean, um zu beweisen, dass diese beiden Denkweisen über die Maschine tatsächlich dasselbe sind. Das Beweisskript sah fast exakt so aus, als würde ein menschlicher Mathematiker es an einer Tafel schreiben, wobei die „smarten Assistenten" im Hintergrund alle technischen Störungen ruhig handhabten.

Das Fazit

ZFLean ist ein Framework, das Mathematikern erlaubt, im flexiblen, intuitiven Stil der traditionellen Mengenlehre (dem „Ton") zu arbeiten, während sie in einem modernen, rigorosen Computerbeweissystem (den „Robotern") leben. Es beseitigt die Reibung der Übersetzung, automatisiert die langweilige Bürokratie und baut Brücken, damit Sie die besten Werkzeuge aus beiden Welten nutzen können, ohne in der Mitte stecken zu bleiben.

Das Ergebnis ist eine Bibliothek von etwa 8.300 Zeilen Code, die das „Mengen-Ebenen"-Mathematisieren in Lean so natürlich und flüssig macht wie das Schreiben auf Papier.

1. Problemstellung

Die moderne Formalisierung in Beweisassistenten wie Lean basiert überwiegend auf der Typentheorie (insbesondere abhängiger Typentheorie), in der mathematische Objekte als konstruierte Typen definiert werden. Obwohl dieser Ansatz leistungsstark ist, kann er für mathematische Arbeiten auf Mengen-Ebene (ZFC) umständlich sein, die oft aus folgenden Gründen bevorzugt werden:

Extensionales Schließen: Schließen über Gleichheit basierend auf Elementen statt auf Konstruktion.
Partialität: Natürliche Handhabung partieller Funktionen über Relationen statt deren Kodierung mit Option-Typen oder abhängigen Typen.
Kategorienartiges Schließen: Arbeiten „bis auf Isomorphie" statt strikter definitorischer Gleichheit.

Die Herausforderung: Die direkte Arbeit in einem mengentheoretischen Modell innerhalb eines getypten Assistenten (wie dem ZFC-Modell in Lean's Mathlib) führt zu erheblichen Reibungsverlusten:

Boilerplate: Benutzer müssen ständig „Nebenbedingungen" (z. B. Nachweis, dass eine Relation wohldefiniert ist, Nachweis, dass eine Funktion total ist) manuell verwalten.
Brüchigkeit: Der Übergang zwischen mengentheoretischen Objekten (ZFSet) und nativen Lean-Typen (Type) ist manuell und fehleranfällig.
Fehlende Automatisierung: Bestehende Werkzeuge verfügen oft nicht über die spezifischen Umformungsregeln und Taktiken, die erforderlich sind, um mengentheoretische Beweise so flüssig zu gestalten wie getypte Beweise.

2. Methodik

Der Autor stellt ZFLean vor, eine Lean 4-Bibliothek, die auf dem bestehenden ZFC-Modell von Mathlib aufbaut. Die Methodik konzentriert sich auf die Schaffung eines uniformen relationalen Kalküls und Interoperabilitätsbrücken, um die Entwicklung auf Mengen-Ebene ergonomisch zu gestalten.

Kern-Design-Entscheidungen:

Fundament: Nutzt die Implementierung von ZFC in Mathlib, die Mengen als den extensionalen Quotienten induktiver „Vormengen" (PSet) konstruiert.
Relationaler Kalkül: Anstatt Funktionen als erstklassige totale Objekte zu behandeln (wie in der Standard-Typentheorie), betrachtet ZFLean sie als funktionale Relationen. Es wird ein Kalkül für binäre Relationen, partielle Funktionen und totale Funktionen eingeführt.
Automatisierung durch Taktiken: Das Framework führt drei leichte Taktiken ein (zrel, zpfun, zfun), die darauf ausgelegt sind, Wohlformtheits-Nebenbedingungen automatisch zu erledigen (z. B. Nachweis, dass eine Komposition eine Relation oder eine Funktion ist).
Brücken: Die Bibliothek konstruiert explizite Isomorphismen (Brücken) zwischen kanonischen ZFC-Objekten (z. B. ZFBool, ZFNat) und nativen Lean-Typen (Bool, Nat), wodurch Eigenschaften zwischen beiden Welten transportiert werden können.

3. Hauptbeiträge

A. Relationaler Kalkül und Automatisierung

Definitionen: Formalisierung von Konverse, Identität, Komposition, Definitionsbereich, Wertebereich und Bild für Relationen.
Funktionalität: Unterscheidung zwischen partiellen Funktionen (IsPFunc) und totalen Funktionen (IsFunc).
Taktiken:
- zrel: Erledigt Ziele, die beweisen, dass eine Menge eine Relation ist ( $R \subseteq A \times B$ ).
- zpfun: Erledigt Ziele, die beweisen, dass eine Menge eine partielle Funktion ist.
- zfun: Erledigt Ziele, die beweisen, dass eine Menge eine totale Funktion ist.
- Diese Taktiken nutzen attribut-markierte Lemmata (z. B. @[zfun]), um Nebenbedingungen rekursiv zu lösen und Boilerplate vom Benutzer zu verbergen.
Notation: Einführung einer praktischen Syntax für Funktionsanwendung (@zf(x)) und $\lambda$ -Abstraktion, mit Theoremen für $\beta$ -Reduktion, $\eta$ -Expansion und Extensionalität.

B. Kanonische Konstruktionen

Die Bibliothek bietet eine Suite standardmäßiger mathematischer Objekte, die innerhalb von ZFC definiert sind, vollständig mit ihren universellen Eigenschaften:

Boolesche Werte: Eine zweielementige Menge $B$ mit algebraischer Struktur (Konjunktion, Disjunktion, Negation) und einem Fall-Entscheidungsbeseitiger.
Natürliche Zahlen ( $\mathbb{N}$ ): Definiert als die kleinste induktive Menge (von-Neumann-Ordinalzahlen). Enthält einen Rekursor, ein Induktionsprinzip und arithmetische Operationen. Entscheidend ist, dass sie mit einer CommSemiring-Struktur ausgestattet ist, um Lean's ring-Taktik nutzen zu können.
Ganze Zahlen ( $\mathbb{Z}$ ) und Rationale Zahlen ( $\mathbb{Q}$ ): Konstruiert als Quotiententypen von Paaren natürlicher/ganzer Zahlen, wobei Operationen von Repräsentanten gehoben werden.
Koprodukte und Optionen: Mengentheoretische Definitionen von Summentypen und Optionstypen.

C. Isomorphismen und Transport

Einbettungen und Isomorphismen: Definition mengentheoretischer Einbettungen ( $A \hookrightarrow_z B$ ) und Isomorphismen ( $A \cong_z B$ ) über injektive und bijektive Funktionen.
Cantor-Schröder-Bernstein-Theorem: Innerhalb des Frameworks formalisiert.
Transport: Beweis, dass ZFC-Konstruktionen isomorph zu nativen Lean-Typen sind (z. B. ZFBool $\simeq$ Bool). Dies ermöglicht Benutzern, Theoreme nahtlos von der reichhaltigen typentheoretischen Bibliothek Mathlib in den mengentheoretischen Kontext zu „transportieren".

D. Fallstudie: Currying-Isomorphismus

Das Papier demonstriert die Nützlichkeit des Frameworks durch den Beweis des Currying-Isomorphismus: $C^{A \times B} \cong (C^B)^A$ .

Der Beweis definiert curryz und uncurryz als Funktionen auf Mengen-Ebene.
Es wird bewiesen, dass sie gegenseitige Inverse sind, wobei die Automatisierung des Frameworks genutzt wird, um Nebenbedingungen zu behandeln (Wohldefiniertheit von Kompositionen und Bildern).
Das Beweisskript spiegelt eng standardmäßige mathematische Argumente wider, wobei die Automatisierungsschicht die „langweilige" mengentheoretische Verifikation übernimmt.

4. Ergebnisse

Artefakt-Größe: Die Bibliothek besteht aus 8.324 Zeilen Lean-Code und 706 bewiesenen Theoremen.
Komponentenaufschlüsselung:
- Relationaler Kalkül: ~2.534 Zeilen Code (172 Theoreme).
- Natürliche Zahlen: ~1.260 Zeilen Code (199 Theoreme).
- Einbettungen/Isomorphismen: ~1.626 Zeilen Code (31 Theoreme).
Benutzerfreundlichkeit: Die Fallstudie zeigt, dass das Framework den Reibungsverlust der Formalisierung auf Mengen-Ebene erfolgreich reduziert. Benutzer können Beweise schreiben, die wie standardmäßige mengentheoretische Argumente aussehen, ohne manuell nachweisen zu müssen, dass jede Komposition von Relationen eine gültige Relation ist.
Interoperabilität: Die Fähigkeit, zwischen ZFSet und nativem Type zu wechseln, ermöglicht die Wiederverwendung der algebraischen Taktiken von Mathlib (wie ring) auf mengentheoretischen Objekten.

5. Bedeutung

Überbrückung von Fundamenten: ZFLean versöhnt effektiv die „mengentheoretische" und die „typentheoretische" Sichtweise der Mathematik innerhalb eines einzigen Beweisassistenten. Es ermöglicht Mathematikern, die für ein spezifisches Problem natürlichste Fundamentierung zu wählen (extensionale Mengen vs. konstruktive Typen), ohne den Zugriff auf die Automatisierung des Ökosystems zu verlieren.
Ergonomie: Durch die Automatisierung der mühsamen Nebenbedingungen, die der Mengenlehre inhärent sind (Nachweise der Mitgliedschaft, Wohldefiniertheit von Relationen), macht es die ZFC-Entwicklung in Lean für Nicht-Experten machbar und für groß angelegte Formalisierungen praktikabel.
Erweiterbarkeit: Das modulare Design (relationaler Kalkül + kanonische Objekte + Brücken) ermöglicht eine einfache Erweiterung. Zukünftige Arbeiten umfassen die Formalisierung der reellen Zahlen (via Cauchy-Folgen oder Dedekind-Schnitte) und der elementaren Analysis.
Vergleich: Im Gegensatz zu Isabelle/ZF (wo Mengenlehre eine separate Objektlogik ist) oder den mengentheoretischen Entwicklungen in Rocq (die oft eine tiefe Integration mit typentheoretischer Automatisierung vermissen lassen), bietet ZFLean einen hybriden Ansatz, der Beweise auf Mengen-Ebene hält, während die native typentheoretische Infrastruktur von Lean genutzt wird.

Zusammenfassend bietet ZFLean ein robustes, ergonomisches und interoperables Framework für die Durchführung grundlegender Mathematik in ZFC innerhalb von Lean 4, das erfolgreich die Einstiegshürde für mengentheoretische Formalisierung senkt und gleichzeitig die Kompatibilität mit dem breiteren Mathlib-Ökosystem wahrt.