Der Lean-Begleiter zu Analysis I

 (terrytao.wordpress.com)
2 Punkte von GN⁺ 2025-06-01 | 1 Kommentare | Auf WhatsApp teilen
  • Terence Tao hat ein Begleit-Repository gestartet, das Definitionen, Sätze und Übungsaufgaben aus dem Lehrbuch Analysis I in Lean-Code überträgt
  • Aufgrund der Eigenschaften des Lehrbuchs, das die Konstruktion der natürlichen Zahlen, ganzen Zahlen, rationalen Zahlen und reellen Zahlen sowie Mengenlehre und Logik streng behandelt, eignet es sich strukturell gut zum Lernen mit einem Proof Assistant
  • Der aktuelle Umfang reicht derzeit bis zu Teilen von Kapitel 2, der grundlegenden Mengenlehre in 3.1 und den ganzen Zahlen in 4.1; enthalten ist auch ein Isomorphismus zu den natürlichen Zahlen aus Mathlib
  • Der Code kompiliert in Lean, enthält aber noch viele sorry; statt offizieller Lösungen wird empfohlen, diese in einem Fork auszufüllen
  • Dieses Material ist einerseits ein alternativer Weg, Übungsaufgaben in Lean zu lösen, und kann andererseits als Einstiegsmaterial dienen, um mit fortschreitender Lektüre den Umgang mit Mathlib zu lernen

Ein Projekt zur Übertragung von Analysis I nach Lean

  • Lean companion to “Analysis I” ist ein Projekt, das verschiedene Definitionen, Sätze und Übungsaufgaben aus Analysis I nach Lean „übersetzt“
  • Die Übungsaufgaben des Buches können auch gelöst werden, indem die entsprechenden sorry im Lean-Code ausgefüllt werden
  • Offizielle Lösungen zu den Übungsaufgaben sollen nicht im Begleiter gehostet werden; Versionen mit ausgefüllten sorry können als Fork des Repositories erstellt werden

Warum das Lehrbuch gut zu Lean passt

  • Analysis I ist ein Lehrbuch, das zur Ergänzung bestehender Lehrbücher zur reellen Analysis einen stärkeren Fokus auf grundlegende Fragen legt
    • Konstruktion der natürlichen Zahlen, ganzen Zahlen, rationalen Zahlen und reellen Zahlen
    • Mengenlehre und Logik, die die Entwicklung hochgradig strenger Beweise ermöglichen
  • Als das Buch geschrieben wurde, gab es bereits Proof Assistants wie Coq und Agda, doch formale Verifikation war damals kein Anliegen
  • Später zeigte sich durch Erfahrungen mit formaler Verifikation, dass der Inhalt des Buches gut zu Proof Assistants passt
  • Die naive Typentheorie, die im Buch implizit für die Konstruktion der Standard-Zahlensysteme verwendet wurde, passt gut zu Leans dependenter Typentheorie
  • Auch Leans Unterstützung für Quotiententypen greift die Konstruktionsweise des Buches passend auf

Der bisher nach Lean übertragene Umfang

Verhältnis zu Mathlib

  • Die Formalisierung ist so angelegt, dass sie sich an einigen Stellen von der Standard-Mathematikbibliothek Mathlib für Lean löst und sich an anderen Stellen auf Mathlib stützt
  • In Mathlib gibt es bereits ein Standardkonzept für natürliche Zahlen
  • In der Lean-Formalisierung wird zunächst Chapter2.Nat entwickelt, das die natürlichen Zahlen „von Hand“ neu konstruiert
    • Arbeitet man im Namespace Chapter2, kann es als Nat verwendet werden
    • Dabei werden grundlegende Resultate eingerichtet, die parallel zu den Hilfssätzen über natürliche Zahlen in Mathlib verlaufen
    • Viele dieser Beweise bleiben als Leserübungen offen und sind derzeit durch sorry ersetzt
  • Im Epilog-Abschnitt wird ein Isomorphismus zwischen diesen alternativen natürlichen Zahlen und den natürlichen Zahlen aus Mathlib aufgebaut
    • Genauer gesagt ist auch dieser Isomorphismus selbst als Übungsaufgabe angelegt
  • Danach wird die Konstruktion der natürlichen Zahlen aus Kapitel 2 nicht weiter verwendet; stattdessen kommen die natürlichen Zahlen aus Mathlib zum Einsatz
  • Für spätere Kapitel des Buches ist geplant, sich zunehmend stärker auf Definitionen und Funktionen aus Mathlib zu stützen als auf die eigenen Konstruktionen der früheren Kapitel

Nutzung und Stand der Verifikation

  • Der Code des Repositories kompiliert in Lean
  • Allerdings ist noch nicht getestet, ob die vielen sorry im Code tatsächlich alle ausgefüllt werden können
  • Es muss auch noch geprüft werden, ob die benötigten Hilfssätze oder die API der Lean-Dateien ausreichend sind
    • Das Ziel ist zu überprüfen, ob sich die sorry konzeptionell natürlich ausfüllen lassen, ohne auf schwer verständliche Lean-Programmiertricks angewiesen zu sein
  • Gewünscht ist, dass Freiwillige den Begleiter playtesten, um zu prüfen, ob sich die Übungsaufgaben tatsächlich in Lean lösen lassen
  • Auch weiteres Feedback ist willkommen

Charakter als Einstiegsmaterial für Lean und Mathlib

  • Dieser Begleiter kann nicht nur für reelle Analysis, sondern auch als Einführung in Lean und Mathlib genutzt werden
  • In dieser Hinsicht ähnelt er in gewissem Maß dem Natural number game
  • Das Natural number game überschneidet sich thematisch stark mit Kapitel 2 von Analysis I

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2025-06-01
Meinungen auf Hacker News

  • Das Interessanteste daran, Mathematik mit Lean zu unterrichten, ist meiner Meinung nach das unmittelbare Feedback. Wenn der Beweis eines Studierenden falsch ist, kompiliert er einfach nicht.
    Früher konnte man Feedback nur bekommen, wenn jemand wie ein Tutor, Dozent oder Experte darübergeschaut hat; jetzt kann der Lean-Compiler schnell Rückmeldung geben.
    Für die Zukunft wäre es schön, wenn der Lean-Compiler – ähnlich wie der Rust-Compiler Vorschläge zur Codekorrektur macht – noch lehrreicheres Feedback liefern würde; vielleicht braucht es dafür ein spezialisiertes LLM.

    • Ich stimme fast vollständig zu, mache mir aber Gedanken darüber, dass beim Lernen von Beweisen das langsame Denken verloren gehen könnte.
      Früher bestand das Mathematikstudium oft darin, lange über Aufgaben zu brüten, auf Papier allerlei Ansätze auszuprobieren; dieser Prozess führte manchmal dazu, dass man Konzepte verinnerlichte und auf neue Ideen kam.
      Mit Lean könnte es auch zu einer Arbeitsweise werden, bei der man einfach vieles ausprobiert, zufällig überprüft und Dinge raushaut. Als ich ein paarmal mit Coq gearbeitet habe, ist mir ebenfalls vor allem in Erinnerung geblieben, dass ich herumprobiert und an verschiedenen Stellen herumgedreht habe.
    • Acorn funktioniert bereits auf diese Weise. Wenn ein Beweis fehlschlägt, aber „fast richtig“ ist, zeigt VS Code Vorschläge wie die folgenden an:
      reduce(r.num, r.denom) = reduce(a, b)
      cross_equals(a, b, r.num, r.denom)
      r.denom * a = r.num * b
      Es verwendet kein LLM; in der VS-Code-Erweiterung läuft ein kleines lokales Modell. Es wäre schön, wenn dieses kleine lokale Modell eines Tages so stark würde, dass es Menschen weit übertrifft. Mehr dazu steht unter https://acornprover.org/docs/tutorial/proving-a-theorem/.

  • Ich freue mich wirklich darauf. Es wäre schön, wenn es in ein eigenes Repository verschoben würde, damit man es leichter finden und an andere weitergeben kann.
    Ich hatte mich ursprünglich für Mathematik interessiert, und Taos Analysis war das erste Lehrbuch, das mir zeigte, wie Mathematik auf die strenge Weise aufgebaut ist, die mein Programmiererkopf erwartet hatte.
    Später habe ich auch ein wenig Lean ausprobiert und fand es ähnlich befriedigend, aber Mathlib war ziemlich komplex, wenn man es zum Lernen mathematischer Konzepte nutzen wollte. Deshalb freut es mich, dass eine Brücke zwischen Buch und Werkzeug entsteht.

    • Ich habe Konvergenz, Cauchy-Folgen und Ähnliches ebenfalls mit diesem Buch gelernt. Es erschien bei einem lokalen gemeinnützigen Verlag namens Hindustan Book Agency und war sehr günstig.

  • Es ist schön zu sehen, dass Theorem Proving bei Mainstream-Themen der Mathematik wie der Analysis an Fahrt gewinnt.
    In der Programmiersprachentheorie wurde bereits Mitte der 2010er Jahre, als die Werkzeuge ziemlich ausgereift wurden, ein Standardlehrbuch wie Winskels The Formal Semantics of Programming Languages in Isabelle formal verifiziert. Es ist keine vollständige 1:1-Übertragung, aber http://concrete-semantics.org ist ein Beispiel dafür.
    Wenn man sich für Theorem Proving interessiert, halte ich persönlich diesen Bereich für einen deutlich leichteren Einstieg. Denn Sätze der Analysis sind für sich genommen schon ziemlich schwierig.

    • Es überrascht mich nicht, wenn Beweise in der Programmiersprachentheorie für den Einstieg leichter sind. Wie andere sagen, scheint es dort viel mehr formalisierte Verfahren zu geben.
      Man führt strukturelle Induktion durch, wendet die Induktionsannahme an, zeigt, dass Invarianten erhalten bleiben, und macht so weiter.
      Ich habe weder sehr viele Theorem-Proving-Beweise gemacht noch mit Beweisassistenten „mathematische“ Beweise wie in der Analysis geführt, aber wenn mathematische Beweise einen deutlich anderen Ansatz verlangen, frage ich mich, wie viel Know-how sich zwischen beiden Bereichen übertragen lässt.
      Erwähnen möchte ich auch Rocqs Software Foundations. Vielleicht gibt es einen Lean-Port, aber als ich die ersten Teile nachvollzogen habe, war das ziemlich angenehm.

  • Es wäre sehr interessant zu bewerten, wie sich der Mainstream-„Lehrbuch“-Ansatz vom Ansatz von Mathlib unterscheidet.
    Im Allgemeinen formulieren formalisierte Mathematikbibliotheken Ergebnisse so allgemein wie möglich und machen es leichter, Beweisentwicklungen intuitiver und eleganter zu refaktorisieren.
    Refactoring ist deshalb leicht, weil das System ständig nachverfolgt, was logisch woraus folgt. Bei der Arbeit mit Papier und Stift hat man das nicht, weshalb man Gelegenheiten zur Überarbeitung oft verpasst.
    Eine naheliegende Frage ist auch, ob es sinnvoll ist, im Grundstudium reelle Analysis in der Mathlib-Version mit „maximaler Allgemeinheit“ zu unterrichten. Dasselbe gilt natürlich auch für andere Bereiche beweisbasierter Mathematik.

    • Für Einführungskurse sicher nicht, denke ich. Es gibt ohnehin schon zu viel zu lernen: wie man Beweise führt, wie man programmiert, und dazu noch den eigentlichen Stoff des Fachs.
      Soweit ich weiß, ähneln die Erfahrungen von Lehrenden, die das tatsächlich versucht haben, diesem Eindruck. Für fortgeschrittene Studierende kann es in Ordnung sein, aber bei durchschnittlichen Studierenden dürfte es wahrscheinlich Unterrichtszeit verschwenden.
    • Aus Sicht eines Mathematikers, der auch seit Langem programmiert, glaube ich, dass jede Art von programmatischem Formalismus daran scheitern wird, ein grundlegendes Verständnis zu vermitteln.
      Meine Voreingenommenheit kommt allerdings daher, dass ich mathematische Konzepte aus Papers gelernt habe.
      Code stellt eine enorme zusätzliche Belastung dar und folgt meiner Erfahrung nach meist keinerlei Stilstandards. Als jemand, der auch mathematische Papers lesen musste, die als unverständlich gelten, würde ich sagen: Für Code gibt es praktisch fast keine Standards der Verständlichkeit, daher ist er zehnmal schlimmer.

  • Auf Terence Taos eigenem YouTube-Kanal gibt es ebenfalls einige Videos, in denen er Lean verwendet: https://www.youtube.com/@TerenceTao27
    Ich kenne die Details nicht, aber es war cool zu sehen, wie er mit oder ohne LLM arbeitet.

  • Für ein grundlegendes Thema wie Analysis halte ich das für ein sehr gutes Projekt und einen guten Ansatz.
    Zwei Sorgen kommen mir sofort in den Sinn. Erstens verwenden die zentralen Analysis-Ergebnisse in Mathlib den Begriff der Filter, um Grenzwerte allgemein und einheitlich zu behandeln. Einige Ergebnisse sind dennoch auf die Epsilon-Delta-Form spezialisiert. Ich vermute, Taos Analysis wird den traditionelleren Epsilon-Delta-Ansatz verwenden.
    Zweitens entwickelt sich Mathlib schnell und bricht häufig Dinge. Namen ändern sich, Refactorings passieren ständig, sodass nachgelagerte Repositories kontinuierliche Wartung brauchen.

  • Ein ziemlich radikaler Gedanke, aber ich finde, der Mathematikunterricht sollte sich darauf konzentrieren, Computeralgebrasysteme wie Mathematica und Theorem Prover wie Lean zu entwickeln. Visualisierung und praktische Anwendungen sollten ebenfalls stark einbezogen werden.
    Im Extremfall könnte das bedeuten, dass man gar keine Papiermathematik mehr macht und trotzdem alles, was man gelernt hat, in Lean beweisen kann.
    Das heutige System konzentriert sich auf endlose Rechnungen von Hand; das wirkt auf mich ziemlich nutzlos und langweilig und führt dazu, dass Menschen Mathematik nicht mögen.

  • Ein Lean-Lehrbuch, schön. Aber warum gibt es kein HoTT?
    „Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?“
    https://news.ycombinator.com/item?id=43196452
    Weitere Lean-Ressourcen, die diese Woche auf HN erschienen sind:
    „100 theorems in Lean“
    https://news.ycombinator.com/item?id=44075061
    „Google-DeepMind/formal-conjectures: collection of formalized conjectures in lean“ https://news.ycombinator.com/item?id=44119725

    • Die Formalisierung verschiedener Ideen aus HoTT läuft derzeit in der Agda-Community. https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/
      Die genaue Motivation liegt außerhalb meines Fachgebiets, daher weiß ich es nicht, aber Agda scheint besser geeignet zu sein als Lean, um diese Ideen zu formalisieren.
      Später in diesem Jahr soll außerdem ein neues Lehrbuch erscheinen, das eine modernere Aktualisierung des bestehenden HoTT-Buchs darstellt, inklusive Agda-Formalisierung.
      https://www.cambridge.org/core/books/introduction-to-homotopy-type-theory/0DD31EC06C80797A50ACE807251E80B6
      https://github.com/HoTT-Intro/Agda
    • HoTT ist ein sehr technisches und sehr enges Thema, daher ergibt es keinen Sinn, zwei derart ambitionierte Projekte gleichzeitig anzugehen.
      HoTT ist keineswegs kurz davor, als vernünftiger Standard akzeptiert zu werden, und für die meisten Menschen ist es ein Thema, bei dem sie schon am Anfang stecken bleiben.
      Das ist ein bisschen so, als würde man einen JavaScript-Framework-Entwickler fragen, warum er kein Framework für Elm oder Haskell gebaut hat.
    • Ich sehe auch nicht, warum HoTT dabei sein sollte.
      Es wurde deutlich weniger Arbeit investiert, um HoTT-Theorem-Prover benutzerfreundlich zu machen, und die Dokumentation ist deutlich schwächer.
      Auch der Nutzen von HoTT ist unklar. Es scheint nur dann Arbeit zu sparen, wenn man mit sehr obskuren Konstruktionen aus der Kategorientheorie zu tun hat.
    • Die Frage „Warum gibt es kein HoTT?“ ist etwas seltsam.
      Terrence Tao hat mehrere Lehrbücher zur Analysis, und dies ist das Lean-Begleitmaterial zu seinem ersten Buch. Er hat kein Lehrbuch zur Typentheorie, also gibt es auch keine höhere Typentheorie. Das, worum es ursprünglich geht, ist etwas völlig anderes.
    • Schon die Tatsache, dass es sich um Begleitmaterial zu einem bestehenden Lehrbuch handelt, beantwortet die Frage „Warum nicht HoTT?“. Ein weiterer Grund könnte sein, dass die Leute am didaktischen Wert zweifeln.

  • Sehr cool. Analysis I war für mich als Ingenieur und nicht als Mathematiker das erste „echte“ Mathematiklehrbuch, bei dem ich nach mehreren Anläufen mit anderen Büchern wie Rudin das Gefühl hatte, es vollständig nachvollziehen und durcharbeiten zu können.
    Ich hoffe, dass das Lean-Begleitmaterial es für Menschen, die mit Mathematik und Programmierung vertraut sind und rigoros lernen wollen, zugänglicher macht.

  • In den letzten Jahren gab es immer wieder Versuche, Taos Buch Analysis I in Lean zu formalisieren, und es gab Leute, die genau das tun wollten, was Tao jetzt macht. Leider kamen die meisten nicht über die ersten paar Kapitel hinaus; Tao hofft, weiter zu kommen
    Ich hatte auch überlegt, es selbst zu versuchen. Denn wenn ich in meinem Begleitblog zu Analysis I https://taoanalysis.wordpress.com/ formalisierte Beweise zu jeder Übungsaufgabe ergänzen würde, wäre das wohl nützlich für diejenigen, die das Buch durcharbeiten
    Ich habe es auch auf dem privaten Discord-Server zum Buch gepostet, teile die einschlägigen Materialien aber auch hier, da sie hilfreich sein könnten
    https://github.com/cruhland/lean4-analysis — stammt aus https://github.com/cruhland/lean4-axiomatic
    https://github.com/Shaunticlair/tao-analysis-lean-practice
    https://github.com/vltanh/lean4-analysis-tao
    https://github.com/gabriel128/analysis_in_lean
    https://github.com/mk12/analysis-i
    https://github.com/melembroucarlitos/Tao_Analysis-LEAN
    https://github.com/leanprover-community/NNG4/ — folgt zwar nicht Taos Buch, ist aber die Lean4-Version des Natural Number Game und inhaltlich Kapitel 2 sehr ähnlich
    https://github.com/djvelleman/STG4/ — ein Mengenlehre-Spiel für Lean4, könnte also Kapitel 3 ähneln. Allerdings sieht man in https://github.com/djvelleman/STG4/blob/main/Game/Metadata.lean import Mathlib.Data.Set.Basic, daher scheint es die Mengen von Lean zu importieren, statt Mengen neu zu definieren und Axiome aufzustellen. Dieser Ansatz könnte Lean „zu viel“ über Mengenlehre wissen lassen und für den Zweck ungünstig sein
    https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc — zur Konstruktion der ganzen Zahlen
    https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/IntegerGame.lean — könnte dieselbe Datei wie oben sein
    https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/RationalGameAlgebra.lean — zur Konstruktion der rationalen Zahlen
    https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality — zeigt eine Möglichkeit, einen benutzerdefinierten Set-Typ zu definieren