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…