Notations in Differential Geometry

Stream: Is there code for X?

[Trebor Huang]

If I read the docs correctly then there isn't too much differential geometry in mathlib (no differential forms etc). In fact, to my knowledge there isn't any work in any proof assistant that formalizes a substantial part of conventional introductory differential geometry. (I would be delighted to see a counterexample!)

Is there a rough plan of the formalization in mathlib? In particular, I'm interested in the notation system it is going to use. It is well known that differential geometry is "the study of invariants under change of notations". And all the textbooks I've read almost always heavily overload notation, and are very inconsistent with each other. So perhaps a formalization would really provide insight on how to organize concepts in diff. geo. into readable notation.

[Kevin Buzzard]

My understanding is that work in this area is slow but sure right now, with part of the slowness due to the fact that we're currently moving from lean 3 to lean 4. We have smooth manifolds and the tangent bundle. To get the cotangent bundle and its wedge powers, which we'll need for differential forms, we need to be able to do linear algebra on bundles over smooth manifolds, and my understanding is that this problem has been solved recently. I think that one long term goal is de Rham cohomology of a manifold and there will be a meeting in Banff in May about cohomology theories where I hope some progress will be made.