Topic sessions

Stream: Lean Together 2019

[Patrick Massot]

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:

[Johan Commelin]

Aah, so that is where I get to talk?

[Patrick Massot]

That would be the next topic session

[Patrick Massot]

since topic sessions last only one hour

[Rob Lewis]

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

[Rob Lewis]

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

[Johan Commelin]

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:

[Assia Mahboubi]

@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).

[Sebastian Ullrich]

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

[Rob Lewis]

This sounds great!

[Assia Mahboubi]

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.

[Cyril Cohen]

@Sebastian Ullrich great!