Algebra in Lean🔗

Dies sind Kursnotizen zum Formalisieren von Algebra mit dem interaktiven Theorembeweiser Lean und seiner Mathematikbibliothek Mathlib. Sie begleiten die Vorlesung Algebra und Zahlentheorie (Universität Freiburg, Winter 2026/27) mit ihrem deutschsprachigen Skript und sind dafür gedacht, parallel zum Kurs Interactive Theorem Proving using Lean von Peter Pfaffelhuber gelesen zu werden, der Lean selbst einführt. Wir gehen hier den komplementären Weg: Wir nehmen an, dass Sie gerade die Algebra lernen, und zeigen an Beispielen, dass sich der Stoff der Vorlesung mit vertretbarem Aufwand formalisieren lässt — und dass das sogar richtig Spaß machen kann.

Wie diese Notizen funktionieren. Ausgewählte Beweise aus dem Skript werden Satz für Satz nach Lean übersetzt: Jeder deutsche Originalsatz steht als Kommentar direkt über dem Lean-Code, der ihn umsetzt. Sie werden sehen, dass die Standardphrasen eines Vorlesungsbeweises — „Ansonsten liefert die Restklasse …“, „Nach dem Satz von Lagrange …“, „Also existiert mindestens ein …“ — wiedererkennbaren Zügen in Lean entsprechen. Jedes Kapitel endet mit einer Übungsaufgabe, deren sorry Sie durch einen Beweis ersetzen sollen.

Woher bekomme ich das Material? Die Übungsdateien liegen im selben Repository wie diese Notizen, im Ordner AlgebraInLean/:

git clone https://git.cplx.vm.uni-freiburg.de/kebekus/AlgebraInLean.git
cd AlgebraInLean
lake exe cache get
code .

Öffnen Sie dann zum Beispiel AlgebraInLean/LittleFermat.lean. Warten Sie, bis die orangefarbenen Balken verschwinden; setzen Sie den Cursor in einen Beweis und beobachten Sie, wie das Infoview-Panel den aktuellen Beweiszustand anzeigt. Für die Installation von Lean und VS Code selbst folgen Sie der Anleitung der Lean-Community oder der ausführlichen Anleitung am Anfang der Notizen von Peter Pfaffelhuber.