CMSA New Technologies in Mathematics Seminar: Approaches to the formalization of differential geometry

In the last five years, there has been early work on the computer formalization of differential geometry. I will survey the projects I am aware of. I will also describe two projects of my own, as case studies for typical challenges. The first (joint with Floris van Doorn) is an exercise in developing suitable abstractions, the second (joint with Mario Carneiro) is an exercise in developing suitable automation.