PreprintCC BY 4.0HAL
Synthetic Differential Geometry in Lean
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.
Related
- Synthetic geometry of differential equations: I. Jets and comonad structure
- Assumption-Lean Inference for Spectral Differential Network Analysis of High-Dimensional Time Series
- Retro-synthetic Riemannian geometry in Rocq I : Taylor series of a metric
- Turaev cobracket, synthetic geometry and applications
- An outline of shifted Poisson structures and deformation quantisation in derived differential geometry
BibTeX
@misc{brasca2026synthetic,
title = {{Synthetic Differential Geometry in Lean}},
author = {Riccardo Brasca and Gabriella Clemente},
howpublished = {HAL},
year = {2026},
month = oct,
eprint = {2603.17457},
archivePrefix = {arXiv},
url = {https://hal.science/hal-05555752v3},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Synthetic Differential Geometry in Lean
AU - Riccardo Brasca
AU - Gabriella Clemente
PY - 2026
DA - 2026/10/15
PB - HAL
UR - https://hal.science/hal-05555752v3
AB - 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.
ER -