In diesem Seminar lernen Sie den interaktiven Beweisassistenten Lean und die Beweisbibliothek Mathlib kennen. Insbesondere lernen Sie,
- in Lean formulierte mathematische Aussagen zu verstehen,
- selbst mathematische Aussagen in Lean zu formulieren, und
- in Lean formalisierte Aussagen mit „Taktik-Beweisen“ zu verifizieren.
Hintergrund
Lean ist eine funktionale Programmiersprache, die gleichermaßen für die Entwicklung verifizierbarer Software und für die Formalisierung und Verifikation mathematischer Aussagen geeignet ist. Zum Beispiel wird Lean von Amazon Web Services eingesetzt, um die Verlässlichkeit ihrer Richtliniensprache Cedar zu garantieren (AWS Blog). Die erste größere Aufmerksamkeit in der Mathematik wurde Lean durch Peter Scholzes liquid tensor experiment zuteil (Lean community blog). 2023 verifizierte eine Gruppe von Mathematiker um Terence Tao den Beweis der polynomiellen Freiman-Ruzsa-Vermutung in Lean (Quanta Magazine).
Inzwischen gibt es nicht nur KI-Modelle, die in der Lage sind, eigenständige mathematische Forschung zu betreiben, sondern auch Modelle, die komplexeste Aussagen und Beweise eigenständig in Lean formalisieren können. Um nur einige Beispiele zu nennen:
- diverse Erdös-Probleme
- Sätze über dichteste Kugelpackungen in den Dimensionen 8 und 24, für die Maryna Viazovska 2022 die Fields-Medaille erhielt
- die Existenz einer komplexen Struktur auf der 6-dimensionalen Sphäre
Vieles spricht also dafür, dass formalisierte Formulierungen sich in absehbarer Zeit als neuer mathematischer Sprach-Standard durchsetzen werden. Ziel des Seminars ist es, sich mittels Formalisierungsübungen (ohne KI-Unterstützung) ein eigenes Verständnis dieser Sprache anzueignen.
Ablauf
Kern des Seminars wird das eigens entwickelte Lernspiel „Robo“ bzw. eine vom Math For AI Fund unterstützte Weiterentwicklung desselben sein.
Das Seminar beginnt in der ersten Vorlesungswoche am angegebenen Termin. Eine vorherige Anmeldung ist nicht erforderlich. Sie sollten einen eigenen Laptop (mit funktionierendem WLAN und eduroam-Zugang) mitbringen. Falls Sie kein geeignetes Gerät haben, melden Sie sich bitte im Vorfeld.