Zum Hauptinhalt springen

Funktionalanalysis in Lean

Lean ist ein interaktiver Beweisassistent, das heißt ein Programm in dem es möglich ist mathematische Sätze zu beweisen. Beweisassistenten wurden kürzlich genutzt um ein technisches Lemma im Bereich der algebraischen Geometrie zu verifizieren (das Liquid Tensor Experiment initiiert von Peter Scholze). In der Analysis ist die mathematische Bibliothek von Lean noch nicht allzu mächtig und Ziel dieses Projektes ist es einen Beitrag für die Funktionalanalysis zu leisten.

Empfohlen sind grundlegende Kenntnisse aus den Bereichen Analysis sowie Lineare Algebra und Grundkenntnisse im Bereich Funktionalanalysis und Programmiererfahrung wären vorteilhaft. Die Dauer der Bearbeitung innerhalb der Arbeitsgruppe soll mindestens vier Wochen betragen. Zudem wird eine schriftliche Ausarbeitung und ein Abschlussvortrag im Seminar erwartet.