Elements of Differential Geometry in Lean: A Report for Mathematicians

Anthony Bordg, Nicolò Cavalleri

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,…