Real manifolds in a theorem prover?

Question

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 on the whole 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).

Answer 1

Andrew Ashworth posted an answer on the Lean discussion forum, and I'll give it here for the sake of having an answer.

Fabian Immler and Bohua Zhan have given a formalisation of $C^k$ and $C^\infty$ manifolds at https://www.isa-afp.org/entries/Smooth_Manifolds.html, describing their development as:

We formalize the definition and basic properties of smooth manifolds in Isabelle/HOL. Concepts covered include partition of unity, tangent and cotangent spaces, and the fundamental theorem of path integrals. We also examine some concrete manifolds such as spheres and projective spaces. The formalization makes extensive use of the analysis and linear algebra libraries in Isabelle/HOL, in particular its “types-to-sets” mechanism.

There's an accompanying paper http://home.in.tum.de/~immler/documents/immler2018manifolds.pdf, which is interesting.

At a few points they point out difficulties that seem to stem from the simple type system available in Isabelle/HOL. In particular they complain that they can't define the tangent space at a point as a type itself, but only as a set, and this is what causes so much difficulty with using the existing Isabelle/HOL library. They also at a few points have some difficulty where they apparently can't do arithmetic with the natural number indexing the dimension of one of their manifolds --- so when defining $n$-spheres for all $n$ they have to jump through some awkward hoops.