2000

Stream: general

[Patrick Massot]

Who has a nice idea for mathlib's 2000th commit? Remember the 1000th commit was the big module refactor.

[Patrick Massot]

Maybe some huge commit by @Sebastien Gouezel bringing manifolds in?

[Sebastien Gouezel]

We should not let numerology prevail over good practice: I'd rather let the interface stabilize (I am still changing some design decisions due to the difficulties I encounter further on), and then submit it in small chunks that would be easier to discuss and review.

[Patrick Massot]

I can see summer fun is over.

[Patrick Massot]

But of course I agree that getting the interface right is very important

[Patrick Massot]

Yesterday night I finally read the Isabelle manifolds paper and, apart from yelling "maths needs dependent types, continuing with Isabelle is foolish", it also makes it clear that partial functions are a huge pain for everybody.

[Patrick Massot]

It also makes it very clear that we need mathematicians to play this game together with computer science experts. Or else we need to be more explicit in our books about what is a joke aimed only at illustrating a definition. Otherwise we'll see more people putting a manifold structure on spheres and projective spaces using an explicit atlas.

[Patrick Massot]

(and claiming these constructions are "advanced results"...)

[Sebastien Gouezel]

This is why I decided to do this in Lean: it has to be done, and it has to be done in the right generality (including manifolds with boundaries, infinite dimensional manifolds, and so on, with the possibility to include without futher problems oriented manifolds, contact manifolds, and so on). The difficulty is really not with the proofs, but with the definitions!

[Jeremy Avigad]

A better question is, what should we do for 2001?
https://www.rottentomatoes.com/m/2001_a_space_odyssey/quotes/

[Sebastien Gouezel]

I have started submitting some stuff. If this goes well, you could get the smooth manifold structure on the tangent bundle to a smooth manifold for 2000 (but before that you would need to review local_equivs #1359, then local homeomorphisms, then manifolds for a general groupoid, then smooth manifolds, then fiber bundles).

[Chris Hughes]

It was #1394. How boring.

[Patrick Massot]

Oh crap

[Patrick Massot]

Do you think people will complain if we rewrite history and force push?

[Sebastien Gouezel]

Or aim for 2048, which is definitely more round that 2000.