And tangent bundles too! Thank you Sébastien Gouëzel! Tangent bundles would be hard to do in simple type theory (e.g. Isabelle/HOL) because they are naturally a dependent type, and if you work around this in the way that the HOL people usually do then you seem to have to abandon typeclasses (so sheaves of rings would be hard to work with).
I think that one measure of how appropriate a computer proof system is for human researchers is whether it can state the Clay Millenium problems. If a system isn’t strong enough to even state the problems then surely it is not going to be of much interest to most “working mathematicians”. Which systems can state all of them? None of the systems can. Manifolds are an initial but important step towards the statement of the Hodge Conjecture. Of course we also have to formalise some cohomology theories. I have an MSc student, Shenyang Wu, working on group cohomology, which I always felt was the most concrete and down-to-earth of the cohomology theories which I know.
But before we get too excited, let’s still remember that Lean does not (yet) have the Cauchy Integral Formula…
Xena 
Pingback: Lean does not (yet) have real manifolds. | Xena
I think Harrison did Cauchy’s integral theorem circa 2005 in HOL, but some trickier stuff (residues, Rouche, etc) was not done until an Isabelle port a decade later.
LikeLike
Yes, most of the other systems are way ahead of us when it comes to analysis. This is partly because it’s difficult to set up and partly because most of the mathematicians involved with Lean are more on the algebraic/topological side of things. We’ll get there in the end. Isabelle can state the Riemann Hypothesis.
LikeLiked by 1 person
What about tangent microbundles?
LikeLike
I don’t know what they are! [googles] OK so whilst these might not be in Lean yet, they would be easy to do — much easier than real manifolds, because they seem to be a topological definition rather than one that uses the C^infty structure. It was the C^infty structure, and in particular what that means for a manifold with boundary, which was made the process so subtle.
LikeLike