2.2 KiB
Aufgabe: Entwickle passend zum vorliegenden Skript einen Einfügungskurs in LEAN.
Hintergrund: Ich werde dieses Skript im kommenden Semester für die Vorlesung "Algebra und Zahlentheorie" verwenden, die die in Deutschland üblichen Vorlesungen in "Linearer Algebra" fortsetzt. Parallel bietet ein Kollege (=Peter Pfaffelhuber) eine Einführung in den Beweisassistenten "LEAN" an.
Ich möchte für die Studenten aus diesem Grund ein weiteres Skript verfassen, "Algebra in LEAN", das vom Stil etwa dem bekannten Tutorial "Mathematics in LEAN" entspricht. Das Ziel ist, Studenten für Formalisierung zu interssieren und praktisch zu zeigen, dass studienrelevante Inhalte tatsächlich mit vertretbarem Aufwand formalisiert werden können -- und das Formalisierung vielleicht sogar richtig Spaß machen kann.
-
Die Sprache sollte Deutsch sein.
-
Das neue Skript richtet sich an Studenten, die Algebra lernen und noch wenig Erfahrung mit LEAN haben. Insbesondere kennen die Studenten die Spezifika von Mathlib noch nicht und haben höchstens einmal kursatorisch in "Mathematics in LEAN" geschaut.
-
Der Inhalt sollte einen Querschnitt der Themen aus der Vorlesung aufgreifen, mit meiner Kapitelstruktur, die dem Skript ähnelt. Idealerweise sollte interessantere Beweise examplarisch umgesetzt werden.
-
Konstruierbarkeit von Punkten in der Ebene ist in Mathlib nicht wirklich vorhanden. Das lassen wir vielleicht besser weg.
-
Ich stelle mir vor, Beweise wörtlich aus der Vorlesung zu übernehmen und Satz-für-Satz in LEAN zu übersetzen, damit die Studenten sehen, wie sich die Standardphrasen in LEAN/Mathlib übersetzen. Die Beweise im vorliegenden Skript sollten dann Links zum LEAN-Skript bekommen.
-
Ähnlich wie in "Mathematics in LEAN" sollte erläutert werden, wie die wesentlichen Begriffe ("Gruppe", "Körper", "Gruppenwirkung") in der Mathlib dargestellt sind, und wie man mit diesen Begriffen in LEAN umgeht.
-
Ich bin unsicher, wie man das LEAN-Skript technisch am besten realisiert. Mit einem GIT-Repo, das man den Studenten zur Verfügung stellt? Als Webseite und/oder PDF? Mit einem VERSO Textbook?
-
Vielleicht ist es sinnvoll, erst einmal einen einzelnen Beweis beispielhaft umzusetzen, bevor wir eine Vielzahl von Beweisen bearbeiten.