Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synthetic Differential Geometry in Lean

Riccardo Brasca, Gabriella Clemente

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.

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.
Paper Structure (13 sections, 22 theorems, 64 equations)

This paper contains 13 sections, 22 theorems, 64 equations.

Table of Contents

  1. Synthetic versus ordinary differential calculus
  2. Logical framework and Lean implementation
  3. The axiom of unique choice
  4. Lean implementation
  5. Excluded middle
  6. Basics
  7. Basic definitions and results
  8. One variable differential calculus
  9. 1-Kock–Lawvere rings
  10. Kock–Lawvere rings
  11. Several variables differential calculus
  12. Partial derivatives
  13. Taylor theorems in several variables

Key Result

Theorem 1.1.1

(Taylor's theorem in ordinary differential calculus) Let $f\in C^k(U,\mathbb{R})$. For any $l\leq k$ and any $x_0\in U$, as $\|h\| \to 0$

Theorems & Definitions (42)

  • Theorem 1.1.1
  • Lemma 2.3.1
  • proof
  • Definition 3.1.1
  • Lemma 3.1.2
  • Lemma 3.1.3
  • Lemma 3.1.4
  • Lemma 3.1.5
  • Lemma 3.1.6
  • proof
  • ...and 32 more