Zulip Chat Archive

Stream: maths

Topic: Lean for the curious mathematician


view this post on Zulip Johan Commelin (Jan 28 2020 at 11:36):

I am organising a Lean workshop in Freiburg (Germany), 13–17 July 2020.
Some of you may have heard of the plans already during the Lean Together meeting in Pittsburgh. I've finally got the organisational hiccups worked out. So, if you are a mathematician, or you know a mathematician who is really interested in learning more about Lean, please let them know about this meeting: https://math.commelin.net/2020/lftcm/

The plan is to have a couple of talks and tutorial sessions, but to also have ~50% of the time dedicated to hackathons and brainstorming sessions, or pair programming. Novices could team up with experts, to see how they go about setting up a theory, etc...

There is limited funding for PhD students and postdocs. Please let me know if you need this.
In general, if you have any questions, please ask.

ping: @Patrick Massot @Kevin Buzzard @Sebastien Gouezel @Rob Lewis @Yury G. Kudryashov @Antoine Chambert-Loir @Vincent Beffara @Scott Morrison and any others I may have forgotten.

view this post on Zulip Kevin Buzzard (Jan 28 2020 at 12:24):

I'll be there!

view this post on Zulip Kevin Buzzard (Jan 28 2020 at 12:24):

Are you interested in UGs or is it PhD and above?

view this post on Zulip Johan Commelin (Jan 28 2020 at 12:25):

I'll be there!

Awesome! I was counting on you (-;

view this post on Zulip Johan Commelin (Jan 28 2020 at 12:27):

More pings: @Alex J. Best @Oliver Nash @Lennard Henze :up: :up:

view this post on Zulip Rob Lewis (Jan 28 2020 at 12:29):

I hope I'll be there, although I can't commit 100% right now. Sounds like a great event!

view this post on Zulip Yury G. Kudryashov (Jan 28 2020 at 16:00):

I'll need a formal invitation letter to apply for a visa. My name is spelled in passport as Iurii Kudriashov.

view this post on Zulip Johan Commelin (Jan 28 2020 at 16:07):

@Yury G. Kudryashov I'll ask (tomorrow) our secretary to write such a letter.

view this post on Zulip Oliver Nash (Jan 28 2020 at 21:11):

@Johan Commelin This sounds superb, I would love to attend. I will first have to check with work and, more importantly, with my wife. I will look into the details soon. Either way, I'm glad it's going ahead.

view this post on Zulip Luca Seemungal (Jan 28 2020 at 22:15):

@James Palmer

view this post on Zulip Patrick Massot (Feb 01 2020 at 15:12):

My attention has been subtly drawn to the fact that I failed to publicly write here: of course I'll go the Johan's workshop!

view this post on Zulip Jasmin Blanchette (Feb 07 2020 at 12:10):

Ah, this was well hidden under #maths. I'm in I guess!

view this post on Zulip Johan Commelin (Feb 07 2020 at 19:04):

Cool! Thanks for signing up!

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 19:05):

Now it's clear that even if borders will open soon, I'll have no time to get a visa before leaving Toronto.

view this post on Zulip Kevin Buzzard (May 11 2020 at 19:09):

:-(

view this post on Zulip Alex J. Best (May 11 2020 at 19:10):

Is this still running? I sortof figured it was cancelled like most other events this summer.

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 19:15):

I don't know whether it was cancelled but I'm sure that I'm not coming. Though we may have a series of web talks.

view this post on Zulip Kevin Buzzard (May 11 2020 at 19:28):

Web talks would be cool

view this post on Zulip Johan Commelin (May 11 2020 at 20:20):

My fear is that this won't be a physical meeting. I'll look into an online format this week.

view this post on Zulip Johan Commelin (May 11 2020 at 20:21):

But since the plan was just a couple of talks and mostly hackathon, it might not be very different from what we are doing here on Zulip. And the "newbie sits next to expert to gets started" part of the program will go down the drain anyway.

view this post on Zulip Patrick Massot (May 11 2020 at 20:35):

We could have "newbie sits next to expert to gets started" on Discord or Twitch or something like this

view this post on Zulip Johan Commelin (May 11 2020 at 20:39):

I should definitely look into Discord and/or Twitch. We can discuss ideas tomorrow (or later this week).

view this post on Zulip Patrick Massot (May 11 2020 at 20:52):

Of course you should make a new round of announcement if this goes online.

view this post on Zulip Ryan Lahfa (May 11 2020 at 21:46):

I'm still super interested into this and would attend online, I think it makes sense as many seminars are online, it could be announced at http://mathseminars.org/ too (maybe?)

view this post on Zulip Kevin Buzzard (May 11 2020 at 22:31):

You'd be welcome to use my lean discord server. By mid-June I might have got the hang of it

view this post on Zulip Kevin Buzzard (May 11 2020 at 22:31):

The only reason I went for discord is that a lot of undergraduates use it

view this post on Zulip Aniruddh Agarwal (May 11 2020 at 23:04):

I would like to express interest in this as well.

view this post on Zulip Johan Commelin (May 13 2020 at 15:29):

Over the last few days I've thought a bit about this. It's clear that there is sufficient interest in doing something. I see two options:

  1. We turn this into a online workshop.

    • We have several live-streaming sessions via Twitch, where people can see "experts" working with Lean, and demoing how Lean/mathlib works.
    • We can use Discord and/or Zulip to answer questions from newcomers
    • We can advertise this in several places.

If we choose this option, then I cannot organise this alone. I currently do not have enough time to be the only organiser, and also during the week itself, I will need to be offline several moments to supervise my kids with homeschooling etc.
I really like this option, but I would need 2 or 3 coorganisers that have ample experience with lean and/or organising workshops.

  1. I postpone this till a later date, when I have enough time and energy to organise this. Maybe we can then even meet physically.

view this post on Zulip Patrick Massot (May 13 2020 at 15:32):

Options 1 and 2 are not mutually exclusive, right? Option 1 wouldn't cost any money I guess. So you could hopefully spend the money you allocated to this at a later time.

view this post on Zulip Johan Commelin (May 13 2020 at 15:35):

Yup, that's true.

view this post on Zulip Johan Commelin (May 13 2020 at 15:35):

If I don't wait 2 years. Because then the money is gone (-;

view this post on Zulip Kevin Buzzard (May 13 2020 at 15:37):

I am supposed to be running my summer projects but I wonder whether we can somehow integrate everything that week. I can certainly try and help but I have a very busy May and I have committed to doing a lot of things in June to prepare for the summer projects. I am sure I can help somehow though.

view this post on Zulip Patrick Massot (May 13 2020 at 15:38):

I'm not sure there is is so much to do in option 1. And Johan doesn't have to feel in charge. We can simply decide we have a special week, simply making sure we have enough experienced users willing to spend even more time with beginners that week.

view this post on Zulip Johan Commelin (May 13 2020 at 15:43):

Well, it would be good to have some sort of plan. What happens if 50 new people show up with almost no lean experience?

view this post on Zulip Kevin Buzzard (May 13 2020 at 15:43):

Ask me on 1st July and I'll tell you

view this post on Zulip Johan Commelin (May 13 2020 at 15:43):

We should give them some sort of program: at time X:Y you can follow Mario on Twitch. 2 hours later Yury is giving a talk. Etc...

view this post on Zulip Kevin Buzzard (May 13 2020 at 15:44):

You can live stream on discord you know

view this post on Zulip Johan Commelin (May 13 2020 at 15:44):

Ooh, I didn't know.

view this post on Zulip Kevin Buzzard (May 13 2020 at 15:45):

@Kenny Lau is this limited to 9 people?

view this post on Zulip Kenny Lau (May 13 2020 at 15:45):

where did you get that number from

view this post on Zulip Kevin Buzzard (May 13 2020 at 15:45):

https://www.techjunkie.com/enable-screen-share-discord/

view this post on Zulip Kenny Lau (May 13 2020 at 15:46):

Discord allows you and up to nine other people on your server can do live video chat while simultaneously sharing desktops.

view this post on Zulip Kevin Buzzard (May 13 2020 at 15:46):

"Discord allows you and up to nine other people on your server can do live video chat while simultaneously sharing desktops." But I don't know if that means that 100 other people can watch and not share their desktops

view this post on Zulip Kenny Lau (May 13 2020 at 15:46):

I don't know

view this post on Zulip Johan Commelin (May 13 2020 at 15:48):

We can try (-;

view this post on Zulip Kevin Buzzard (May 13 2020 at 15:49):

I'll find out by 28th June

view this post on Zulip Bhavik Mehta (May 13 2020 at 15:49):

I think twitch streaming with questions in discord/zulip/twitch chat would work well

view this post on Zulip Kevin Buzzard (May 13 2020 at 15:50):

Yes I know for sure I can Twitch stream to more than 9 people. I am slightly worried by potential spammy Twitch chat though.

view this post on Zulip Kenny Lau (May 13 2020 at 15:50):

that's the joy of twitch

view this post on Zulip Patrick Massot (May 13 2020 at 15:52):

I think I can help with organization in any case.

view this post on Zulip Bhavik Mehta (May 13 2020 at 15:54):

i'm sure people around here wouldn't mind moderating a little

view this post on Zulip Kevin Buzzard (May 13 2020 at 15:56):

It will just be an experiment; I'm sure we'll find something which works at some point...

view this post on Zulip Mario Carneiro (May 13 2020 at 16:34):

Oh, I'd almost forgot about this workshop, as it seemed like I couldn't go. If it's going online then that changes things. I can join in the festivities, however they end up

view this post on Zulip Ryan Lahfa (May 13 2020 at 16:36):

Kevin Buzzard said:

You can live stream on discord you know

It's not super stable

view this post on Zulip Ryan Lahfa (May 13 2020 at 16:36):

From experience

view this post on Zulip Ryan Lahfa (May 13 2020 at 16:37):

The simplest thing to do IMHO is to use OBS Studio: https://obsproject.com with someone who has a very fast connection to stream to YouTube Live or Twitch or whatever is preferred and do some testing on the setup

view this post on Zulip Ryan Lahfa (May 13 2020 at 16:38):

Kevin Buzzard said:

Yes I know for sure I can Twitch stream to more than 9 people. I am slightly worried by potential spammy Twitch chat though.

Moderation?

view this post on Zulip Kevin Buzzard (May 13 2020 at 16:38):

Yeah I've used that for Twitch in the past

view this post on Zulip Ryan Lahfa (May 13 2020 at 16:40):

We can even hold a "Twitch Plays Natural Number Games" using https://github.com/hzoo/TwitchPlaysX ; I don't guarantee any result beyond stupid stuff happening :D

view this post on Zulip Kevin Buzzard (May 13 2020 at 16:40):

You can pre-prepare answers and then cut and paste, which is annoying

view this post on Zulip Ryan Lahfa (May 13 2020 at 16:40):

Indeed

view this post on Zulip Jalex Stark (May 13 2020 at 16:53):

I just did a twitch stream. Notes for others who want to do this for the first time:

  1. I used "StreamLabs OBS" which is free and has windows and Mac versions, idk how easy it is to install on linux.
  2. It took me about 30 minutes of fiddling with StreamLabs settings before I was ready to go live. There are many tutorial videos on youtube.
  3. It helps to have a second monitor to do the programming on, so you can use your first monitor to watch twitch chat and deal with admin-y things
  4. If you want Twitch to save a recording of the stream, you have to check a box in your settings before you start

view this post on Zulip Ryan Lahfa (May 13 2020 at 16:57):

Jalex Stark said:

I just did a twitch stream. Notes for others who want to do this for the first time:

  1. I used "StreamLabs OBS" which is free and has windows and Mac versions, idk how easy it is to install on linux.
  2. It took me about 30 minutes of fiddling with StreamLabs settings before I was ready to go live. There are many tutorial videos on youtube.
  3. It helps to have a second monitor to do the programming on, so you can use your first monitor to watch twitch chat and deal with admin-y things
  4. If you want Twitch to save a recording of the stream, you have to check a box in your settings before you start

OBS Studio is very very simple to install under Linux, it's in all major distributions

view this post on Zulip Jalex Stark (May 13 2020 at 16:57):

I feel like my de bruijn factor on this stream was like 10

view this post on Zulip Ryan Lahfa (May 13 2020 at 16:57):

  1. can also be replaced by 2 machines, or a phone/tablet

view this post on Zulip Jalex Stark (May 13 2020 at 16:58):

I got through 1a and 1b of this problem set:
https://www.mathcamp.org/2012/quiz/
in about 1h30m

view this post on Zulip Jalex Stark (May 13 2020 at 16:59):

I think next time I will start with walking through the problem on a whiteboard

view this post on Zulip Ryan Lahfa (May 13 2020 at 16:59):

OBS Studio can be fine-tuned depending on your hardware/connection, like if you want to decrease latency (zerolatency mode), or if you want to optimize quality, etc. Some streaming providers also have an option for latency, YT has a super zero latency mode, where it tries to get you as close as you can, during my tests, I could run ~ 30-45 mn stream with ~3-5 seconds of latency with a 1 Gbps/600 Mbps (and 1-5 ms latency) connection over Ethernet.

view this post on Zulip Ryan Lahfa (May 13 2020 at 17:00):

Jalex Stark said:

I think next time I will start with walking through the problem on a whiteboard

Do you know about openboard.ch ?

view this post on Zulip Jalex Stark (May 13 2020 at 17:00):

yes, that's what i use

view this post on Zulip Jalex Stark (May 13 2020 at 17:00):

with a wacom intuos pen tablet

view this post on Zulip Ryan Lahfa (May 13 2020 at 17:00):

Oh nice :)

view this post on Zulip Jalex Stark (May 13 2020 at 17:01):

well I haven't done it in a long time, but when i was in academia i would often have research video calls through it, and then send the pdf to all the participants afterward

view this post on Zulip Ryan Lahfa (May 13 2020 at 17:02):

Also, an alternative would be to use BBB + OBS Studio, I have seen this setup in the wild, I don't how does it compare to the rest, but if someone wants to do test, here's a public instance of BBB: http://ensemble-bbb.scaleway.com/ (some French cloud has done cool stuff for video conferencing capabilities due to COVID)

view this post on Zulip Jalex Stark (May 13 2020 at 17:03):

i had 9 random people wander through, a couple staying long enough to ask questions

view this post on Zulip Bhavik Mehta (May 13 2020 at 17:22):

Is there a specific way to share an openboard with people during a call? I'm currently drawing on onenote and sharing but openboard looks good - it'd be nice to have an option other than screensharing

view this post on Zulip Jalex Stark (May 13 2020 at 17:27):

well most things that offer screenshare have an option to screenshare a specific application

view this post on Zulip Jalex Stark (May 13 2020 at 17:28):

openboard has a "podcast" button, who knows what that does but you may want to play with it

view this post on Zulip Bhavik Mehta (May 13 2020 at 17:29):

Yeah but screenshare comes with quality loss which you don't get with eg zoom whiteboard or onenote

view this post on Zulip Bhavik Mehta (May 13 2020 at 17:29):

Podcast seems to record to a video file

view this post on Zulip Johan Commelin (May 13 2020 at 17:33):

If people like the idea of having an online week "Lean for the curious mathematician", shall we start a new stream?

view this post on Zulip Jalex Stark (May 13 2020 at 17:40):

Stream name "Organizing online events"?

view this post on Zulip Johan Commelin (May 13 2020 at 17:40):

Fine with me

view this post on Zulip Mario Carneiro (May 13 2020 at 17:41):

I think stream name "Lean for the curious mathematician". We have other streams for previous events

view this post on Zulip Mario Carneiro (May 13 2020 at 17:41):

I'm still subscribed to "Lean Together 2019" :)

view this post on Zulip Patrick Massot (May 13 2020 at 17:42):

Ryan Lahfa said:

OBS Studio is very very simple to install under Linux, it's in all major distributions

Indeed you can install it. But then I had a horrible experience trying to use it to record screencast. I'm not really sure but I think it was mostly crashing randomly.

view this post on Zulip Jalex Stark (May 13 2020 at 17:42):

Would "Lean for the curious mathematician 2020" be better?

view this post on Zulip Johan Commelin (May 13 2020 at 17:42):

Ok, maybe rename? @Jalex Stark do you agree?

view this post on Zulip Jalex Stark (May 13 2020 at 17:43):

well i also like the idea of a general stream where people can go to talk about, e.g. how twitch and discord work

view this post on Zulip Patrick Massot (May 13 2020 at 17:43):

At least that was the original title. Of course it's fairly restrictive (many people around here are not mathematicians)

view this post on Zulip Jalex Stark (May 13 2020 at 17:43):

but you are still trying to aim at mathematicians?

view this post on Zulip Johan Commelin (May 13 2020 at 17:44):

That is true, we can just turn it into Lean for the curious

view this post on Zulip Patrick Massot (May 13 2020 at 17:44):

General discussion about twitch and discord are a different topic

view this post on Zulip Johan Commelin (May 13 2020 at 17:44):

Jalex Stark said:

but you are still trying to aim at mathematicians?

I am...

view this post on Zulip Jalex Stark (May 13 2020 at 17:44):

me too, mostly, and I think the event works better if that's the aim

view this post on Zulip Johan Commelin (May 13 2020 at 17:44):

But of course... we offer multiple "tracks"

view this post on Zulip Patrick Massot (May 13 2020 at 17:44):

I have nothing against non-mathemticians, but focus can help sometimes

view this post on Zulip Mario Carneiro (May 13 2020 at 17:44):

You should mention that it's going online on the webpage

view this post on Zulip Johan Commelin (May 13 2020 at 17:45):

I'm also fine with having another week "Lean for the curious computer scientist" two weeks later (-;

view this post on Zulip Patrick Massot (May 13 2020 at 17:45):

Maybe there is a misunderstanding about the word mathematician. Does it include math students?

view this post on Zulip Johan Commelin (May 13 2020 at 17:45):

Yes, the webpage might even move (and I'll add a forwarder). But first we need to think about what exactly we want, and how it will happen.

view this post on Zulip Johan Commelin (May 13 2020 at 17:46):

Let's move to the stream

view this post on Zulip Filippo A. E. Nuccio (May 14 2020 at 10:56):

Hi Johan, what are the plans about the workshop given the pandemic? Are you still holding it in Freiburg?

view this post on Zulip Johan Commelin (May 14 2020 at 10:59):

No, we've just been talking about it the last couple of days. It will probably be online.

view this post on Zulip Johan Commelin (May 14 2020 at 10:59):

See also the new stream: https://leanprover.zulipchat.com/#narrow/stream/238830-Lean-for.20the.20curious.20mathematician.202020

view this post on Zulip Filippo A. E. Nuccio (May 14 2020 at 11:00):

Yes, I am sorry, I have now discovered the whole discussion and I am going through it. Do you still want me to send you an e-mail with details (of course, no funding needed)?

view this post on Zulip Johan Commelin (May 14 2020 at 11:00):

Nope, that's no longer necessary.

view this post on Zulip Johan Commelin (May 14 2020 at 11:00):

I'll update the website soon

view this post on Zulip Filippo A. E. Nuccio (May 14 2020 at 11:00):

Ok, great. Thanks, looking forward to it.

view this post on Zulip Johan Commelin (May 14 2020 at 11:12):

I've just sent an email to everyone who registered before. For details, keep an I on zulip (the stream linked above), and the website.

view this post on Zulip Ryan Lahfa (May 14 2020 at 13:54):

Bhavik Mehta said:

Is there a specific way to share an openboard with people during a call? I'm currently drawing on onenote and sharing but openboard looks good - it'd be nice to have an option other than screensharing

With OBS Studio, you could do this by making the output of OBS Studio a fake window or something like that and ask for conference systems to share the fake window

view this post on Zulip Jalex Stark (May 14 2020 at 13:56):

I don't understand what the intermediate OBS layer is for

view this post on Zulip Ryan Lahfa (May 14 2020 at 13:56):

Patrick Massot said:

Ryan Lahfa said:

OBS Studio is very very simple to install under Linux, it's in all major distributions

Indeed you can install it. But then I had a horrible experience trying to use it to record screencast. I'm not really sure but I think it was mostly crashing randomly.

That sound like a video graphics issue but that's an horrible experience for anything that wants to do more than just decoding some video using VLC if you're using nVidia (proprietary or nouveau open source driver), and i915 / Intel open source driver had recent serious issues in kernel ≥5.3,<5.6, AMD is another difficult subject depending on whatever you run old hardware (tough luck) or newer hardware (open source drivers by AMD)

view this post on Zulip Jalex Stark (May 14 2020 at 13:57):

zoom and google hangouts both give me an option to pick a specific application when I tell it to screenshare

view this post on Zulip Kevin Buzzard (May 14 2020 at 13:57):

I'm screen sharing on discord right now, just to see if it works

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:00):

Jalex Stark said:

I don't understand what the intermediate OBS layer is for

On Linux, depending on your window manager, on your exact setup, some apps don't pick up the right windows, OBS Studio is rather here to consolidate everything you want for, you can throw dynamic stuff too using the JavaScript feature (for showing chat on the screen or whatever), it really depends in the end of how it's going to look like

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:06):

I didn't need any additional software to stream on discord

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:06):

https://discord.com/invite/AnHKcDm

view this post on Zulip Jalex Stark (May 14 2020 at 14:10):

Cool! it seems a little bit worse than twitch streaming in that

  1. i had to click or type things like 10 times after opening your link before seeing your video
  2. i don't see a way to look at text chat and the video at the same time

view this post on Zulip Jalex Stark (May 14 2020 at 14:11):

I guess discord > twitch for a "classroom" setting, where the above problems aren't important, and it's valuable to let participants say stuff over audio

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:16):

Jalex Stark said:

Cool! it seems a little bit worse than twitch streaming in that

  1. i had to click or type things like 10 times after opening your link before seeing your video
  2. i don't see a way to look at text chat and the video at the same time
  1. are you on browser/"native" app?
  2. you can click to have the reduced button in the bottom right, that'll create another window and then you can arrange the Discord chat & the stream

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:17):

Jalex Stark said:

I guess discord > twitch for a "classroom" setting, where the above problems aren't important, and it's avluable to let participants say stuff over audio

depends on the level of interaction

view this post on Zulip Jalex Stark (May 14 2020 at 14:17):

A general streaming note:
text is harder to read for viewers than for you, you should probably turn your font size up a notch or two when starting a stream

view this post on Zulip Jalex Stark (May 14 2020 at 14:19):

right, if i were giving the sort of lecture that i would give to an audience of 30 undergrads, the point at which everyone is too timid to ask a question unless they're sure it's good, I would say twitch it obviously better

view this post on Zulip Jalex Stark (May 14 2020 at 14:20):

also if you're trying to reach 30 people, then the trivial inconveniences that they face on discord but not twitch means that you'll miss at least one or two of them

view this post on Zulip Jalex Stark (May 14 2020 at 14:21):

cf. 9 am vs 10am classes in a university building

view this post on Zulip Shing Tak Lam (May 14 2020 at 14:22):

Jalex Stark said:

I guess discord > twitch for a "classroom" setting, where the above problems aren't important, and it's valuable to let participants say stuff over audio

I've been in a few BigBlueButton sessions, and that seems pretty good for what it's worth.

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:22):

Interesting

view this post on Zulip Jalex Stark (May 14 2020 at 14:25):

is BigBlueButton another software?

view this post on Zulip Shing Tak Lam (May 14 2020 at 14:26):

It's a website (probably has some software)

view this post on Zulip Jalex Stark (May 14 2020 at 14:26):

Here's a topic on twitch v discord : https://leanprover.zulipchat.com/#narrow/stream/238828-Organizing-online.20events/topic/streaming.3A.20twitch.2Fdiscord.2F.3F/near/197562721

view this post on Zulip Shing Tak Lam (May 14 2020 at 14:27):

It has whiteboard with presentations, polling the audience, screen sharing, video, audio and text chat

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:27):

I am apparently kbuzzard on Twitch

view this post on Zulip Jalex Stark (May 14 2020 at 14:29):

i recommend going into your settings and finding the checkbox for "save a video of my stream"

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:30):

I want a hour of someone coding slowly??

view this post on Zulip Jalex Stark (May 14 2020 at 14:30):

I learned about this only after my first stream and I was sad; I had assumed this box was checked by default

view this post on Zulip Jalex Stark (May 14 2020 at 14:31):

kids love to have a twitch stream or video thereof on in the background while doing other stuff, as long as you talk a decent amount

view this post on Zulip Jalex Stark (May 14 2020 at 14:31):

I listen to people play pokemon games while i answer questions on the new members stream or write solutions to kata

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:32):

Oh how interesting. I've watched my kids play but the only pokemon I watched on Twitch was that fish

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:32):

and I did not stay too long

view this post on Zulip Jalex Stark (May 14 2020 at 14:34):

these folks make a decent amount of money posting videos of themselves solving logic puzzles (and, importantly, narrating their thoughts the whole time, and repeating the proofs of well-known sudoku lemmas often, for the benefit of newcomers)
https://www.youtube.com/watch?v=9m9t8ie9-EE

view this post on Zulip Johan Commelin (May 14 2020 at 14:35):

If they did that in lean they would make less mistakes and earn less money :wink:

view this post on Zulip Jalex Stark (May 14 2020 at 14:35):

:slight_smile: They are approximately my model for what my twitch stream should be, and indeed I am not concerned about making any money

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:44):

Shing Tak Lam said:

It's a website (probably has some software)

I mentioned it somewhere on the top, you can try it here : http://ensemble-bbb.scaleway.com/ on a public instance

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:45):

I use it to teach security to software engineering students and it's being widely used in many university/schools in France

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:45):

(in combination with OBS Studio sometimes, because of some exotic requirements)

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:46):

Jalex Stark said:

kids love to have a twitch stream or video thereof on in the background while doing other stuff, as long as you talk a decent amount

I don't do that often but do you think we can then teach Lean and group definition to kids? O:-)

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:47):

How is the Twitch stream?

https://www.twitch.tv/kbuzzard

Can you see the screen and hear nothing?

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:47):

Kevin Buzzard said:

How is the Twitch stream?

https://www.twitch.tv/kbuzzard

Can you see the screen and hear nothing?

I can see the screen

view this post on Zulip Bhavik Mehta (May 14 2020 at 14:47):

Yes

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:48):

Is the res OK?

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:48):

It seems a bit small

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:48):

There a lot of space

view this post on Zulip Shing Tak Lam (May 14 2020 at 14:48):

Yeah

view this post on Zulip Bhavik Mehta (May 14 2020 at 14:48):

Very readable for me

view this post on Zulip Bhavik Mehta (May 14 2020 at 14:48):

Yeah it seems a bit small

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:48):

Screen-Capture_select-area_20200514164826.png

view this post on Zulip Shing Tak Lam (May 14 2020 at 14:48):

There's a scaling issue for me. It's only in the middle of the screen

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:48):

I've just gone up one ctrl-shift-+ unit

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:49):

Shing Tak Lam said:

There's a scaling issue for me. It's only in the middle of the screen

That's my fault. That's what the OBS looks like

view this post on Zulip Shing Tak Lam (May 14 2020 at 14:49):

Are you capturing the screen or the window on OBS?

view this post on Zulip Bhavik Mehta (May 14 2020 at 14:49):

It's at the top now

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:49):

I am using "Window Capture (Xcomposite)" in "Sources"

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:49):

Also, it's bit blurred

view this post on Zulip Bhavik Mehta (May 14 2020 at 14:49):

But the same size

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:50):

Kevin Buzzard said:

I am using "Window Capture (Xcomposite)" in "Sources"

If you put in the top left and then you can resize it I guess

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:50):

yes, it's being resized

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:50):

Am I streaming with 0 issues yet?

view this post on Zulip Bhavik Mehta (May 14 2020 at 14:50):

Jalex Stark said:

kids love to have a twitch stream or video thereof on in the background while doing other stuff, as long as you talk a decent amount

can confirm i sometimes do this

view this post on Zulip Bhavik Mehta (May 14 2020 at 14:51):

bigger would be nice

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:51):

Kevin Buzzard said:

Am I streaming with 0 issues yet?

not yet

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:51):

it's still not maxed

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:51):

it's also somewhat blurred but readable, it can impair readability for the unicode stuff

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:52):

you maxed vertically

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:52):

you just need to go for the horizontal now

view this post on Zulip Shing Tak Lam (May 14 2020 at 14:52):

Yeah, twitch says you're streaming at 1024p60 for me. Which is a weird resolution...

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:52):

we lost a part of the screen

view this post on Zulip Bhavik Mehta (May 14 2020 at 14:52):

it's back now

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:53):

it's super readable now

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:53):

but could definitely expand on the horizontal

view this post on Zulip Bhavik Mehta (May 14 2020 at 14:53):

should one of us start re-streaming kevin's stream so he can see what we see?

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:53):

we lost some bottom part

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:53):

:D @Bhavik Mehta

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:53):

The problem is that now I am not sharing my full VS Code stream. Where are the settings? Why can't I just say "stream this window"?

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:53):

Screen-Capture_select-area_20200514165338.png

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:55):

Kevin Buzzard said:

The problem is that now I am not sharing my full VS Code stream. Where are the settings? Why can't I just say "stream this window"?

You need to deal with placement&resolution at the OBS Studio level

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:55):

Your full VS Code window is streamed, but it seems like your're streaming at a small resolution

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:55):

So that stuff gets clipped when you resize it

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:56):

Either it's a Twitch parameter or when you "started streaming" for OBS Studio, you got this 1024x768 resolution and you need to go higher

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:56):

It might be a limitation of your hardware/bandwidth also though

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:57):

I think the issue was that I set eveything up on one monitor and then wanted to stream with a bigger one

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:57):

That might be the culprit

view this post on Zulip Shing Tak Lam (May 14 2020 at 14:57):

Go to Settings > Video and see what the resolution is like?

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:58):

on what?

view this post on Zulip Shing Tak Lam (May 14 2020 at 14:58):

OBS

view this post on Zulip Kevin Buzzard (May 14 2020 at 14:58):

got it

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:58):

(deleted)

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:59):

perfect @Kevin Buzzard !

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:59):

It's crystal clear

view this post on Zulip Bhavik Mehta (May 14 2020 at 15:01):

even better

view this post on Zulip Reid Barton (May 14 2020 at 15:24):

There's still a buzzing/clicking sound but it's quiet

view this post on Zulip Antoine Chambert-Loir (Jun 20 2020 at 22:56):

@Johan Commelin Hello. I had planned to participate this meeting but have't been able to work on this for the past 6 months. In any case, I have freed this week for this although I don't have a feeling of how it is possible to have such a week online. Best wishes. Antoine

view this post on Zulip Yury G. Kudryashov (Jun 20 2020 at 23:02):

BTW, what are we going to do about timezones?

view this post on Zulip Jalex Stark (Jun 20 2020 at 23:52):

There's some talk about this here. I think the plan is to have a Europe-centric notion of "morning" and "afternoon" sessions. People in the americas could come to the afternoon sessions without much trouble. People in east easia could come to the morning sessions without much trouble. We should strive to have recordings of lectures available immediately after the session, for the benefit of people in non-european timezones. Twitch does this automatically for kevin's content there.

view this post on Zulip Mario Carneiro (Jun 20 2020 at 23:54):

We could livestream on youtube

view this post on Zulip Jalex Stark (Jun 20 2020 at 23:55):

I watched someone's thesis as a livestream on youtube, seemed like it was easy and well-suited to our purposes

view this post on Zulip Mario Carneiro (Jun 20 2020 at 23:56):

At PLDI they had many 7+ hour livestreams. I think they used a big zoom call to multiplex all the talks together

view this post on Zulip Patrick Massot (Jun 29 2020 at 12:42):

Antoine Chambert-Loir said:

Johan Commelin Hello. I had planned to participate this meeting but have't been able to work on this for the past 6 months. In any case, I have freed this week for this although I don't have a feeling of how it is possible to have such a week online. Best wishes. Antoine

Antoine, did you see that we now have information about how it will happen online?

view this post on Zulip Johan Commelin (Jul 06 2020 at 06:01):

@Aaron Anderson @Patrick Stevens @Paul van Wamelen @Kyle Miller
You've all been making PRs to mathlib recently. Are you aware of this workshop that takes place next week? For more information, see here: https://leanprover-community.github.io/lftcm2020/

view this post on Zulip Aaron Anderson (Jul 06 2020 at 15:28):

I am aware, but I don’t think I can make it from this timezone.


Last updated: May 10 2021 at 07:15 UTC