Department Mathematik
print
Navigationspfad
Inhaltsbereich


Sommersemester 2025

Computergestütztes mathematisches Beweisen
Vorlesung: dienstags 8:15-9:45 Uhr und freitags 14:15-15:45 Uhr, Raum B 251
Zentralübung: donnerstags 14:15-15:45 Uhr (Raum wird noch bekanntgegeben)
Die Übung findet im CIP-Pool statt. Dort beginnen wir gemeinsam mit der Bearbeitung des jeweils aktuellen Übungsblatts, die dann selbst vervollständigt werden kann. Am 24. April
findet noch keine Übung statt.
Dozent: Dr. Ralf Gerkmann
Prüfung: Der Erwerb der ECTS-Punkte erfolgt am Ende der Vorlesungszeit durch eine 30-minütige mündliche Prüfung (Termine nach Vereinbarung).
Vorlesungsskript: wird in Kürze hier bereitgestellt
Übungsblätter: sind über Moodle verfügbar
Vorlesungsverlauf:
DatumInhalt Lean-CodeSkript
25.04.25
Inhalt: Dank der Fortschritte in den Bereichen Softwaretechnik und Programmiersprachen der letzten Jahre ist es möglich geworden, mathematische Definitionen, Sätze und Beweise einerseits in der allgemein üblichen, gut lesbaren Notation auf dem Computer darzustellen, dabei anderer­seits aber so präzise zu bleiben, dass die Korrektheit und Lückenlosigkeit der Argumentation von Algorithmen geprüft werden kann. Im vorliegenden Kurs soll die Formulierung beliebiger mathematischer Inhalte mit Hilfe des Beweisassistenzsystems „Lean 4“ erlernt werden.

Obwohl sich die Darstellung sehr stark an der vertrauten mathematischen Notation orientiert, ist es hilfreich, über einige Grundkonzepte Bescheid zu wissen, die man auch in anderen Pro­gram­miersprachen antrifft (z.B. Listen, Strukturen, Vererbung, Typklassen, Rekursion). Darum kümmern wir uns in einem ersten (kurzen) Teil der Vorlesung. Durch diese Grundlagen ist es einfacher, die Arbeitsweise des Systems nachzuvollziehen. Anschließend beschäftigen wir uns damit, wie mathematische Aussagen und Beweise unter Lean aufgebaut sind, und wie man diese auf möglichst komfortable Weise darstellt und strukturiert.

Im weiteren Verlauf konzentrieren wir uns dann ganz auf das mathematische Beweisen. Anhand verschiedener Themen, die größtenteils aus den Anfängervorlesungen bekannt sind, erlernen wir schrittweise die Übertragung mathematischer Konzepte auf das Lean-System. Unter ande­rem befassen wir uns mit
  • Beweisen von Gleichungs- und Ungleichungsketten auf der Basis bekannter Rechenregeln
  • vollständiger und transfiniter Induktion, Ordinal- und Kardinalzahlen
  • Beweis von Mengengleichungen
  • Verifikation von Berechnungsverfahren (euklidischer Algorithmus)
  • algebraischen Grundstrukturen (Gruppen, Ringe, Körper)
  • Analysis (Konvergenz von Reihen, Stetigkeit, Differenzierbarkeit)
  • Linearer Algebra (Konstruktion von Vektorräumen, Matrizenkalkül, Dimensionsbegriff)
Bei der Behandlung dieser Themen werden wir uns auch mit dem Lean-Typuniversum und dem vorhandenen Axiomensystem vertraut machen, das wir dem heutzutage allgemein akzeptierten Axiomensystem der Mathematik (Prädikatenlogik und ZFC-Mengenlehre) gegenüberstellen. Auf diese Weise lernen wir also zwei alternative Zugänge zu den Grundlagen der Mathematik kennen.
Literatur Für das Lean-System gibt es bereits eine Reihe von Anleitungen, Einführungen und Vorlesungs­skripten, die man auf der Homepage von Lean findet. Von dort kann man das System auch herunterladen und auf dem eigenen Rechner installieren. Näheres dazu erfahren Sie in der Vorlesung. Der Aufbau der Vorlesung orientiert sich aber an keiner der Quellen auf dieser Seite.
zurück zur Personalseite