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
Betreuer
Studenten
