Papers With

← All papers
First page of Synthetic Differential Geometry in Lean

Synthetic Differential Geometry in Lean

Riccardo Brasca, Gabriella Clemente

cs.LO Mar 18, 2026 · v1
formalization geometry
Read PDF arXiv abstract
TL;DR
Formalizes synthetic differential geometry and a multivariable Taylor theorem in Lean with mathlib.
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.
Problem

Synthetic differential geometry (SDG) provides an alternative foundation for differential calculus using nilpotent infinitesimals, but it had not been formalized in the Lean proof assistant with mathlib.

Approach

The authors formalize synthetic differential geometry in Lean 4 using the mathlib library. The main result proved and formalized is a Taylor theorem for functions of several variables, where the series expansion is around an infinitesimal neighborhood. Most proofs are new. The work highlights the possibility of using mathlib to do constructive mathematics within the SDG framework.

Results

The formalization produces a machine-checked proof of a multivariate Taylor theorem in the synthetic differential geometry setting, with most proofs being novel constructions developed during the formalization process.