Interaktive Theorembeweiser ermöglichen es, formale Beweise z.B. über Mathematik oder Programmverifikation computergestützt zu führen, d.h. der Computer überprüft nicht nur die Korrektheit des endgültigen Beweises, sondern hilft auch beim Schreiben desselben. Bisher geschieht dies beim Theorembeweiser Lean dadurch, dass es eine interaktive Anzeige des aktuellen Beweisziels gibt. Für spezifischere Anwendungen gibt es allerdings auch sogenannte Widgets, welche eine grafische Unterstützung beim Schreiben bestimmter Beweise bieten, hier zum Beispiel Widgets, welche beim Erstellen einer Lösung für ein Sudoku-Rätsel bzw. einen Rubik-Würfel hilfreich sind:
Quelle: Markus Himmel, https://github.com/TwoFX/sudoku
Quelle: Kendall Frey, https://github.com/kendfrey/rubiks-cube-group
Im mathematischen Feld der Kategorientheorie, präziser gesagt im Bereich der monoidalen Kategorien, werden String-Diagramme als grafische Repräsentation von mathematischen Objekten verwendet, um Beweise intuitiver zu machen:
Quelle: Peter Selinger, A Survey of Graphical Languages for Monoidal Categories
Ziel dieser Masterarbeit ist, es ein Lean-VSCode-Widget zu bauen, welches Morphismen in bestimmten Klassen monoidaler Kategorien darstellt und manipulierbar macht.
Voraussetzungen
- Kenntnisse in Algebra (wenn auch nicht unbedingt Kategorientheorie)
- Kenntnisse in Theorembeweisen oder abhängigen Typen werden nicht benötigt
Schlüsselworte
Lean Betreuer
| Wissenschaftliche Mitarbeiter |
|---|
| Dr. Jakob von Raumer |