Dieser zweiwöchige Blockkurs an der Freien Universität Berlin bietet eine praxisorientierte Einführung in die formale Beweisverifikation mit dem Theorembeweiser Lean. Die Vorlesungen finden am Zuse-Institut Berlin (ZIB) statt; die Räume für die Tutorien an der FU werden nach Anmeldestand bekanntgegeben. Der Kurs steht allen offen (auch Gasthörer*innen); bei den Tutorien haben FU-Studierende mit ABV-Bedarf Priorität. Bitte einen eigenen Laptop mitbringen. Erwartet werden solide Kenntnisse aus Analysis I und Linearer Algebra I; Programmierkenntnisse sind nicht erforderlich, eine technische Affinität ist jedoch hilfreich. Lehrsprache ist Englisch (Beiträge auf Deutsch sind willkommen). Alle Informationen und Materialien — u. a. zu Logik, Mengenlehre, natürlichen Zahlen, Unendlichkeit der Primzahlen und Grundzügen der Graphentheorie — finden sich auf der GitHub-Seite des Kurses.

Für eine Anrechnung im Master wird der Kurs um differenzierte Übungen und erweiterte Prüfungsleistungen ergänzt. Die Übungsaufgaben sind dreistufig: grundlegende Aufgaben (mit gut lesbaren Beweisvorlagen), vertiefte Aufgaben auf Master-Niveau sowie optionale Stretch-Aufgaben; während der Übungen erfolgt Betreuung und eine informelle Fortschrittsrückmeldung. Die Abschlussprüfung ist eine schriftliche Klausur, die sowohl Konzeptverständnis als auch praktische Lean-Fertigkeiten prüft. Zusätzlich bearbeiten Master-Studierende ein Lean-Formalisierungsprojekt (einzeln oder zu zweit) und präsentieren es in einem mündlichen Prüfungsgespräch ein bis zwei Wochen nach Kursende; die M.Sc.-Note ergibt sich aus Klausur und Projekt.