Zulip Chat Archive
Stream: Lean for the curious mathematician 2020
Topic: Video uploads
Dan Stanescu (Jun 30 2020 at 18:45):
Can't seem to find any information about possible video recordings from the conference and subsequent uploads to YouTube or some other service. Since people elsewhere than EU will have trouble being present in all live sessions I'm sure there's a plan for that. Will this be announced later?
Johan Commelin (Jun 30 2020 at 18:45):
Yup, we haven't settled completely on what we will do. Advice and/or help is welcome.
Johan Commelin (Jun 30 2020 at 18:46):
Maybe we should start a leanprover-community account on youtube? And post the recordings in some stream there?
Rob Lewis (Jun 30 2020 at 18:46):
I can only speak for myself, but right now I'm hoping to pre-record at least one of my talks, and I'll definitely post it myself if there's no organizational plan.
Rob Lewis (Jun 30 2020 at 18:47):
Johan Commelin said:
Maybe we should start a
leanprover-communityaccount on youtube? And post the recordings in some stream there?
It exists already, we used it for FoMM/LT2020.
Johan Commelin (Jun 30 2020 at 18:47):
Ooh, great
Johan Commelin (Jun 30 2020 at 18:47):
I guess we can reuse that?
Rob Lewis (Jun 30 2020 at 18:47):
https://www.youtube.com/channel/UCWe5B7Ikr0AI9727doEUxPg?view_as=subscriber
Rob Lewis (Jun 30 2020 at 18:47):
Yep!
Johan Commelin (Jun 30 2020 at 18:47):
Who are the admins of that account?
Rob Lewis (Jun 30 2020 at 18:48):
Me, but there are some others here who could guess the password pretty easily...
Dan Stanescu (Jun 30 2020 at 18:49):
Even if talks are not pre-recorded, live talk recordings will be great to have. They may not have quite the same quality, but that's OK.
Rob Lewis (Jun 30 2020 at 18:51):
Oh, hey, @Reid Barton has comments on his FoMM video. https://www.youtube.com/watch?v=8jEeIfbQ2eY
Rob Lewis (Jun 30 2020 at 18:51):
Are you the Reid Barton?
Reid Barton (Jun 30 2020 at 18:52):
as far as youtube comments go, could be worse, I suppose
Johan Commelin (Jun 30 2020 at 18:53):
You didn't have your IMO medals with you... so how can they know for sure?
Bryan Gin-ge Chen (Jun 30 2020 at 18:53):
Is o-minimality still getting formalized? (can't tell if this question is now on-topic or off-topic).
Johan Commelin (Jun 30 2020 at 18:54):
Well... let's say that we're still working on o-minimality
Johan Commelin (Jun 30 2020 at 18:54):
But the formalisation hasn't gotten any real love yet.
Bryan Gin-ge Chen (Jun 30 2020 at 18:56):
Cool, looking forward to seeing more!
Patrick Massot (Jun 30 2020 at 21:38):
Great, I wanted to ask about having a leanprover-community Youtube account.
Patrick Massot (Jun 30 2020 at 21:39):
This is certainly much more discoverable than most alternatives, even if it may not be the most ethic choice.
Tom Harris (Jul 05 2020 at 13:03):
Just wanted to add my +1 for video uploads. I am planning to attend the first half of the conference but the second half clashes with a pre-planned cycling holiday. I hope to be able to catch up on what I miss later (from a curious ex-mathematician).
Johan Commelin (Jul 14 2020 at 18:19):
All the talks so far have been recorded, and the recordings have been uploaded to youtube: https://www.youtube.com/playlist?list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N
I've also added the links on to the recordings over at https://researchseminars.org/seminar/LeanCurious
Johan Commelin (Jul 15 2020 at 17:36):
Todays talks have been uploaded and links have been added on https://researchseminars.org/seminar/LeanCurious
Youtube playlist: https://www.youtube.com/watch?v=8mVOIGW5US4&list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N
Last updated: Dec 20 2023 at 11:08 UTC