Zulip Chat Archive

Stream: general

Topic: July meeting in Amsterdam


view this post on Zulip Rob Lewis (Jun 24 2019 at 08:47):

Hey everyone! We're planning to have a small Lean users meeting in Amsterdam next month, July 10-12. Sorry for the late notice, this has been planned sort of last minute. @Kevin Buzzard @Patrick Massot @Floris van Doorn will join the local crowd, and anyone else who wants to make the trip is more than welcome.

view this post on Zulip Rob Lewis (Jun 24 2019 at 08:48):

We'll start Wednesday afternoon to allow for travel time that morning.

view this post on Zulip Patrick Massot (Jul 04 2019 at 15:33):

Do we have a participant list for this Amsterdam meeting next week? It would help to prepare for greater efficiency. @Jan-David Salchow for instance, will you be around?

view this post on Zulip Jan-David Salchow (Jul 10 2019 at 05:37):

I’m still avoiding lean while finishing my thesis ;) But I’m happy to show up on Thursday or Friday evening

view this post on Zulip Jan-David Salchow (Jul 10 2019 at 05:38):

Is there a schedule for the meeting somewhere? Or is it purely informal?

view this post on Zulip Rob Lewis (Jul 10 2019 at 08:18):

Oops, sorry Patrick, I missed your message from before. Jan-David, there's no official schedule, but we can keep you updated!

view this post on Zulip Kevin Kappelmann (Jul 13 2019 at 11:15):

Hi, we had a brief discussion about tactics that people wish would be there. Here's the list
- Groebner basis: compute if something is an ideal
- Polya (nonlinarith and field)
- modules: normalforms like ring, abel
- continuity: Proving continuity of (composition of) functions
- obtain: combine have : \exists ... with rcases this ...
- fix the WLOG tactic
- Label for rcases: rcases label : term with ...
- some tactic to collect have statements, e.g. something like have : ..., moreover have : ...., show ... by simp -- the last simp uses the last two collected hypotheses


Last updated: May 12 2021 at 04:19 UTC