LEAN – der Beweis stimmt!

Die Forschung in der Mathematik ist eine höchst aktive Welt. Das Herzstück dabei sind die mathematischen Sätze und deren Beweise. Diese Beweise werden aber immer komplizierter und auch die Kontrolle auf Korrektheit ist schwierig und fehleranfällig. Da die Verifikation eines Beweises ein nur bedingt kreativer Prozess ist, kann er in sogenannten Beweisassistenten formalisiert werden. Lean in der Version 3 und 4 ist einer der modernsten und leistungsfähigsten. Dies wurde unter anderem durch die Verifikation eines Satzes des deutschen Fields-Medaillenträger Peter Scholze sowie an einem Beweis von Terence Tao, ebenfalls Fields-Medaillenträger, nachgewiesen. In unserem Projekt haben wir uns intensiv mit dem auf Typentheorie basierenden Lean 4 beschäftigt und eigene Definitionen und Beweise „geleant“. Unser großes Ziel ist es am Ende das Paradoxon von Banach-Tarski, welches noch nicht geleant ist, zu leanen und damit einen Beitrag zur Bibliothek der mit Lean verifizierten Sätze zu leisten.