2 papers
cs.LO2026
Synthetic Differential Geometry in Lean
Riccardo Brasca, Gabriella Clemente
This article is about the formalization of synthetic differential geometry with the Lean proof assistant and the mathematical library mathlib. The main result we prove and formaliz…
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…