Synthetic Differential Geometry in Lean
Logic in Computer Science
2026-04-01 v2 Differential Geometry
Abstract
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.
Keywords
Cite
@article{arxiv.2603.17457,
title = {Synthetic Differential Geometry in Lean},
author = {Riccardo Brasca and Gabriella Clemente},
journal= {arXiv preprint arXiv:2603.17457},
year = {2026}
}