Synthetic Differential Geometry in Lean
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908923169079296 |
|---|---|
| author | Brasca, Riccardo Clemente, Gabriella |
| author_facet | Brasca, Riccardo Clemente, Gabriella |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_17457 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Synthetic Differential Geometry in Lean Brasca, Riccardo Clemente, Gabriella Logic in Computer Science Differential Geometry 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. |
| title | Synthetic Differential Geometry in Lean |
| topic | Logic in Computer Science Differential Geometry |
| url | https://arxiv.org/abs/2603.17457 |