Synthetic Differential Geometry in Lean
Abstract
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.- Publication
- Preprint