Zulip Chat Archive

Stream: Lean Together 2019

Topic: So Long, and Thanks for All the Fish

Johan Commelin (Jan 11 2019 at 13:21):

Eventually my neighbourhood filter tends to that of Freiburg.
Henceforth I will have very good memories of this workshop.

I couldn't say goodbye to everyone. But I really enjoyed this workshop! Kudos to Rob and Johannes. Thanks to Jasmin for getting a grant (-; I loved the talks, the hacking sessions were excellent. Thanks to all of you.
Keep up the good math!

Simon Hudon (Jan 11 2019 at 14:57):

It was a pleasure meeting you in person and interacting with you!

Patrick Massot (Jan 11 2019 at 20:56):

I'm also back at home, and very happy with my week in Amsterdam. Thanks everybody, especially Jasmin, Johannes and Rob!

Johannes Hölzl (Jan 11 2019 at 21:17):

Thanks everybody for joining the meeting!

Rob Lewis (Jan 12 2019 at 10:54):

Yes, thank you all for a wonderful week! Let's keep the momentum going. Hope to see you all again at Lean Together 2020.

William Whistler (Jan 12 2019 at 14:50):

Great to meet you all, and thank you very much for the valuable talks and side discussions (and of course, thank you once again to the organisers for making it all happen!).

Patrick Massot (Jan 12 2019 at 21:07):

@Rob Lewis and @Johannes Hölzl I think it would be good to update the schedule the agenda one last time in order to keep an accurate record of what was actually done (and maybe move it to a better format that this google doc).

Simon Hudon (Jan 12 2019 at 22:34):

Did anyone think of taking notes of the more informal conversations?

Amin Bandali (Jan 12 2019 at 22:42):

Did anyone think of taking notes of the more informal conversations?

They'd be especially valuable since there doesn't seem to be any video recordings from the sessions of the last two days, for those of us that didn't manage to make it to Amsterdam for the conference

Rob Lewis (Jan 13 2019 at 10:54):

Which parts are inaccurate? Surprisingly, I thought we stayed fairly close to the suggested plan. I guess the Lean 4 discussion moved down a slot.

Rob Lewis (Jan 13 2019 at 10:55):

I'm traveling until Wednesday and have a huge backlog of stuff to get through, but I can add reformatting the schedule to the list, unless anyone wants to do it faster. :wink:

Simon Hudon (Jan 14 2019 at 14:00):

Friday was more according to schedule but I don't think @Assia Mahboubi's and @Cyril Cohen's talks were on the schedule. Also, are their slides online?

Patrick Massot (Jan 14 2019 at 15:02):

I would mention that the perfectoid slot on Thursday actually started with unification hints by Assia and Cyril, and the actual perfectoidy stuff was animated by Kevin. The documentation was Jeremy and I, not Kevin and I (Kevin talked of course, but he was not standing up). And the mathlib reorganization discussion was led by Johannes and Mario.

Rob Lewis (Jan 14 2019 at 15:04):

Assia's Coq file and Cyril's Lean file are on the website.

Last updated: Dec 20 2023 at 11:08 UTC