Department Mathematik
print
Navigationspfad
Inhaltsbereich


Sommersemester 2026
Computergestütztes mathematisches Beweisen

Vorlesung: montags und freitags, jeweils 14:15-15:55 Uhr, im Raum B 134
Zentralübung: dienstags 10:15-11:45 Uhr, Raum BU 135 (CIP-Pool)
Hinweis: Am 14. 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: Das Skript besteht aus einer Reihe von verlinkten, mit ausfürlichem Text versehenen Lean-Dateien, die demnächst unter Moodle abgerufen werden können. Zusätzlich wird es (als Hilfe für die Bearbeitung der Übungsaufgaben) eine kurze Zusammenstellung der bisher behandelten Lean-Anweisungen geben.
Übungsblätter: sind demnächst über Moodle verfügbar
Vorlesungsverlauf:
DatumInhalt
12.04.26
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 nachzuvollzie­hen. Anschließend beschäftigen wir uns damit, wie mathematische Aussagen und Beweise unter Lean aufge­baut 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 verschie­de­ner Themen, die größtenteils aus den Anfängervorlesungen bekannt sind, erlernen wir schrittweise die Über­tragung mathematischer Konzepte auf das Lean-System. Unter ande­rem befassen wir uns mit
  • der Anwendung logischer Schlussregeln und dem Beweis von Mengengleichungen
  • der Beweisführung mittels vollständiger Induktion
  • dem Umgang mit Gleichungs- und Ungleichungsketten sowie mit Summenformeln
  • den Grundlagen der Analysis (Konvergenz von Reihen, Stetigkeit, Differenzierbarkeit)
  • dem Umgang mit algebraischen Grundstrukturen (Gruppen, Ringe, Vektorräume) und
    dem Beweis einfacher Sätze der Algebra
  • dem Aufbau des Zahlensystems (natürliche, ganze, rationale und reelle Zahlen)
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 Ma­thematik (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