teorth/analysis: ein Lean-Begleiter zu Analysis I

Eine Lean-Begleitung zu Analysis I

Dieses Repository enthält eine Formalisierung von Terence Taos Analysis I im Beweisassistenten Lean. Das README beschreibt sie als eine möglichst treue Paraphrase des Lehrbuchs, die dem Originaltext nahe bleiben und zugleich die Funktionen und die Syntax von Lean zeigen soll. Der Autor stellt ausdrücklich klar, dass die Formalisierung nicht auf Effizienz optimiert ist und in einigen Fällen vom idiomatischen Lean-Gebrauch abweichen kann. Textstellen, die im Buch als Übungen für die Leser belassen wurden, erscheinen in dieser Übersetzung als sorry. Der Autor beabsichtigt nicht, Lösungen direkt in das Repository aufzunehmen, sondern lädt Leser ein, das Projekt zu forken und die Übungen selbst zu versuchen. Das README erklärt außerdem, dass der Text nicht direkt zitiert, sondern an geeigneten Stellen auf das Original verwiesen wird, sodass die Formalisierung als kommentierte Begleitung zum Lehrbuch zu verstehen ist und nicht als Ersatz.

Der schrittweise Übergang zu Mathlib-Definitionen

Ein großer Teil des Materials aus Analysis I existiert bereits in Mathlib, der Standard-Mathematikbibliothek von Lean, allerdings mit leicht abweichenden Definitionen. Das README erläutert, wie die Formalisierung diese Unterschiede auflöst: Sie geht schrittweise von den Definitionen des Lehrbuchs zu den Definitionen von Mathlib über, je weiter man im Text fortschreitet. Kapitel 2 entwickelt zum Beispiel eine Theorie der natürlichen Zahlen unabhängig von Mathlib, während alle späteren Kapitel stattdessen die natürlichen Zahlen von Mathlib verwenden. Ein Epilog zu Kapitel 2 zeigt, dass die beiden Auffassungen isomorph sind. Dasselbe Muster wiederholt sich bei den reellen Zahlen: Ein Epilog zu Kapitel 5 beweist einen Isomorphismus mit den Mathlib-reellen Zahlen, und Kapitel 6 hat einen Epilog, der die dortigen Grenzwerte mit denen von Mathlib verbindet. Wegen dieses Aufbaus, so das README, kann die Formalisierung auch als Einführung in verschiedene Teile von Mathlib dienen.

Technische Änderungen gegenüber dem Lehrbuch

Eine kleine Anzahl von Definitionen weicht vom Buch ab, damit die Formalisierung mit den Mathlib-Konventionen übereinstimmt. Das README nennt drei davon. Sequenzen werden ab null statt ab eins indiziert, weil Mathlib die 0-basierten natürlichen Zahlen deutlich besser unterstützt. Operationen, die im Text undefiniert bleiben, etwa Division durch null oder die formale Limesbildung bei nicht-Cauchy-Folgen, erhalten stattdessen einen Junk-Wert wie 0, wodurch jede Operation total wird. Das README begründet dies damit, dass Lean totale Funktionen besser unterstützt als partielle, und verweist auf einen Blogbeitrag von Kevin Buzzard zur Division durch null in der Typentheorie. Schließlich werden die natürlichen Zahlen aus Kapitel 2 als induktiver Typ konstruiert statt auf rein axiomatischem Weg; die Peano-Axiome sind im Epilog dieses Kapitels formalisiert.

Abgedeckte Kapitel und Aufbau

Kapitel 1 des Buches ist nicht formalisiert. Alles von Kapitel 2 bis Kapitel 11 ist vorhanden, zusammen mit Anhang A über die Grundlagen der mathematischen Logik und Anhang B über das Dezimalsystem. Die Kapitelreihenfolge reicht von den natürlichen Zahlen, der Mengenlehre, den ganzen und rationalen Zahlen und den reellen Zahlen über Folgengrenzwerte, Reihen, unendliche Mengen, stetige Funktionen, Differentiation und das Riemann-Integral. Für jeden Abschnitt liefert das README drei Links: eine Verso-Seite mit der formalisierten Fassung, eine generierte HTML-Dokumentation und die jeweilige Lean-Quelldatei. Die Abschnittsnamen folgen der Struktur des Buches, von Abschnitt 2.1 über die Peano-Axiome bis Abschnitt 11.10 über Konsequenzen des Hauptsatzes der Differential- und Integralrechnung, sodass die Navigation im Repository der Reihenfolge des Lehrbuchs entspricht.

Weitere Lean-Inhalte im Repository

Neben der Formalisierung von Analysis I hostet das Repository mehrere unabhängige Lean-Projekte unter der Überschrift Additional content. Das README sagt, der Autor nutze das Repository, um einige andere kleinere Lean-Inhalte zu hosten, die nichts mit dem Lehrbuch zu tun haben. Eine Formalisierung des Buches des Autors über Maßtheorie ist vorhanden und als work in progress markiert. Es gibt Unterstützung für physikalische Einheitensysteme, einschließlich des SI-Systems, jeweils mit Anwendungsbeispielen. Das Repository enthält außerdem eine Formalisierung der endlichen Auswahl, die Lean's Auswahlaxiom vermeidet, einige endliche Wahrscheinlichkeitstheorie und vier Einträge zu Erdős-Problemen: eine Lösung zu Nummer 379, Pikhurkos Gegenbeispiel zu Nummer 613 sowie Lösungen zu den Nummern 707 und 987. Jedes dieser Extras hat im README eigene Dokumentations- und Quellverweise. Nur die Maßtheorie-Formalisierung ist ausdrücklich als unvollständig gekennzeichnet.

Build des Projekts und der Webseite

Das README dokumentiert zwei Build-Wege. Nach der Installation von Lean und dem Klonen des Repositorys baut ./build.sh das Projekt selbst. ./build-web.sh erstellt die Webseite des Projekts, wobei die Ausgabe in _site/ landet und anschließend mit python3 serve.py ausgeliefert werden kann. Das Aktualisieren der Lean- und Mathlib-Versionen ist ein manueller Vorgang: Die Datei lakefile.lean muss bearbeitet werden, um die require-Zeilen für Mathlib und doc-gen4 zu ändern, die Datei lean-toolchain muss angepasst werden, und lake update -R -Kenv=dev muss ausgeführt werden. Das README warnt, dass dies die Toolchain auf die neueste Lean-Version setzen kann, die dann zurückgesetzt werden muss, und merkt an, dass das Projekt eine veraltete Methode verwendet, um doc-gen4 bedingt anzufordern.

Lizenz und externe Ressourcen

Das Repository wird unter der Apache License 2.0 vertrieben. Der Lizenzauszug gewährt eine unbefristete, weltweite, nicht exklusive, gebührenfreie, lizenzgebührenfreie und unwiderrufliche Urheberrechtslizenz zum Vervielfältigen, Erstellen abgeleiteter Werke, öffentlichen Ausstellen, öffentlichen Aufführen, Unterlizenzieren und Verteilen des Werks. Er gewährt außerdem eine Patentlizenz für Patentansprüche, die durch Beiträge eines Contributors notwendigerweise verletzt werden; die Lizenz endet, wenn der Empfänger Patentstreitigkeiten anstrengt. Der Auszug enthält keine Aussagen zu Gewährleistung, Support oder Sicherheit, und auch das README macht dazu keine Angaben. Das README verweist außerdem auf die Projektwebseite, die Webseite des Buches und die Springer-Ausgabe, einen Blogbeitrag zur Ankündigung des Projekts, einen Lean-Zulip-Kanal, Hinweise für Mitwirkende und eine separate Lean-Formalisierung von Analysis II, die von einem anderen Team erstellt wurde.

Redaktionelles Fazit

Das README beschreibt das Repository als kommentierten Begleiter zu Analysis I und nicht als Ersatz, was die Kapitelliste bestätigt: Kapitel 2 bis 11 sowie Anhang A und B, während Kapitel 1 bewusst fehlt. Das Repository hostet außerdem lehrbuchfremde Lean-Arbeit, darunter Maßtheorie, Einheitensysteme und mehrere Einträge zu Erdős-Problemen, alles unter derselben Apache-2.0-Lizenz.

Offizielle Quellen

1. Official documentation
2. Official README
3. Project repository