Zum Bearbeiten/Auswerten einer einzelnen Datei ist oftmals der Web-Editor ausreichend. Es gibt zwei Server mit im wesentlichen identischen Editoren:
Kurze Dateien lassen sich einfach durch Kopieren und Versenden der URL teilen. Längere Dateien kann man herauf- und herunterladen.
Um an Projekten zu arbeiten, die aus mehreren Dateien bestehen, kommt man meist an einer lokalen Installation von Lean nicht herum. Der Editor mit der besten Unterstützung für die Entwicklung in Lean ist VS Code. Auf der Leanprover-Community-Seite gibt es für Lean und VS Code eine Installationsanleitung. Nach erfolgreicher Installation ist der nächste Schritt, ein Projekt zu initialisieren, z.B. durch Klonen dieses Repositories.
Mathematics in Lean führt systematisch in die Syntax von Lean ein und behandelt wichtige Teile der Beweisbibliothek mathlib. Kapitel 6 (Structures) und 7 (Hierarchies) gehen bereits deutlich über das hinaus, was im Robo-Spiel vorkommt. Wer sich für Algebra interessiert, liest dann in Kaptitel 8 (Groups and Rings) weiter, wer sich eher für Analysis interessiert, in Kapitel 9 (Topology).
Die Taktik-Varianten mit Fragezeichen (simp?, exact?, apply?, rw?) kamen im Spiel nicht vor, sind aber sehr nützlich – einfach mal ausprobieren! Auch aesop? kann Beweise abkürzen.
In der offiziellen Dokumentation von mathlib gibt es eine rudimentäre Suchfunktion. Wenn man keine Idee hat, wie der Satz heißen könnte, nach dem man sucht, benutzt man besser Loogle. Um zum Beispiel den Satz
theorem imp_iff_not_or : A → B ↔ ¬A ∨ B
in mathlib zu finden, würde man (_ → _ ) ↔ (¬ _ ∨ _) looglen.
Loogle versteht -> und <-> anstelle von → und ↔. Um Suchanfragen mit anderen Unicode-Symbolen zu formulieren, muss man die Anfrage zunächst in einem externen Editor formulieren und nach Loogle kopieren.
Es gibt eine sehr freundliche weltweite Lean/mathlib-Community, die rund um die Uhr Fragen beantwortet. Um Fragen zu stellen, muss man sich allerdings zunächst einen Account auf Zulip zulegen. Die erste Anlaufstelle ist dann der new members-Kanal.
Wir wollen uns im zweiten Teil des Seminars elementarer Analysis zuwenden. Um die Formulierung von Analysis in mathlib nachvollziehen zu können, benötigen wir das das Konzept eines Filters. Dazu:
- das Topologie-Kapitel in Mathematics in Lean
- ein hilfreiches Bild auf Wikipedia
- ein kleines Tutorium in diesem repository (Web-Editor)
