Zulip Chat Archive

Stream: general

Topic: advertising Lean meetings

Jeremy Avigad (Aug 13 2020 at 00:22):

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

Lean for the Curious Mathematician: https://leanprover-community.github.io/lftcm2020/
Formal Methods in Mathematics / Lean Together 2020: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/
Lean Together 2019: https://lean-forward.github.io/lean-together/2019/

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.

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.

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:

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

Rob Lewis (Aug 13 2020 at 20:12):

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

Jeremy Avigad (Aug 13 2020 at 20:20):

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

Patrick Massot (Aug 13 2020 at 20:37):

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

Patrick Massot (Aug 13 2020 at 20:37):

FoMM2020 was mostly about meeting.

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.

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

Alex J. Best (Aug 13 2020 at 20:43):

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

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: Dec 20 2023 at 11:08 UTC