Zulip Chat Archive

Stream: general

Topic: 2000


Patrick Massot (Aug 23 2019 at 09:09):

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

Patrick Massot (Aug 23 2019 at 09:13):

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

Sebastien Gouezel (Aug 23 2019 at 09:27):

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 (Aug 23 2019 at 09:28):

I can see summer fun is over.

Patrick Massot (Aug 23 2019 at 09:28):

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

Patrick Massot (Aug 23 2019 at 09:32):

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 (Aug 23 2019 at 09:34):

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 (Aug 23 2019 at 09:36):

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

Sebastien Gouezel (Aug 23 2019 at 09:43):

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 (Aug 24 2019 at 12:24):

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

Sebastien Gouezel (Aug 25 2019 at 09:03):

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 (Sep 04 2019 at 08:21):

It was #1394. How boring.

Patrick Massot (Sep 04 2019 at 08:21):

Oh crap

Patrick Massot (Sep 04 2019 at 08:22):

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

Sebastien Gouezel (Sep 04 2019 at 09:02):

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


Last updated: Dec 20 2023 at 11:08 UTC