PhD Defense Dagur Tomas Asgeirsson
Title: Towards a formalized theory of solid modules
Abstract: This thesis is concerned with the formalization of condensed mathematics. It consists of three papers, each of which is a substantial step towards a formalization of the theory of solid abelian groups in the Lean theorem prover. The first paper presents a formalization of Nöbeling's theorem, a technical result which is independent of condensed mathematics proper, but important when setting up the foundations of the solid theory. The second paper describes the most general categorical framework into which condensed sets fit, and how the theory is formalized using this framework. Important examples of condensed sets are given by discrete sets, and the third paper proves the equivalence of several conditions on a condensed set which characterize it as discrete. All the results in the papers have been formalized in Lean and integrated into its mathematical library, mathlib.
Principal supervisor:
Associate Professor Dustin Clausen
Assessment committee:
Professor, Chair Søren Eilers
Department of Mathematical Sciences, University of Copenhagen
Professor, Kevin Buzzard, Imperial College London
Assistant Professor Johan Commelin, University of Utrecht