## Stream: maths

### Topic: Lean for the curious mathematician

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

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.

I'll be there!

#### Kevin Buzzard (Jan 28 2020 at 12:24):

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

#### Johan Commelin (Jan 28 2020 at 12:25):

I'll be there!

Awesome! I was counting on you (-;

#### Johan Commelin (Jan 28 2020 at 12:27):

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

#### 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!

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

#### Johan Commelin (Jan 28 2020 at 16:07):

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

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

@James Palmer

#### 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!

#### Jasmin Blanchette (Feb 07 2020 at 12:10):

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

#### Johan Commelin (Feb 07 2020 at 19:04):

Cool! Thanks for signing up!

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

:-(

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

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

#### Kevin Buzzard (May 11 2020 at 19:28):

Web talks would be cool

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

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

#### 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

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

#### Patrick Massot (May 11 2020 at 20:52):

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

#### 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?)

#### 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

#### Kevin Buzzard (May 11 2020 at 22:31):

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

#### Aniruddh Agarwal (May 11 2020 at 23:04):

I would like to express interest in this as well.

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

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

#### Johan Commelin (May 13 2020 at 15:35):

Yup, that's true.

#### Johan Commelin (May 13 2020 at 15:35):

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

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

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

#### 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?

#### Kevin Buzzard (May 13 2020 at 15:43):

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

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

#### Kevin Buzzard (May 13 2020 at 15:44):

You can live stream on discord you know

#### Johan Commelin (May 13 2020 at 15:44):

Ooh, I didn't know.

#### Kevin Buzzard (May 13 2020 at 15:45):

@Kenny Lau is this limited to 9 people?

#### Kenny Lau (May 13 2020 at 15:45):

where did you get that number from

#### Kevin Buzzard (May 13 2020 at 15:45):

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

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

#### 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

I don't know

We can try (-;

#### Kevin Buzzard (May 13 2020 at 15:49):

I'll find out by 28th June

#### Bhavik Mehta (May 13 2020 at 15:49):

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

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

#### Kenny Lau (May 13 2020 at 15:50):

that's the joy of twitch

#### Patrick Massot (May 13 2020 at 15:52):

I think I can help with organization in any case.

#### Bhavik Mehta (May 13 2020 at 15:54):

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

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

#### 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

#### Ryan Lahfa (May 13 2020 at 16:36):

Kevin Buzzard said:

You can live stream on discord you know

It's not super stable

From experience

#### 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

#### 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?

#### Kevin Buzzard (May 13 2020 at 16:38):

Yeah I've used that for Twitch in the past

#### 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

#### Kevin Buzzard (May 13 2020 at 16:40):

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

Indeed

#### 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

#### 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

#### Jalex Stark (May 13 2020 at 16:57):

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

#### Ryan Lahfa (May 13 2020 at 16:57):

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

#### Jalex Stark (May 13 2020 at 16:58):

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

#### Jalex Stark (May 13 2020 at 16:59):

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

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

#### 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 ?

#### Jalex Stark (May 13 2020 at 17:00):

yes, that's what i use

#### Jalex Stark (May 13 2020 at 17:00):

with a wacom intuos pen tablet

Oh nice :)

#### 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

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

#### Jalex Stark (May 13 2020 at 17:03):

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

#### 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

#### Jalex Stark (May 13 2020 at 17:27):

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

#### 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

#### 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

#### Bhavik Mehta (May 13 2020 at 17:29):

Podcast seems to record to a video file

#### 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?

#### Jalex Stark (May 13 2020 at 17:40):

Stream name "Organizing online events"?

Fine with me

#### Mario Carneiro (May 13 2020 at 17:41):

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

#### Mario Carneiro (May 13 2020 at 17:41):

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

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

#### Jalex Stark (May 13 2020 at 17:42):

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

#### Johan Commelin (May 13 2020 at 17:42):

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

#### 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

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

#### Jalex Stark (May 13 2020 at 17:43):

but you are still trying to aim at mathematicians?

#### Johan Commelin (May 13 2020 at 17:44):

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

#### Patrick Massot (May 13 2020 at 17:44):

General discussion about twitch and discord are a different topic

#### Johan Commelin (May 13 2020 at 17:44):

Jalex Stark said:

but you are still trying to aim at mathematicians?

I am...

#### Jalex Stark (May 13 2020 at 17:44):

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

#### Johan Commelin (May 13 2020 at 17:44):

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

#### Patrick Massot (May 13 2020 at 17:44):

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

#### Mario Carneiro (May 13 2020 at 17:44):

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

#### 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 (-;

#### Patrick Massot (May 13 2020 at 17:45):

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

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

#### Johan Commelin (May 13 2020 at 17:46):

Let's move to the stream

#### 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?

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

#### 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)?

#### Johan Commelin (May 14 2020 at 11:00):

Nope, that's no longer necessary.

#### Johan Commelin (May 14 2020 at 11:00):

I'll update the website soon

#### Filippo A. E. Nuccio (May 14 2020 at 11:00):

Ok, great. Thanks, looking forward to it.

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

#### 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

#### Jalex Stark (May 14 2020 at 13:56):

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

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

#### 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

#### Kevin Buzzard (May 14 2020 at 13:57):

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

#### 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

#### Kevin Buzzard (May 14 2020 at 14:06):

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

#### Kevin Buzzard (May 14 2020 at 14:06):

https://discord.com/invite/AnHKcDm

#### Jalex Stark (May 14 2020 at 14:10):

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

2. i don't see a way to look at text chat and the video at the same time

#### 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

#### Ryan Lahfa (May 14 2020 at 14:16):

Jalex Stark said:

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

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

#### 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

#### 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

#### 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

#### 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

#### Jalex Stark (May 14 2020 at 14:21):

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

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

Interesting

#### Jalex Stark (May 14 2020 at 14:25):

is BigBlueButton another software?

#### Shing Tak Lam (May 14 2020 at 14:26):

It's a website (probably has some software)

#### 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

#### Shing Tak Lam (May 14 2020 at 14:27):

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

#### Kevin Buzzard (May 14 2020 at 14:27):

I am apparently kbuzzard on Twitch

#### 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"

#### Kevin Buzzard (May 14 2020 at 14:30):

I want a hour of someone coding slowly??

#### 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

#### 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

#### 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

#### Kevin Buzzard (May 14 2020 at 14:32):

and I did not stay too long

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

#### Johan Commelin (May 14 2020 at 14:35):

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

#### 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

#### 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

#### 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

#### Ryan Lahfa (May 14 2020 at 14:45):

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

#### 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:-)

#### 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?

#### 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

Yes

Is the res OK?

#### Ryan Lahfa (May 14 2020 at 14:48):

It seems a bit small

#### Ryan Lahfa (May 14 2020 at 14:48):

There a lot of space

Yeah

#### Bhavik Mehta (May 14 2020 at 14:48):

Yeah it seems a bit small

#### Ryan Lahfa (May 14 2020 at 14:48):

Screen-Capture_select-area_20200514164826.png

#### 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

#### Kevin Buzzard (May 14 2020 at 14:48):

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

#### 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

#### Shing Tak Lam (May 14 2020 at 14:49):

Are you capturing the screen or the window on OBS?

#### Bhavik Mehta (May 14 2020 at 14:49):

It's at the top now

#### Kevin Buzzard (May 14 2020 at 14:49):

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

#### Ryan Lahfa (May 14 2020 at 14:49):

Also, it's bit blurred

#### Bhavik Mehta (May 14 2020 at 14:49):

But the same size

#### 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

#### Ryan Lahfa (May 14 2020 at 14:50):

yes, it's being resized

#### Kevin Buzzard (May 14 2020 at 14:50):

Am I streaming with 0 issues yet?

#### 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

#### Bhavik Mehta (May 14 2020 at 14:51):

bigger would be nice

#### Ryan Lahfa (May 14 2020 at 14:51):

Kevin Buzzard said:

Am I streaming with 0 issues yet?

not yet

#### Ryan Lahfa (May 14 2020 at 14:51):

it's still not maxed

#### Ryan Lahfa (May 14 2020 at 14:51):

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

#### Ryan Lahfa (May 14 2020 at 14:52):

you maxed vertically

#### Ryan Lahfa (May 14 2020 at 14:52):

you just need to go for the horizontal now

#### Shing Tak Lam (May 14 2020 at 14:52):

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

#### Ryan Lahfa (May 14 2020 at 14:52):

we lost a part of the screen

it's back now

#### Ryan Lahfa (May 14 2020 at 14:53):

but could definitely expand on the horizontal

#### 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?

#### Ryan Lahfa (May 14 2020 at 14:53):

we lost some bottom part

:D @Bhavik Mehta

#### 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"?

#### Ryan Lahfa (May 14 2020 at 14:53):

Screen-Capture_select-area_20200514165338.png

#### 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

#### 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

#### Ryan Lahfa (May 14 2020 at 14:55):

So that stuff gets clipped when you resize it

#### 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

#### Ryan Lahfa (May 14 2020 at 14:56):

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

#### 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

#### Ryan Lahfa (May 14 2020 at 14:57):

That might be the culprit

#### Shing Tak Lam (May 14 2020 at 14:57):

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

on what?

OBS

got it

(deleted)

#### Ryan Lahfa (May 14 2020 at 14:59):

perfect @Kevin Buzzard !

#### Ryan Lahfa (May 14 2020 at 14:59):

It's crystal clear

even better

#### Reid Barton (May 14 2020 at 15:24):

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

#### 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

#### Yury G. Kudryashov (Jun 20 2020 at 23:02):

BTW, what are we going to do about timezones?

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

#### 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

#### 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

#### 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?

#### 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/

#### 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