HOME | ENGLISH | IMPRESSUM | KIT

Bachelorarbeit (abgeschlossen): Diagrammjagd in einem interaktiven Theorembeweiser

Wir erweitern die mathematische Bibliothek des interaktiven TheorembeweisersLean um Definitionen und erste Resultate über abelsche Kategorien. Insbesondere formalisieren wir die Theorie der Pseudoelemente, welche die Beweistechnik der Diagrammjagd in einem allgemeinen kategoriellen Kontext zugänglich macht. Wir nutzen die in Lean verfügbaren Methoden der Metaprogrammierung zur Entwicklung einer interaktiven Taktik, die Exaktheitsaussagen in abelschen Kategorien durch Diagrammjagd mit Pseudoelementen halbautomatisch beweisen kann. Mithilfe dieser Automatisierung geben wir den ersten formal verifizierten Beweis des Schlangenlemmas, einem wichtigen Werkzeug der homologischen Algebra, das aufgrund seiner Rolle in der Konstruktion der langen exakten Sequenz in Kohomologie in vielen Bereichen der reinen Mathematik und darüber hinaus Anwendung findet.

Schlüsselworte

Lean, Formalisierung 

Veröffentlichungen

Veröffentlichung
Diagram Chasing in Interactive Theorem Proving

Betreuer

Wissenschaftliche Mitarbeiter
Sebastian Ullrich

Studenten

Studenten
Markus Himmel