Formal verification of a theorem by Clausen and Scholze

• Applicant: Professor Dr. Johan Commelin
• Subject Area: Mathematics
• Term: from 2021 to 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 468348485

This is a proposal in pure mathematics, and more particularly condensed mathematics – a new subfield of mathematics currently being developed by Dustin Clausen and Peter Scholze.Following up on a challenge by Scholze, this proposal brings together two highly different things: condensed mathematics and computer verified mathematics. The task of this project is to formally verify the foundations of condensed mathematics, up to the main theorem on liquid R-modules. This theorem is the cornerstone in the new approach to analytic geometry put forward by Clausen and Scholze. The proof relies on an intricate mix of homological algebra and functional analysis.

• DFG Programme: WBP Position