Any Lean live streams?

Stream: general

[Mark Ettinger]

A quick search on Zulip reveals several years ago there were some Lean Twitch streams. As a mathematician learning Lean4 (too slowly), I would greatly benefit from hanging out and asking questions during a stream by someone experienced in Lean. Are there any ongoing streams on Twitch or elsewhere?

[Yaël Dillies]

I am in fact considering starting streaming some sessions once I have a stable setup, but it might be a few months before that happens

[Kenny Lau]

you could consider streaming yourself :slight_smile:

[Mark Ettinger]

I have considered streaming myself but, unfortunately, I'm a bit too self-conscious with my stumbling about in Lean. @Yaël Dillies I can guarantee you at least one enthusiastic attendee so I hope your setup becomes stable sooner rather than later!

[Kenny Lau]

surely if someone else is streaming their own efforts then it's more likely that they wouldn't have the time to answer your questions; but if you yourself are streaming then chat can answer your questions

[Julian Berman]

@awalterschulze occasionally streams at https://www.twitch.tv/awalterschulze

[Julian Berman]

I think @David Renshaw does as well perhaps more sporadically?

[David Renshaw]

sometimes, yeah!

[awalterschulze]

Mark Ettinger said:

I have considered streaming myself but, unfortunately, I'm a bit too self-conscious with my stumbling about in Lean. Yaël Dillies I can guarantee you at least one enthusiastic attendee so I hope your setup becomes stable sooner rather than later!

If you think you are stumbling around in Lean we did too:
https://www.youtube.com/playlist?list=PLYwF9EIrl42RFQgbmcR_LSCWRIx2WKbXs
https://www.youtube.com/playlist?list=PLYwF9EIrl42Qr52nnmeuSXp47S79sB3W0
https://www.youtube.com/playlist?list=PLYwF9EIrl42Q18E0JtYn9QUau4MCLppiL
And this was not our first stumble, we were stumbling and being very self-conscious streamers in Coq for a few years before that.

We are of the opinion that this stumbling is valuable to see. Proofs/Dependent Type programming can be very intimidating. It is good to see that there are people in the space that are struggling, but still completing some projects and that everyone here isn't born an expert, like it might seem. We hope that our streams help a little to make it seem more approachable.

Btw don't expect more than 1 live viewer per stream, this is a niche subject. But you can expect a few hundred views after uploading to youtube, which is pretty amazing.

Please do start a live stream, there needs to be more.
Remember to also upload your content to youtube after, you would be surprised about the great people you meet. The thing with any skill, is to just start and if you persist you will get better. If you don't become good, no one will notice and if you do become good, no one will remember how you started. And if you are critical of yourself, then maybe that is worth challenging.

Setup: It doesn't have to be complicated, we did crazy stuff with setup up OBS on AWS with special mics, it just ended up being annoying and interrupting our coding. There is nothing wrong with starting with just using your laptop mic and Zoom, which can stream to Twitch and then download the video from Twitch after. How about making incremental improvements only if you need to.

Finally, if you just want to ask questions, Zulip is really the best place. People here answer very quickly and are very helpful, you might as well be on a live stream, but better.

[Alok Singh]

https://youtube.com/@therevaloksingh and this motivates me to stream more

[Eric Rodriguez]

^ lol @ Zulip turning that into a mail link

[Julian Berman]

Don't you mean lol@Zulip ? (EDIT: oh fun, so it does check for the TLD somewhere too).

[Bolton Bailey]

I was considering making a video to try to formalize a very nice proof of the fact that the LCM of the first N positive integers is at least 2^n for n > 7 from the note mentioned in this comment. Perhaps this is a good opportunity to turn it into a live stream as well.

[Bolton Bailey]

Do we have a livestream announcement thread?

[Bolton Bailey]

It seems we do! #general > livestream announcement

[Aaron Liu]

I would watch a livestream

[Violeta Hernández]

I'd hang out in chat assuming that I'm awake at that hour

[l1mey]

I'm beginning to livestream lean content to do with verification of compiler optimisations. My schedule is here https://l-m.dev/stream/ and my channel is https://www.twitch.tv/lmdotdev/.