Zulip Chat Archive

Stream: Lean Together 2019

Topic: Topic sessions


view this post on Zulip Patrick Massot (Jan 04 2019 at 18:10):

Maybe we could already gather extra suggestions for the topic sessions on Thursday and Friday. I have one: the end of Patrick's talk :stuck_out_tongue_wink:

view this post on Zulip Johan Commelin (Jan 04 2019 at 18:12):

Aah, so that is where I get to talk?

view this post on Zulip Patrick Massot (Jan 04 2019 at 18:12):

That would be the next topic session

view this post on Zulip Patrick Massot (Jan 04 2019 at 18:13):

since topic sessions last only one hour

view this post on Zulip Rob Lewis (Jan 04 2019 at 18:23):

Jeremy is your session chair. Johan, you can ask him to drag Patrick off the stage if he isn't done in 45 minutes.

view this post on Zulip Rob Lewis (Jan 04 2019 at 18:23):

But I think we actually did put the perfectoid spaces project as a suggested discussion topic, so you guys are in luck.

view this post on Zulip Johan Commelin (Jan 04 2019 at 18:27):

We're supposed to give a 90 minute talk together, in peace and harmony. This means that Patrick will do the talking, while I'll be the clown :clown:

view this post on Zulip Assia Mahboubi (Jan 09 2019 at 10:27):

@Cyril Cohen and myself are proposing an extra suggestion: the end of Assia's talk. The proposal is to give an introduction to 2 ingredients of the mathcomp library that could be of interest for mathlib too: small scale reflection (how to take the most of conversion when defining concepts) and unification hints (in particular how to implement instance inference with bundled structures).

view this post on Zulip Sebastian Ullrich (Jan 09 2019 at 10:37):

I'm fine with using the beginning of the Lean 4 discussion slot (first slot on Thursday) for this, then following up with a discussion on why or why not we should do this in Lean 4, then discuss all the other feelings people have about Lean 4

view this post on Zulip Rob Lewis (Jan 09 2019 at 10:39):

This sounds great!

view this post on Zulip Assia Mahboubi (Jan 09 2019 at 10:46):

I'm fine with using the beginning of the Lean 4 discussion slot (first slot on Thursday) for this, then following up with a discussion on why or why not we should do this in Lean 4, then discuss all the other feelings people have about Lean 4

Wonderful, many thanks @Sebastian Ullrich ! Of course not hesitate to chair the session firmly so that there is enough time left for the other important items of the Lean 4 topic.

view this post on Zulip Cyril Cohen (Jan 09 2019 at 10:46):

@Sebastian Ullrich great!


Last updated: May 08 2021 at 21:09 UTC