# Real manifolds in a theorem prover?

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).

• I think {proof-assistants}; my question on that tag a while ago was well enough received, though I guess standards might change. I will edit the tags. Jul 18, 2019 at 0:02
• It's just my opinion, but this question looks fine for MO, because the math community as a whole is, I think, curious about where the current frontier of proof assistant technology is (whereas questions about technicalities that are peculiar to a particular proof assistant would probably not be so welcome). On the other hand, in the long run you might be better off finding a friendly expert who is likely to know the answer to this sort of thing. Jul 18, 2019 at 14:41
• All the experts I asked so far said "well, they're not in the systems I know, as far as I know..." Jul 19, 2019 at 0:40
• It seems difficult to me to implement manifolds without first doing it for multivariate calculus. Has this been done already? Jul 24, 2019 at 20:22
• I would say "the definition of a real manifold has been around for over 80 years"; the standard reference is Hassler Whitney, "Differentiable Manifolds", Annals of Mathematics 37 (1936), 645-680, where he defined them in order to prove the embedding and immersion theorems. people.math.osu.edu/davis.12/courses/6701/whitney36.pdf
– user44143
Jul 28, 2019 at 2:55

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:
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.