Lean Together 2021

Stream: general

[Rob Lewis]

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]

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]

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]

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]

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]

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]

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

[Rob Lewis]

That would be awesome!

[Rob Lewis]

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]

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]

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]

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

[Kevin Kappelmann]

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

[Rob Lewis]

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

[Kevin Buzzard]

Does it have sea?

[Rob Lewis]

It looks way less fun

[Rob Lewis]

No map at all

[Mario Carneiro]

I've used gather, it was pretty ok

[Mario Carneiro]

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]

I was at the beach

[Kevin Buzzard]

there are loads of places to hide in gather

[Rob Lewis]

Kevin Kappelmann said:

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

What did you prefer about wonder?

[Rob Lewis]

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

[Rob Lewis]

But that's a very superficial impression.

[Kevin Buzzard]

i see on the home page of wonder that we could have made "zones" somehow

[Rob Lewis]

I see nothing on the home page of wonder about pricing or time/user limits.

[Chris B]

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

[Rob Lewis]

Oh, nice, thanks

[Rob Lewis]

That could be the deciding factor!

[Kevin Buzzard]

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

[Chris B]

Yep. It was nice meeting you guys lol.

[Kevin Kappelmann]

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!

[Rob Lewis]

I see, thanks!

[Kevin Buzzard]

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]

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]

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

[Rob Lewis]

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

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]

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]

"Local" is whatever your browser thinks is your local timezone.

[Rob Lewis]

I'll try to clarify.

[Frédéric Dupuis]

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

[Rob Lewis]

Thank @Patrick Massot :smile:

[Mario Carneiro]

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

[Rob Lewis]

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]

The same happened to me BTW

[Damiano Testa]

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]

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]

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

[Rob Lewis]

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

[Patrick Massot]

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

[Damiano Testa]

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]

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]

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]

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

[Damiano Testa]

Agreed!

[Anatole Dedecker]

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]

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]

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]

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]

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

[Jannis Limperg]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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]

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

[Alex J. Best]

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]

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

[Kevin Buzzard]

Rob Lewis said:

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

Current version is brilliant.

[Kevin Kappelmann]

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]

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]

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]

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

[Kevin Kappelmann]

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]

A post-Christmas reminder, please register for this if you haven't already.

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]

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

[Patrick Massot]

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.

[Patrick Massot]

Done.

[Rob Lewis]

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

[Rob Lewis]

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.

[Huỳnh Trần Khanh]

The YouTube stream broke :/

[Thomas Browning]

Does this link work: https://www.youtube.com/watch?v=yH3-zE0bYCU

[Rob Lewis]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Gihan Marasingha]

Will the slides be uploaded somewhere?

[Kevin Buzzard]

Floris already uploaded his in the stream I think

[Alex J. Best]

#Lean Together 2021

[Adam Topaz]

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

[Tom Ellis]

@Adam Topaz https://www.youtube.com/watch?v=DYhR5dIEbJ4 I am also having problems with Zoom

[Tom Ellis]

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

[Rob Lewis]

Please try to use the dedicated stream for LT2021 discussion:

#Lean Together 2021

[Rob Lewis]

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]

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