Lean has real manifolds!

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…

About xenaproject

The Xena Project aims to get mathematics undergraduates (at Imperial College and beyond) trained in the art of formalising mathematics on a computer. Why? Because I have this feeling that digitising mathematics will be really important one day.
This entry was posted in General, undergrad maths and tagged , , . Bookmark the permalink.

5 Responses to Lean has real manifolds!

  1. Pingback: Lean does not (yet) have real manifolds. | Xena

  2. Coq^2 says:

    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.


    • xenaproject says:

      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.

      Liked by 1 person

  3. Milnor Fan says:

    What about tangent microbundles?


    • xenaproject says:

      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.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s