Formale Verifikation eines Satzes von Clausen und Scholze

• Antragsteller: Professor Dr. Johan Commelin
• Fachliche Zuordnung: Mathematik
• Förderung: Förderung von 2021 bis 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 468348485

Dies ist ein Vorschlag in der reinen Mathematik, und insbesondere in der kondensierten Mathematik - einem neuen Teilgebiet der Mathematik, das derzeit von Dustin Clausen und Peter Scholze entwickelt wird.Einer Herausforderung von Scholze folgend, bringt dieser Vorschlag zwei sehr unterschiedliche Dinge zusammen: kondensierte Mathematik und computerverifizierte Mathematik. Die Aufgabe dieses Projekts ist es, die Grundlagen der kondensierten Mathematik formal zu verifizieren, bis hin zum Hauptsatz der "liquid R-Modules". Dieser Satz ist der Eckpfeiler des neuen Ansatzes zur analytischen Geometrie, der von Clausen und Scholze vorgelegt wurde. Der Beweis beruht auf einer komplizierten Mischung aus homologischer Algebra und Funktionalanalysis.

• DFG-Verfahren: WBP Stelle