We formalize synthetic differential geometry using the Lean proof assistant and the mathlib library. Our primary contribution is a formalized Taylor theorem for multivariable functions with series expansion around infinitesimal neighborhoods, featuring novel proofs and demonstrating constructive mathematics possibilities.
Riccardo Brasca, Gabriella Clemente
Synthetic Differential Geometry in Lean
Riccardo Brasca, Gabriella Clemente
HAL (2026)