[banner] Michael Eisermann

Sesqui-LEAN-ear

Absolut einmalig und garantiert frei von Leistungspunkten! Das nächste sensationelle studentische Seminar, im September 2025 wieder in Hilberts Herberge, auf der wunderschönen Burg Liebenzell, von Donnerstag 18.09. bis Sonntag 21.09.2025.

Begeistert blicken wir zurück auf unser Seminar zu Kategorien im Januar 2023 auf der Burg Liebenzell, unser Sesquinar zu Tensoren im September 2023 in der JuHe Tübingen und unser Semi-LEAN-ear im September 2024 wieder auf der Burg. Aufhören wenn es am schönsten ist? Noch nicht... Wir freuen uns auf den vierten Streich, das Sesqui-LEAN-ear!

Was ist LEAN?

Der Lean theorem prover ist ein interaktiver Beweis-Assistent mit einer sehr aktiven Community und einer umfangreichen Bibliothek. In einem formalen System wie Lean können wir mathematische Objekte definieren, ihre Eigenschaften spezifizieren und Beweise formal ausführen. Der Beweis-Assistent prüft diese Beweise auf ihre logische Korrektheit. In einer gelungenen Formalisierung sind somit Aussagen vollständig präzise und Beweise garantiert korrekt.

Formales Beweisen und automatisierte Verifikation entspricht Programmierung und Compilierung, es erfordert praktische Erfahrung ebenso wie theoretische Grundlagen. Im Mathestudium wird zwar viel bewiesen, mehr oder weniger detailliert, doch selten erklärt und nie praktiziert, was ein (vollständiger, formaler) Beweis wirklich ist. Hier lernen wir genau das! Der zusätzliche Aufwand der Formalisierung lohnt sich, die Vorteile sind vielfältig:

Was kann man mit Lean erreichen?

Von 100 klassischen Theoremen sind bereits über 75 in Lean formalisiert. (Jede solche Auswahl ist natürlich willkürlich, doch Wiedijks Liste ist inzwischen kanonisiert.) Weite Teile des Bachelor-Curriculums wurden in Lean formalisiert, siehe mathlib; vermutlich wird dies zukünftig auf die Bachelor-Ausbildung zurückwirken. Anfangs waren Beweis-Assistenten ein Untersuchungsgegenstand der formalen Logik, inzwischen sind sie so ausgereift, dass sie als Werkzeug in der mathematischen Forschung eingesetzt werden. Umfang und Bedeutung formalisierter Mathematik wird in Zukunft zunehmen.

Die Ansprüche, die Mathematiker:innen an Beweise stellen, haben sich über die Jahrhunderte immer wieder verändert. Wäre im digitalen Zeitalter nicht eine vollständige Formalisierung und algorithmische Überprüfung von Beweisen durch Computer angemessen? Diese Frage bleibt umstritten. Eines aber ist aus den bisherigen Erfahrungen klar: Eine solche Formalisierung hat überhaupt nur dann Aussicht auf Erfolg, wenn ein großer Teil der Formalisierung selbst, also der detaillierten formalen Ausformulierung von Beweisen, systematisch durch Computer unterstützt wird. Hier liegt die Aufgabe von interaktiven Beweisassistenten. Sie ermöglichen es uns Menschen, mathematische Beweise so zu formalisieren, dass ein Computer sie verifizieren kann. [...] Wir müssen davon ausgehen, dass für die nächste Generation Mathematiker:innen Beweisassistenten und digitale Beweisbibliotheken zu einem wichtigen Werkzeug avancieren werden.
Projekt ADAM - Anticipating the Digital Age of Mathematics