33
$\begingroup$

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

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – LSpice Jul 18 '19 at 0:02
  • 6
    $\begingroup$ 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. $\endgroup$ – Timothy Chow Jul 18 '19 at 14:41
  • 1
    $\begingroup$ All the experts I asked so far said "well, they're not in the systems I know, as far as I know..." $\endgroup$ – Kevin Buzzard Jul 19 '19 at 0:40
  • 7
    $\begingroup$ It seems difficult to me to implement manifolds without first doing it for multivariate calculus. Has this been done already? $\endgroup$ – Deane Yang Jul 24 '19 at 20:22
  • 3
    $\begingroup$ 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 $\endgroup$ – Matt F. Jul 28 '19 at 2:55
11
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ There's a formalisation under development in Lean, led by Sebastien Gouezel, but it hasn't landed yet. $\endgroup$ – Scott Morrison Jul 28 '19 at 0:57
  • $\begingroup$ So this has restored my faith in humanity somewhat -- however the date on the paper appears to be "CPP ’19, January 14–15, 2019" -- so this was this year (or at least published this year) and because they're using simple type theory they perhaps won't be able to give the tangent space at a point the structure of a vector space (because a vector space structure in Isabelle/HOL goes on a type, not a set). $\endgroup$ – Kevin Buzzard Jul 28 '19 at 19:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.