Ein Lean-Companion zu Analysis I

 (terrytao.wordpress.com)
2 Punkte von GN⁺ 2025-06-01 | 1 Kommentare | Auf WhatsApp teilen
  • Ein Projekt, das die Kernaussagen von Analysis I, dem Lehrbuch zur reellen Analysis von Terence Tao, in den Lean-Beweisassistenten überträgt
  • Das Projekt passt strukturell gut zum Anspruch des Originals auf Strenge, etwa bei der Konstruktion grundlegender Zahlensysteme und der Beweislogik
  • Es nutzt die Standardbibliothek Mathlib, enthält aber auch Übungen zum eigenen Aufbau zentraler Konzepte und zum eigenständigen Beweisen
  • Man kann üben, indem man Lücken (sorry) im Lean-Code selbst füllt; offizielle Lösungen gibt es nicht, Erweiterungen per Fork sind möglich
  • Für Lean-Einsteiger und Lernende der reellen Analysis gleichermaßen nützlich, um den praktischen Einsatz von Mathlib und Lean kennenzulernen

Überblick

  • Ein Open-Source-Projekt, das das Lehrbuch zur reellen Analysis "Analysis I" von Terence Tao mit dem Lean-Beweisassistenten neu aufbereitet
  • Das Lehrbuch legt im Vergleich zu anderen Analysis-Büchern mehr Gewicht auf den Konstruktionsprozess der natürlichen Zahlen, ganzen Zahlen, rationalen Zahlen und reellen Zahlen sowie auf die dafür nötigen mengentheoretischen und logischen Werkzeuge
  • Viele Teile des Buchs zielen auf den systematischen Aufbau der Fähigkeit zu strengen Beweisen, weshalb es sich strukturell gut für einen Beweisassistenten wie Lean eignet

Merkmale des Lean-Companion-Projekts

  • Es stellt die Definitionen, Sätze und Übungsaufgaben des Originals in Lean-Form "übersetzt" bereit
  • Diese Lean-Dateien enthalten viele Lücken (sorry), die den Lösungen zu den Übungsaufgaben entsprechen und vom Leser selbst ausgefüllt werden können
  • Offizielle Erklärungen oder Lösungen werden nicht bereitgestellt, aber Leser können das Repository forken und ihre eigene Lösungsvariante erstellen

Verbindung zu Mathlib und Unterschiede

  • Einige bereits in Mathlib (Leans Standardbibliothek für Mathematik) implementierte Konzepte, etwa natürliche Zahlen, werden absichtlich noch einmal eigenständig aufgebaut; danach ist auch der Nachweis der Isomorphie (Äquivalenz) zur Mathlib-Version Teil des Projekts
  • Beispielsweise werden in Chapter2.Nat eigene natürliche Zahlen aufgebaut, die von den natürlichen Zahlen aus Mathlib getrennt sind; nach der eigenständigen Behandlung zentraler Resultate übt man am Ende in Lean, dass beide Versionen gleichwertig sind
  • Ab den folgenden Kapiteln wird dann schrittweise immer stärker auf Definitionen und Funktionen aus Mathlib zurückgegriffen

Lernen und Nutzung

  • Dieser Lean-Companion dient nicht nur dem Analysis-Studium, sondern auch als Einführung in die Formalisierung von Mathematik mit Lean und Mathlib
  • Ähnlich wie beim "Natural number game" enthält er strukturierte Übungen, in denen mathematische Objekte in einer Lean-Umgebung direkt definiert und erprobt werden
  • Der Code selbst lässt sich in Lean kompilieren, aber es wurde nicht vollständig verifiziert, ob sich alle Übungsaufgaben (sorry) tatsächlich lösen lassen; insofern sind Playtesting und Feedback erwünscht

Open Source und Beiträge

  • Das Repository ist Open Source und kann von allen eingesehen, geforkt und weiterentwickelt werden
  • Offizielle Lösungen werden nicht separat bereitgestellt, wodurch mehrere Lösungsvarianten unterstützt werden
  • Stand 31. Mai wurde das Projekt in ein eigenständiges, separates Repository überführt

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2025-06-01
Hacker-News-Kommentare

  • Ich bin wirklich gespannt; wenn dieses Projekt in ein eigenständiges Repo ausgelagert wird, lässt es sich viel leichter mit anderen teilen und besser finden. Ich war schon immer neugierig auf Mathematik, und Taos Analysis war das erste Lehrbuch, das mir gezeigt hat, wie streng Mathematik aufgebaut ist, und zwar auf eine Weise, die zu meiner Denkweise als Programmierer passt. Später habe ich mich auch für Lean begeistert, fand Mathlib aber etwas zu komplex, um damit mathematische Konzepte zu lernen. Deshalb gefällt mir dieses Projekt sehr, weil es als Brücke vom Buch zum Tool dient.

    • Ich hatte eine ähnliche Erfahrung. Ich habe Konvergenz, Cauchy-Folgen usw. daraus gelernt, und ich erinnere mich noch daran, dass dieses Buch vom indischen Non-Profit-Verlag Hindustan Book Agency veröffentlicht wurde und deshalb sehr günstig zu bekommen war.

  • Der spannendste Aspekt von Mathematikunterricht mit Lean ist für mich das unmittelbare Feedback: Wenn ein Student einen Beweis falsch macht, kompiliert er nicht. Früher musste das Feedback direkt von einem TA oder Professor kommen, jetzt meldet sich der Lean-Compiler schnell. Ich hoffe, dass es künftig wie beim Rust-Compiler sogar freundlichere Korrekturvorschläge geben wird (dafür könnte ein dediziertes LLM nötig sein).

    • Dem stimme ich fast vollständig zu, aber ich halte auch den Prozess des Nachdenkens über einen Beweis für wichtig. Meine Mathematikerfahrung liegt schon lange zurück, aber ich hatte viele dieser „Mathe-Paradies“-Zeiten, in denen man Aufgaben oder Probleme auf Papier niederschreibt und langsam darüber nachdenkt. Mit Lean könnte es stattdessen in eine eher mechanische Richtung gehen, bei der man einfach zufällige Eingaben ausprobiert oder so lange herumprobiert, bis es automatisch passt. Ich habe früher kurz Coq benutzt und erinnere mich daran, dass ich fast nur herumprobiert habe. Insgesamt sind Theorem Prover in vieler Hinsicht nützlich, aber ich frage mich, ob dadurch dieser langsame Prozess des Verinnerlichens, Konzeptualisierens und des Entstehens neuer Ideen schwächer werden könnte. Mich würde interessieren, was andere dazu denken.

  • Es gibt offenbar einen persönlichen YouTube-Kanal, auf dem man Terence Tao selbst bei der Arbeit mit Lean sehen kann. Ich bin auf diesem Gebiet kein Experte, aber allein zuzuschauen, wie er mit oder ohne LLM arbeitet, fand ich wirklich interessant (https://www.youtube.com/@TerenceTao27).

  • Es wäre wirklich interessant, den traditionellen „Lehrbuchansatz“ mit dem Mathlib-Ansatz zu vergleichen und zu bewerten. Formalisierte Mathematikbibliotheken drücken Ergebnisse im Allgemeinen so allgemein wie möglich aus, und ein Vorteil ist, dass sich die Beweisstruktur selbst leicht elegant refaktorisieren lässt. Das Refactoring ist einfach, weil das System die logischen Abhängigkeiten stets verfolgt, was mit Papier und Stift nicht leicht ist. Deshalb ist es aus meiner Sicht eine naheliegende Frage, ob man die „maximal allgemeine“ Version der Analysis, wie sie in Mathlib auftaucht, in Universitätsvorlesungen lehren sollte. Dasselbe gilt auch für alle anderen beweisbasierten Bereiche der Mathematik.

    • Zumindest für Einführungskurse halte ich das nicht für geeignet. Im Curriculum ist ohnehin schon viel zu viel unterzubringen — Beweismethoden, Programmierung und die grundlegende Theorie. Die Erfahrungen von Professoren, die es tatsächlich versucht haben, scheinen ähnlich zu sein: Für fortgeschrittene Studenten ist es gut, für durchschnittliche Studenten aber oft Zeitverschwendung.

    • Als Mathematiker, der auch lange programmiert hat, glaube ich nicht, dass irgendeine programmatische Formalisierung grundlegendes Verständnis hervorbringen wird. Mein Vorurteil kommt daher, dass ich Konzepte über Papers gelernt habe. Code ist oft stilistisch wenig lesbar und dadurch überwältigend; schon schlecht lesbare Papers sind mühsam, aber bei Code ist es wegen fehlender Standards in meiner Erfahrung noch zehnmal schlimmer.

  • Ich freue mich, dass Theorem Proving in Mainstream-Bereichen der Mathematik wie Analysis zunehmend Aufmerksamkeit bekommt. In der PLT gab es bereits das bekannte Beispiel, dass Winskels The Formal Semantics of Programming Languages in Isabelle formal verifiziert wurde (http://concrete-semantics.org). Wenn man mit Theorem Proving anfangen möchte, ist das meiner Meinung nach leichter und eher zu empfehlen. Hinzu kommt, dass Sätze in der Analysis von Natur aus ziemlich schwierig sind.

    • Es würde mich auch nicht überraschen, wenn PL-Beweise eine niedrigere Einstiegshürde hätten. Man hört oft, dass vieles dort routinisierter wirkt — strukturelle Induktion, Anwendung von Induktion, Beweis von Invarianten, Wiederholung und so weiter. Ich habe nicht viel Theorem Proving gemacht, aber mathematische Beweise (vor allem in der Analysis) habe ich noch nie mit einem Theorem Prover geführt. Ich frage mich, ob „mathematische“ Beweise einen ganz anderen Ansatz verlangen und wie viel Skill-Transfer es dazwischen gibt. Ich habe übrigens Software Foundations in Rocq (vielleicht gibt es eine Lean-Portierung?) durchgearbeitet und hatte viel Freude daran.

  • Ich finde, dieses Projekt und dieser Ansatz passen sehr gut zu einem grundlegenden Thema wie Analysis. Ich habe allerdings zwei Sorgen

    1. Die Kernergebnisse der Analysis in Mathlib werden vereinheitlicht über das Konzept der Filter behandelt, spezielle Fälle dagegen separat in epsilon-delta-Form. Ich erwarte, dass Taos Analysis eher den traditionellen epsilon-delta-Ansatz verwendet.
    2. Mathlib ist ein sich schnell veränderndes Projekt, daher ändern sich Namen und Strukturen ständig. Informationen zur Anbindung müssten fortlaufend gepflegt werden.

  • Ich finde das ein sehr großartiges Projekt. Analysis I war für mich als Ingenieur das erste „echte“ Mathematik-Lehrbuch, das ich wirklich von Anfang bis Ende durcharbeiten konnte; an anderen Büchern (etwa Rudin) bin ich mehrfach gescheitert. Mit einer Lean-Version könnten Leute, die sowohl mit Mathematik als auch mit Programmierung vertraut sind, Konzepte noch strenger lernen.

  • Seit Jahren gibt es Versuche einer offiziellen Lean-Formalisierung von Taos Analysis I, aber es war immer schwer, über ein paar Kapitel hinauszukommen. Eine Zeit lang wollte ich das selbst angehen — ich dachte, es wäre nützlich für Leser des Buches, wenn man zusammen mit dem Analysis I-Lösungsblog (https://taoanalysis.wordpress.com/) passende formalisierte Beweise veröffentlichen würde. Ich habe bereits in einem privaten Discord gesammelte Materialien geteilt, und hier fasse ich noch einmal Referenzprojekte in Lean zusammen, die für mehrere Leute nützlich sein könnten (GitHub- und Gist-Links, offizielle Dokumentation usw.).

  • Ich frage mich, wie wichtig der „Beweis eines Isomorphismus zu dem entsprechenden Objekt in Mathlib“ tatsächlich ist. Könnte es nicht sein, dass praktisch gar nichts verloren geht, wenn man diesen Isomorphie-Teil weglässt? Wird das zum Beispiel wirklich für Dinge wie automatische Übersetzung von Sätzen verwendet?

    • Solche Isomorphie-Beweise sind aus zwei Gründen wichtig:

      1. Sie erlauben es, zu zeigen, dass das selbst konstruierte Objekt und das in Mathlib bereits vorhandene Objekt tatsächlich dasselbe sind, insbesondere wenn das Mathlib-Objekt über eine komplex generalisierte Konstruktion definiert ist; das hilft, den Unterschied zu verstehen.
      2. Sie spielen eine entscheidende Rolle dabei, die offizielle Notation oder Terminologie zu verstehen, die in Mathlib zum Lesen oder Schreiben dieses Objekts verwendet wird.

    • Ich denke, sie haben zumindest pädagogischen Wert, weil man dadurch selbst nachvollzieht, dass die Mengen und Operationen, die man konstruiert hat, auch an anderen Stellen im Buch „dieselben“ sind.

  • Ich freue mich über Lean-basierte Lehrbücher. Aber warum gibt es kein HoTT (Homotopy Type Theory)? Es gibt auch einen Meinungsartikel mit der Frage „Should Type Theory (HoTT) replace (ZFC) set theory“ (https://news.ycombinator.com/item?id=43196452). Außerdem wurden weitere Lean-bezogene Community-Ressourcen geteilt, die diese Woche auf HN aufgetaucht sind — „100 theorems in Lean“ (https://news.ycombinator.com/item?id=44075061) und das DeepMind-Lean-Projekt (https://news.ycombinator.com/item?id=44119725).

    • Ich sehe allerdings nicht, warum unbedingt auch noch HoTT dabei sein müsste. HoTT-Theorem-Prover sind bisher nicht besonders benutzerfreundlich, und es gibt auch nicht genug Dokumentation. Mir ist außerdem nicht klar, welchen Gewinn HoTT bringt; sinnvoll erscheint es meist nur beim Umgang mit extrem speziellen Strukturen wie etwa in der Kategorientheorie.

    • Da es sich um einen traditionellen Lehrbuchansatz handelt, steckt die Antwort auf die Frage „Warum nicht HoTT?“ eigentlich schon darin. Außerdem gibt es meines Erachtens viele Fachleute, die dem pädagogischen Nutzen skeptisch gegenüberstehen.