2 papers
math.CT2024
Categorical Foundations of Formalized Condensed Mathematics
Dagur Asgeirsson, Riccardo Brasca, Nikolas Kuhn +2
Condensed mathematics, developed by Clausen and Scholze over the last few years, proposes a generalization of topology with better categorical properties. It replaces the concept o…
math.HO2024
Anatomy of a Formal Proof
Jeremy Avigad, Johan Commelin, Heather Macbeth +1
Interactive proof assistants make it possible for ordinary mathematicians to write definitions and theorems in a formal proof language, like a programming language, so that a compu…