Formalizing differential geometry in a proof assistant presents challenges that differ from pen-and-paper mathematics, particularly around Lean's treatment of equality, and these challenges are not well documented for working geometers.

The authors report on formalizing differential geometry in Lean's Mathlib, targeting geometers with no type theory background. They highlight differences between formalization and pen-and-paper proofs arising from Lean's handling of equality. Three case studies are presented: Lie groups, vector bundles, and the Lie algebra of a Lie group.

The formalization reveals that definitional equality in Lean forces choices that have no pen-and-paper analogue, particularly around bundled vs. unbundled structures. The case studies demonstrate working solutions for key differential geometry concepts in Mathlib.