Elements of Differential Geometry in Lean: A Report for Mathematicians

TL;DR

This paper discusses the formalization of differential geometry concepts in Lean's mathlib, highlighting differences from traditional methods and illustrating with case studies on Lie groups, vector bundles, and Lie algebras.

Contribution

It provides an accessible account for geometers on formalizing differential geometry in Lean, emphasizing the differences from classical approaches and sharing practical case studies.

Findings

Formalization reveals differences in equality treatment compared to pen-and-paper methods.

Case studies demonstrate the applicability of Lean to complex geometric structures.

The report encourages geometers to explore formal proof systems like Lean.

Abstract

We report on our experience formalizing differential geometry with mathlib, the Lean mathematical library. Our account is geared towards geometers with no knowledge of type theory, but eager to learn more about the formalization of mathematics and maybe curious enough to give Lean a try in the future. To this effect, we stress the possibly surprising difference between the formalization and its pen-and-paper counterpart arising from Lean's treatment of equality. Our three case studies are Lie groups, vector bundles and the Lie algebra of a Lie group.