Lean for the curious mathematician

Stream: maths

[Johan Commelin]

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.

[Kevin Buzzard]

I'll be there!

[Kevin Buzzard]

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

[Johan Commelin]

I'll be there!

Awesome! I was counting on you (-;

[Johan Commelin]

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

[Rob Lewis]

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

[Yury G. Kudryashov]

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

[Johan Commelin]

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

[Oliver Nash]

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

[Luca Seemungal]

@James Palmer

[Patrick Massot]

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]

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

[Johan Commelin]

Cool! Thanks for signing up!

[Yury G. Kudryashov]

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

[Kevin Buzzard]

:-(

[Alex J. Best]

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

[Yury G. Kudryashov]

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]

Web talks would be cool

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Ryan Lahfa]

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]

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

[Kevin Buzzard]

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

[Aniruddh Agarwal]

I would like to express interest in this as well.

[Johan Commelin]

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.

2. 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]

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]

Yup, that's true.

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

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]

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

[Johan Commelin]

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]

You can live stream on discord you know

[Johan Commelin]

Ooh, I didn't know.

[Kevin Buzzard]

@Kenny Lau is this limited to 9 people?

[Kenny Lau]

where did you get that number from

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kevin Buzzard]

"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

[Kenny Lau]

I don't know

[Johan Commelin]

We can try (-;

[Kevin Buzzard]

I'll find out by 28th June

[Bhavik Mehta]

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

[Kevin Buzzard]

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]

that's the joy of twitch

[Patrick Massot]

I think I can help with organization in any case.

[Bhavik Mehta]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

Kevin Buzzard said:

You can live stream on discord you know

It's not super stable

[Ryan Lahfa]

From experience

[Ryan Lahfa]

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]

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]

Yeah I've used that for Twitch in the past

[Ryan Lahfa]

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]

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

[Ryan Lahfa]

Indeed

[Jalex Stark]

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

0. I used "StreamLabs OBS" which is free and has windows and Mac versions, idk how easy it is to install on linux.
1. 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.
2. 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
3. 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]

Jalex Stark said:

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

0. I used "StreamLabs OBS" which is free and has windows and Mac versions, idk how easy it is to install on linux.
1. 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.
2. 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
3. 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]

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

[Ryan Lahfa]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Ryan Lahfa]

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]

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]

yes, that's what i use

[Jalex Stark]

with a wacom intuos pen tablet

[Ryan Lahfa]

Oh nice :)

[Jalex Stark]

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]

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]

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

[Bhavik Mehta]

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]

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

[Jalex Stark]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

Podcast seems to record to a video file

[Johan Commelin]

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

[Jalex Stark]

Stream name "Organizing online events"?

[Johan Commelin]

Fine with me

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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]

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

[Johan Commelin]

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

[Jalex Stark]

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]

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

[Jalex Stark]

but you are still trying to aim at mathematicians?

[Johan Commelin]

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

[Patrick Massot]

General discussion about twitch and discord are a different topic

[Johan Commelin]

Jalex Stark said:

but you are still trying to aim at mathematicians?

I am...

[Jalex Stark]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

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]

Let's move to the stream

[Filippo A. E. Nuccio]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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]

Nope, that's no longer necessary.

[Johan Commelin]

I'll update the website soon

[Filippo A. E. Nuccio]

Ok, great. Thanks, looking forward to it.

[Johan Commelin]

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]

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]

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

[Ryan Lahfa]

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]

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

[Kevin Buzzard]

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

[Ryan Lahfa]

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]

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

[Kevin Buzzard]

https://discord.com/invite/AnHKcDm

[Jalex Stark]

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

[Jalex Stark]

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]

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

[Ryan Lahfa]

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]

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]

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]

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]

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

[Shing Tak Lam]

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.

[Kevin Buzzard]

Interesting

[Jalex Stark]

is BigBlueButton another software?

[Shing Tak Lam]

It's a website (probably has some software)

[Jalex Stark]

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]

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

[Kevin Buzzard]

I am apparently kbuzzard on Twitch

[Jalex Stark]

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

[Kevin Buzzard]

I want a hour of someone coding slowly??

[Jalex Stark]

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

[Jalex Stark]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and I did not stay too long

[Jalex Stark]

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

[Johan Commelin]

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

[Jalex Stark]

: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]

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]

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

[Ryan Lahfa]

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

[Ryan Lahfa]

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]

How is the Twitch stream?

https://www.twitch.tv/kbuzzard

Can you see the screen and hear nothing?

[Ryan Lahfa]

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

[Bhavik Mehta]

Yes

[Kevin Buzzard]

Is the res OK?

[Ryan Lahfa]

It seems a bit small

[Ryan Lahfa]

There a lot of space

[Shing Tak Lam]

Yeah

[Bhavik Mehta]

Very readable for me

[Bhavik Mehta]

Yeah it seems a bit small

[Ryan Lahfa]

Screen-Capture_select-area_20200514164826.png

[Shing Tak Lam]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Are you capturing the screen or the window on OBS?

[Bhavik Mehta]

It's at the top now

[Kevin Buzzard]

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

[Ryan Lahfa]

Also, it's bit blurred

[Bhavik Mehta]

But the same size

[Ryan Lahfa]

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]

yes, it's being resized

[Kevin Buzzard]

Am I streaming with 0 issues yet?

[Bhavik Mehta]

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]

bigger would be nice

[Ryan Lahfa]

Kevin Buzzard said:

Am I streaming with 0 issues yet?

not yet

[Ryan Lahfa]

it's still not maxed

[Ryan Lahfa]

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

[Ryan Lahfa]

you maxed vertically

[Ryan Lahfa]

you just need to go for the horizontal now

[Shing Tak Lam]

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

[Ryan Lahfa]

we lost a part of the screen

[Bhavik Mehta]

it's back now

[Ryan Lahfa]

it's super readable now

[Ryan Lahfa]

but could definitely expand on the horizontal

[Bhavik Mehta]

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

[Ryan Lahfa]

we lost some bottom part

[Ryan Lahfa]

:D @Bhavik Mehta

[Kevin Buzzard]

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]

Screen-Capture_select-area_20200514165338.png

[Ryan Lahfa]

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]

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

[Ryan Lahfa]

So that stuff gets clipped when you resize it

[Ryan Lahfa]

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]

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

[Kevin Buzzard]

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

[Ryan Lahfa]

That might be the culprit

[Shing Tak Lam]

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

[Kevin Buzzard]

on what?

[Shing Tak Lam]

OBS

[Kevin Buzzard]

got it

[Ryan Lahfa]

(deleted)

[Ryan Lahfa]

perfect @Kevin Buzzard !

[Ryan Lahfa]

It's crystal clear

[Bhavik Mehta]

even better

[Reid Barton]

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

[Antoine Chambert-Loir]

@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]

BTW, what are we going to do about timezones?

[Jalex Stark]

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.

[Mario Carneiro]

We could livestream on youtube

[Jalex Stark]

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

[Mario Carneiro]

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

[Patrick Massot]

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]

@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]

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