## Stream: general

### Topic: Lean Together 2021

#### Rob Lewis (Nov 02 2020 at 21:11):

In January 2020 and 2019 we had Lean user meetings. Who says we can't repeat it in pandemic times? @Patrick Massot and I are planning an online Lean Together 2021, the week of January 4. The exact dates and format are TBD, but mark that week on your calendars. We'll try to schedule things acceptably for various timezones, possibly starting at different times on different days. It's unlikely to be five full days.

A few preliminary ideas: we'd love to see casual WIP talks from any and everybody who has WIP to share. Anything formalization-related is in scope. I think a big point of these workshops is to get an idea of what other people around the world are working on and to coordinate efforts. We're not only looking for polished conference talks, and we'd like to leave plenty of time for discussion. We'll invite some speakers from outside the Zulip world, and you should feel free to spread this invitation.

Would you/your team/your research group possibly be interested in presenting something that week? Please let us know, either here or privately, with no commitment! Again, we hope for a mix of casual and more formal presentations, expecting more of the former.

#### Rob Lewis (Nov 02 2020 at 21:13):

We'll have a website up soonish. But we wanted to announce early, so you all can think about what you'll present :smile:

#### Rob Lewis (Nov 03 2020 at 14:19):

Here's a stub of a website. Watch there and in this stream for more updates: https://leanprover-community.github.io/lt2021/

#### Yury G. Kudryashov (Nov 03 2020 at 19:09):

I'd like to give a talk about 1 of 2 projects (not sure which one will see more progress by New Year): dynamics on the circle and complex analysis.

#### Rob Lewis (Nov 04 2020 at 18:16):

Yury G. Kudryashov said:

I'd like to give a talk about 1 of 2 projects (not sure which one will see more progress by New Year): dynamics on the circle and complex analysis.

Exciting! It'll be great to hear about either one.

#### Rob Lewis (Nov 19 2020 at 18:17):

A reminder to everyone, Lean Together 2021 is still in the works, and we'll get some more official info out before too long! But again, if you're at all interested in presenting something, please let us know. Informal WIP is not only okay, it's welcome and expected.

#### Jannis Limperg (Nov 19 2020 at 18:35):

I can talk briefly about the new induction tactic (PR now underway).

#### Rob Lewis (Nov 19 2020 at 18:35):

That would be awesome!

#### Rob Lewis (Nov 25 2020 at 17:42):

Rob Lewis said:

Here's a stub of a website. Watch there and in this stream for more updates: https://leanprover-community.github.io/lt2021/

I've updated the LT2021 site with some more information. The workshop will happen the week of Jan 4, over a number of half-day sessions (with different start times to accommodate various time zones). Please:

• Volunteer to give a talk! Seriously, we'd love to see a short presentation about whatever fun thing you're formalizing at the time. Longer talks are welcome too of course.
• Fill out the registration form. We'll post Zoom links here, but it's nice to brag about a long list of participants.

#### Rob Lewis (Dec 06 2020 at 22:39):

We're considering using gather.town or something similar for social time at LT2021, since big Zoom meetings aren't really great opportunities to chat. Has anyone used tools like this before? Any suggestions or advice?

#### Rob Lewis (Dec 06 2020 at 22:39):

And if anyone would like to test out gather.town, come hang out with me right now at https://gather.town/app/rSiEPSMJAZMtWEhN/lean-test

#### Adam Topaz (Dec 06 2020 at 22:40):

I've used gather town for something hosted by MSRI. It works fairly well imo.

#### Kevin Kappelmann (Dec 06 2020 at 22:43):

I've had way better experience using wonder: https://www.wonder.me/

#### Rob Lewis (Dec 06 2020 at 22:59):

https://www.wonder.me/r?id=73a91efd-9c82-404f-9a89-c90e564072b6

#### Kevin Buzzard (Dec 06 2020 at 23:00):

Does it have sea?

#### Rob Lewis (Dec 06 2020 at 23:00):

It looks way less fun

No map at all

#### Mario Carneiro (Dec 06 2020 at 23:05):

I've used gather, it was pretty ok

#### Mario Carneiro (Dec 06 2020 at 23:06):

it was pretty early in the pandemic so it was kind of a rush job at the time for the conference, but it worked as well as could be expected. I had difficulty finding people online but that's not the platform's fault

#### Kevin Buzzard (Dec 06 2020 at 23:10):

I was at the beach

#### Kevin Buzzard (Dec 06 2020 at 23:10):

there are loads of places to hide in gather

#### Rob Lewis (Dec 06 2020 at 23:13):

Kevin Kappelmann said:

I've had way better experience using wonder: https://www.wonder.me/

What did you prefer about wonder?

#### Rob Lewis (Dec 06 2020 at 23:13):

We just tried out both, they seemed roughly equivalent but gather has lots of gadgets and fun maps.

#### Rob Lewis (Dec 06 2020 at 23:14):

But that's a very superficial impression.

#### Chris B (Dec 06 2020 at 23:25):

Apparently it's free for now. https://support.wonder.me/hc/en-us/articles/360013620818-What-is-the-pricing-of-Wonder-

Oh, nice, thanks

#### Rob Lewis (Dec 06 2020 at 23:25):

That could be the deciding factor!

#### Kevin Buzzard (Dec 06 2020 at 23:28):

Oh @Chris B it was you at Gather! Hi!

#### Chris B (Dec 06 2020 at 23:33):

Yep. It was nice meeting you guys lol.

#### Kevin Kappelmann (Dec 07 2020 at 00:51):

Rob Lewis said:

Kevin Kappelmann said:

I've had way better experience using wonder: https://www.wonder.me/

What did you prefer about wonder?

Last time we tried gather.town, connecting to zones took quite some time and the zone management seemed less flexible and intuitive to us (e.g. no visual bubble). The video and sound quality was also better on wonder. But maybe that has improved since then!

I see, thanks!

#### Kevin Buzzard (Dec 07 2020 at 01:26):

Rob, Chris and I found we could position ourselves in such a way that Chris could hear both of us, but I could not hear Rob, so perhaps there is no zone management and it's more like "you can hear someone iff they're at most x spaces from you".

#### Kevin Kappelmann (Dec 07 2020 at 01:43):

oh, that's some surprising behaviour I'd say... ^^
We'll use wonder for a Christmas social next week with quizzes, games, and mingling zones, all running at the same time. I'll let you know if we encounter difficulties :)
One annoying restriction is that there's a 15 people limit on the number of people joining the same circle (not zone, there's no limit on that). See the FAQ.

#### Rob Lewis (Dec 13 2020 at 17:28):

We have a preliminary schedule up now. Still subject to change, of course, but make a note of it.

#### Rob Lewis (Dec 13 2020 at 17:30):

@Kevin Kappelmann Curious to hear how the Christmas social goes. I think we'll use wonder only because we don't fit in the free tier of gather and the functionality seems pretty equivalent. The sprites and maps in gather are fun but not worth figuring out how to pay for it.

#### Rob Lewis (Dec 13 2020 at 17:34):

Rob Lewis said:

We have a preliminary schedule up now. Still subject to change, of course, but make a note of it.

And please register if you haven't already! It's nice to brag later about how many attendees we had. And we'll email you the meeting info.

#### Frédéric Dupuis (Dec 13 2020 at 17:53):

Very nice -- looking forward to i! Just a minor quibble: it's not clear at all what "local" times mean here; in fact I had to look at the CET times to know I was in the "local" timezone!

#### Rob Lewis (Dec 13 2020 at 17:55):

I'll try to clarify.

#### Frédéric Dupuis (Dec 13 2020 at 17:55):

Oh! Yeah, I didn't expect a website to be that smart :-)

#### Rob Lewis (Dec 13 2020 at 17:55):

Thank @Patrick Massot :smile:

#### Mario Carneiro (Dec 13 2020 at 17:55):

Can you replace "local" with the designator for the local timezone?

#### Rob Lewis (Dec 13 2020 at 18:07):

If one wanted to figure out the javascript to do so, sure. It's not at the top of my to-do list though.

#### Kevin Buzzard (Dec 13 2020 at 18:28):

The same happened to me BTW

#### Damiano Testa (Dec 13 2020 at 18:31):

According to the second answer in https://stackoverflow.com/questions/1091372/getting-the-clients-timezone-offset-in-javascript, the code is

console.log(Intl.DateTimeFormat().resolvedOptions().timeZone)


I tested it and it works for me...

#### Mario Carneiro (Dec 13 2020 at 18:42):

I think you have to use something like https://momentjs.com/timezone/ to get the timezone abbreviation like EST or CET, but if you want America/New_York style you can use what @Damiano Testa posted, and GMT+n is also available in vanilla js

#### Patrick Massot (Dec 13 2020 at 21:01):

I think we now have enough evidence that this trickery is confusing. I put the timezone everywhere but it seems too much.

#### Rob Lewis (Dec 13 2020 at 21:25):

How about a header at the top that says "All times are <timezone>"?

#### Patrick Massot (Dec 13 2020 at 21:30):

I tried that at first but I feared it wouldn't be visible enough.

#### Damiano Testa (Dec 13 2020 at 21:32):

I like the idea of the two timezones: the official one and the one where the browser is. I do have to say that I am not sure that I trust my browser enough to not also double check myself! Having a geographic location mentioned is somewhat reassuring, though.

#### Rob Lewis (Dec 13 2020 at 21:32):

Mario Carneiro said:

I think you have to use something like https://momentjs.com/timezone/ to get the timezone abbreviation like EST or CET, but if you want America/New_York style you can use what Damiano Testa posted, and GMT+n is also available in vanilla js

Then maybe it's worth using this? I agree with you the "(America/New_York time)" everywhere is a little much.

#### Rob Lewis (Dec 13 2020 at 21:33):

Damiano Testa said:

I like the idea of the two timezones: the official one and the one where the browser is. I do have to say that I am not sure that I trust my browser enough to not also double check myself! Having a geographic location mentioned is somewhat reassuring, though.

Yeah, this is why I hard coded the CET times to begin with -- I don't fully trust my browser to get my local time right (or trust myself to have reset my system time if I'm moving around).

#### Rob Lewis (Dec 13 2020 at 21:34):

But if the local time prints the timezone, it's less of an issue.

Agreed!

#### Anatole Dedecker (Dec 13 2020 at 21:34):

Maybe you could put both ? Something like xx:xx local time (yy:yy CET). This way "local time" is easier to understand I think

#### Rob Lewis (Dec 13 2020 at 21:34):

Anatole Dedecker said:

Maybe you could put both ? Something like xx:xx local time (yy:yy CET). This way "local time" is easier to understand I think

This is what it was a couple hours ago and people said it was confusing.

#### Rob Lewis (Dec 13 2020 at 21:37):

All that said, I think any improvement over hard coded CET times, with no local times at all, isn't worth too much time.

#### Anatole Dedecker (Dec 13 2020 at 21:38):

Rob Lewis said:

Anatole Dedecker said:

Maybe you could put both ? Something like xx:xx local time (yy:yy CET). This way "local time" is easier to understand I think

This is what it was a couple hours ago and people said it was confusing.

Oh sorry I didn't see you already said it

#### Kevin Buzzard (Dec 13 2020 at 21:40):

Why not just put the CET times back and leave the local times as they are with the displayed time zones?

#### Jannis Limperg (Dec 13 2020 at 22:05):

Would "xx:yy your local time" instead of "xx:yy local time" be better?

#### Kevin Buzzard (Dec 13 2020 at 22:07):

I think what we have now is excellent for explaining what we mean by local time

#### Mario Carneiro (Dec 13 2020 at 22:08):

How about "xx:yy local" in the box with hover "Your/Country time (GMT+n)", and at the top "All times are in Your/Country time (GMT+n)."

#### Mario Carneiro (Dec 13 2020 at 22:10):

Even if I know it's "your local time", I like the specific reference to a timezone to make sure that the web site has the right idea of what my local time is

#### Rob Lewis (Dec 13 2020 at 23:41):

It's updated. PRs welcome if this isn't to your taste!

#### Alex J. Best (Dec 13 2020 at 23:48):

I think I've said it before here but I'd really recommend checking out using researchseminars.org for conference schedules, it was created by mathematicians and they've thought a lot about all these timezone problems and many more helpful features (one can embed the schedule back in the conference webpage quite easily, people can add the schedule in their (google, ...) calendar, speakers can edit their own title and abstract and change slide links, etc etc).

#### Kevin Buzzard (Dec 13 2020 at 23:59):

+1 to that -- a lot of mathematicians are using that site now (we use it for the London Number Theory Seminar).

#### Kevin Buzzard (Dec 14 2020 at 09:46):

Rob Lewis said:

It's updated. PRs welcome if this isn't to your taste!

Current version is brilliant.

#### Kevin Kappelmann (Dec 17 2020 at 11:01):

Rob Lewis said:

Kevin Kappelmann Curious to hear how the Christmas social goes. I think we'll use wonder only because we don't fit in the free tier of gather and the functionality seems pretty equivalent. The sprites and maps in gather are fun but not worth figuring out how to pay for it.

Besides the Christmas social (17 people), we also used it for another occasion (~25 people). Everything worked very well, the audio & video quality was good. I think it works way better for mingling than having breakout rooms on some video conference system.

There are 2 annoying things:

1. The 15 person/circle limit I mentioned before -- we hit that one once when a guest wanted to show some pictures to everyone. In theory, there's a broadcasting feature, but that's for hosts only. One could send the password to that one guest, but then they need to figure out how to broadcast... and maybe some guests don't want to see the broadcast and continue talking, which is not possible... As you can see, it is not a good solution to circumvent the 15 people/circle restriction.
2. There's a "lock this circle" feature at the top right of the window that some guests used by accident. It might be worth to give everyone a quick tour before sending out the meeting URL.

All in all, I think it works very well, but the 15 people/circle restriction can be annoying. Personally, I think that more than 15 people in one group for mingling doesn't make much sense in most cases anyway, but as noted above, there are some exceptions where it would be useful.

#### Kevin Buzzard (Dec 17 2020 at 11:14):

For the use case I'm envisaging at LT2021 (small chats between people who don't all know each other already) I'm not sure this is going to be a problem -- was the issue that basically at a Christmas social there are a bunch of people you haven't seen for ages who you know white well and a group of 15 can form naturally?

#### Kevin Kappelmann (Dec 17 2020 at 11:19):

In our case, it was a celebration for someone and another person wanted to show some funny pictures about the person to be celebrated. Naturally, everyone was curious and wanted to see them :p
But besides that, circles tended to be ~10 people max and on average ~5-6 people.

#### Kevin Buzzard (Dec 17 2020 at 11:36):

OK so you're saying I shouldn't pull out my funny pictures of Patrick.

#### Kevin Kappelmann (Dec 17 2020 at 12:25):

Only pull them out if your set of morals allows you to live with making 15 people happy but probably way more people disappointed ;p

#### Rob Lewis (Dec 26 2020 at 17:10):

There were some late additions to the program, talks that we wanted to hear but were proposed after we filled all our time slots. So we've added a "prerecorded session." These talks will be available as videos before the workshop starts, for you to watch at your leisure, and the speakers will be available at social hours for informal Q&A sessions.

#### Mohamed Al-Fahim (Dec 27 2020 at 07:40):

Does the RSS feed on https://leanprover-community.github.io/lt2021/schedule.html notify of any changes to the schedule?

#### Patrick Massot (Dec 27 2020 at 10:01):

No. To be honest this feed isn't doing much, it's there by default in Jekyll (the site builder that comes by default with GitHub pages) and we didn't remove it but it's pointless (and it's not even associated to the schedule page, it's global). I think this is meant for blogs. I'll try to see whether I can remove it since it's pointless.

Done.

#### Rob Lewis (Jan 03 2021 at 14:55):

One final reminder: Lean Together 2021 begins tomorrow! There's a stream for discussing the workshop and talks: #Lean Together 2021

#### Rob Lewis (Jan 04 2021 at 12:24):

Rob Lewis said:

One final reminder: Lean Together 2021 begins tomorrow! There's a stream for discussing the workshop and talks: #Lean Together 2021

Bump for anyone logging into Zulip now looking for the meeting info! Things are starting in 1.5 hours.

#### Rob Lewis (Jan 04 2021 at 14:24):

We're not "officially" live streaming this on YouTube. We'll be stopping and restarting the stream after every talk.

#### Rob Lewis (Jan 04 2021 at 14:24):

This is to save us from having to upload local recordings afterward.

#### Rob Lewis (Jan 04 2021 at 14:24):

But you should watch on Zoom if you want seamless live streaming.

#### Gihan Marasingha (Jan 04 2021 at 14:33):

Will the slides be uploaded somewhere?

#### Alex J. Best (Jan 04 2021 at 14:36):

#Lean Together 2021

#### Adam Topaz (Jan 04 2021 at 14:50):

Can someone post the link to the youtube stream.... my zoom seems to be broken atm.

#### Tom Ellis (Jan 04 2021 at 14:51):

But I am at least able to join, grab the link, and leave.

#### Rob Lewis (Jan 04 2021 at 14:51):

Please try to use the dedicated stream for LT2021 discussion:

#Lean Together 2021

#### Rob Lewis (Jan 06 2021 at 15:49):

Rob Lewis said:

Please try to use the dedicated stream for LT2021 discussion:

#Lean Together 2021

I see some people active who are at the workshop but not subscribed to this stream. If you're looking for the LT2021 discussion, subscribe to #Lean Together 2021

#### Rob Lewis (Jan 07 2021 at 12:54):

Starting again in 7 min. One final reminder, subscribe to the #Lean Together 2021 stream if you haven't already.

Last updated: May 14 2021 at 00:42 UTC