Synthetic Differential Geometry in Lean
This work enables formal verification of constructive mathematics in Lean, which is incremental for the proof assistant community.
The authors formalized synthetic differential geometry in Lean, proving a Taylor theorem for functions of several variables around infinitesimal neighborhoods, with most proofs being new.
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 formalize is a Taylor theorem for functions of several variables, where the series expansion is around an infinitesimal neighborhood. Most of our proofs are in fact new. Our investigations highlight the possibility of using mathlib to do constructive mathematics.