Synthetic Differential Geometry in Lean

TL;DR

This paper formalizes synthetic differential geometry in Lean, proving a Taylor theorem around infinitesimals, demonstrating Lean's capability for constructive mathematics.

Contribution

It introduces a formalization of synthetic differential geometry in Lean and proves a new Taylor theorem for multivariable functions.

Findings

Proved a Taylor theorem around infinitesimal neighborhoods

Formalized synthetic differential geometry in Lean

Showcased Lean's potential for constructive mathematics

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.