Which of the formal computer proof verification systems (like Lean, Coq, Agda, Idris, Isabelle-HOL, HOL-Light, Mizar etc) have a basic theory of real manifolds? Up to, say, the definition of a smooth map between manifolds, and examples such as real projective space or Grassmannians?

PS what is the correct tag for questions about proof verification systems? Are they even welcome here?

OK so this question has been around for a week, with no answers.

The concept of a real manifold has been around for over 100 years and is both a fundamental mathematical object and something taught in any half-decent undergraduate mathematics degree. Almost all these lectures are given by mathematicians.

The concept of a formal proof verification system has been around for maybe 40 years, and many mathematical proofs have been formalised in these systems. Almost all the proofs are written by computer scientists.

I am not so sure that the concept of real manifold is mentioned in many computer science degrees. And I am not so sure that there are too many "how to use formal proof verification software" courses in maths departments.

And because that's where we stand today in 2019, it appears that there are basic undergraduate-level mathematical objects which nobody has even attempted to formalise the definition of -- the mathematicians because on the whole they don't know where to start, and the computer scientists because they don't know the definitions.

Since I started trying, as a mathematician, to figure out how these systems worked, I have learnt a lot of things. But the fact that these systems have been around for decades but still none of them seem to contain all the theorems and proofs in a standard pure mathematics undergraduate degree was in some sense the most surprising thing I've learnt.

Hopefully real manifolds will appear in one or more of these systems at some point (or they are there already but nobody posted here yet).