Zulip Chat Archive

Stream: general

Topic: 2000


view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 23 2019 at 09:13):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 23 2019 at 09:28):

I can see summer fun is over.

view this post on Zulip Patrick Massot (Aug 23 2019 at 09:28):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 23 2019 at 09:36):

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

view this post on Zulip 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!

view this post on Zulip 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/

view this post on Zulip 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).

view this post on Zulip Chris Hughes (Sep 04 2019 at 08:21):

It was #1394. How boring.

view this post on Zulip Patrick Massot (Sep 04 2019 at 08:21):

Oh crap

view this post on Zulip Patrick Massot (Sep 04 2019 at 08:22):

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

view this post on Zulip Sebastien Gouezel (Sep 04 2019 at 09:02):

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


Last updated: May 10 2021 at 18:22 UTC