Synthetic Differential Geometry in Lean

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.

Preprint