Informationen zur Praktische Übung Mathematik in Lean
Dozent: Prof. Dr. Peter Pfaffelhuber
Assistent: Jakob Stiefel, M.Sc.
Termin: Mo 14–16 Uhr, SR 232, Ernst-Zermelo-Str. 1
ETCS-Punkte: 3 Punkte
Inhalte
Seit einiger Zeit gibt es Software (besser gesagt Programmiersprachen), mit der sich mathematische Inhalte formal beweisen lassen. Ein mittlerweile ausgereiftes System ist Lean, das wir uns in dieser Praktischen Übung näher ansehen wollen. Dieses Vorgehen erfordert zwar etwas Einarbeitung, birgt aber den großen Vorteil, dass alle Voraussetzungen der zu verifizierenden Aussagen genau überprüft werden. Somit ist im Rahmen dieser Veranstaltung die Möglichkeit gegeben, sich noch einmal mit dem Stoff des ersten Studienjahres in Mathematik auseinanderzusetzen. Die Praktischen Übungen werden auf den Laptops der Studierenden durchgeführt werden.
Sie richten sich vor allem an Lehramts-Studierende in Mathematik, etwa im Rahmen des Master of Education. Anhand von Beispielen aus der Schulmathematik wollen wir die Sprache Lean lernen (um etwa die natürlichen Zahlen einzuführen und einige ihrer Eigenschaften zu zeigen). Wer einen ersten Eindruck von der Sprache bekommen will, kann sich vorab hier informieren:
Aktuelles
Um den Kurs sinnvoll durcharbeiten zu können, sind folgende technische Vorbereitungen zu treffen:
- Lokale Installation von Lean und der dazugehörigen Tools: Folgen Sie bitte den Hinweisen hier.
- Installation von vscode. Bitte befolgen Sie die Download-Hinweise hier.
- Installation des Repositories des Kurses: Navigieren Sie zu einem Ort, wo Sie die Kursunterlagen ablegen möchten und verwenden Sie
leanproject get https://github.com/pfaffelh/schulmathematik_mit_lean
. Dies sollte die Kursunterlagen herunterladen. Anschließend finden Sie das Manuskript unterManuskript/skript.pdf
, und Sie können die Übungen mitcode schulmathematik_mit_lean
öffnen. Die Übungen befinden sich dabei insrc
. Wir empfehlen, dieses Verzeichnis zunächst zu kopieren, etwa nachmysrc
. Andernfalls kann es sein, dass durch ein Update des Repositories die lokalen Dateien überschrieben werden. Um die Kursunterlagen auf den neuesten Stand zu bringen, geben Siegit pull
im Verzeichnisschulmathematik_mit_lean
ein.
Studien- und Prüfungsleistung
Die Anforderungen an Studien- und Prüfungsleistungen entnehmen Sie bitte dem aktuellen Modulhandbuch.
Übungsgruppen und Übungsblätter
2-stündig nach Vereinbarung
Literatur
- Natural number game,
https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ - C. Löh: Exploring Formalisation, Springer, 2022.
Aus dem Uni-Netz verfügbar unter https://link.springer.com/book/10.1007/978-3-031-14649-7 - K. Buzzard. Formalizing Mathematics, course 2023.
Notwendige Vorkenntnisse
Grundvorlesungen
Sprechstunden
Sprechstunde Dozent: nach Vereinbarung
Sprechstunde Assistent: nach Vereinbarung