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 unter Manuskript/skript.pdf, und Sie können die Übungen mit code schulmathematik_mit_lean öffnen. Die Übungen befinden sich dabei in src. Wir empfehlen, dieses Verzeichnis zunächst zu kopieren, etwa nach mysrc. 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 Sie git pull im Verzeichnis schulmathematik_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