Zulip Chat Archive

Stream: general

Topic: advertising Lean meetings


view this post on Zulip Jeremy Avigad (Aug 13 2020 at 00:22):

At least three Lean meetings I know of have materials and recorded talks available :

Would it be helpful to add a Meetings section at the end of the Lean learning resources page? https://leanprover-community.github.io/learn.html.

view this post on Zulip Rob Lewis (Aug 13 2020 at 07:46):

Right now they're linked from the Meet us page but it could make sense to move them.

view this post on Zulip Jeremy Avigad (Aug 13 2020 at 20:05):

Oops, I just did a PR and then saw this message. I don't have a strong opinion here; in either case, we should add LFTCM 2020. Options:

  1. Cancel the PR, add LFTCM 2020 to Meet us.
  2. Delete the list from Meet us in the PR.
  3. Keep both (though the redundancy is probably bad).
    @Rob Lewis What do you think?

view this post on Zulip Rob Lewis (Aug 13 2020 at 20:12):

I'm fine with moving them to the learning resources page.

view this post on Zulip Jeremy Avigad (Aug 13 2020 at 20:20):

O.k., it's in the PR.

view this post on Zulip Patrick Massot (Aug 13 2020 at 20:37):

I think there is room for both. LFTCM was primarily for learning, but FoMM2020 wasn't.

view this post on Zulip Patrick Massot (Aug 13 2020 at 20:37):

FoMM2020 was mostly about meeting.

view this post on Zulip Alex J. Best (Aug 13 2020 at 20:41):

Do we have a list of talks about lean in non Lean meetings? I saw @Anne Baanen gave a talk about ring_exp (the same week as lfctm but in a different conference?) for example and it's on youtube. It would be nice to collate a list of these video links somewhere too.

view this post on Zulip Patrick Massot (Aug 13 2020 at 20:42):

Doesn't YouTube allow that? I think the lean community user can have a list of video it likes (but we can also have something on the main website of course).

view this post on Zulip Alex J. Best (Aug 13 2020 at 20:43):

Yeah I think we can make a playlist? That will appear on the profile

view this post on Zulip Jeremy Avigad (Aug 13 2020 at 20:57):

Often (but not always), the talks are associated with papers. For example, Anne's paper is already list. Maybe it makes sense to add links to such videos after the papers? (This can be in addition to the full YouTube playlist.)


Last updated: May 15 2021 at 23:13 UTC