Zulip Chat Archive

Stream: general

Topic: Lean Together 2021


view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jannis Limperg (Nov 19 2020 at 18:35):

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

view this post on Zulip Rob Lewis (Nov 19 2020 at 18:35):

That would be awesome!

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Adam Topaz (Dec 06 2020 at 22:40):

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

view this post on Zulip Kevin Kappelmann (Dec 06 2020 at 22:43):

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

view this post on Zulip Rob Lewis (Dec 06 2020 at 22:59):

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

view this post on Zulip Kevin Buzzard (Dec 06 2020 at 23:00):

Does it have sea?

view this post on Zulip Rob Lewis (Dec 06 2020 at 23:00):

It looks way less fun

view this post on Zulip Rob Lewis (Dec 06 2020 at 23:00):

No map at all

view this post on Zulip Mario Carneiro (Dec 06 2020 at 23:05):

I've used gather, it was pretty ok

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 06 2020 at 23:10):

I was at the beach

view this post on Zulip Kevin Buzzard (Dec 06 2020 at 23:10):

there are loads of places to hide in gather

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Dec 06 2020 at 23:14):

But that's a very superficial impression.

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

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

view this post on Zulip Rob Lewis (Dec 06 2020 at 23:16):

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

view this post on Zulip 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-

view this post on Zulip Rob Lewis (Dec 06 2020 at 23:25):

Oh, nice, thanks

view this post on Zulip Rob Lewis (Dec 06 2020 at 23:25):

That could be the deciding factor!

view this post on Zulip Kevin Buzzard (Dec 06 2020 at 23:28):

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

view this post on Zulip Chris B (Dec 06 2020 at 23:33):

Yep. It was nice meeting you guys lol.

view this post on Zulip 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!

view this post on Zulip Rob Lewis (Dec 07 2020 at 01:01):

I see, thanks!

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Rob Lewis (Dec 13 2020 at 17:54):

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

view this post on Zulip Rob Lewis (Dec 13 2020 at 17:55):

I'll try to clarify.

view this post on Zulip Frédéric Dupuis (Dec 13 2020 at 17:55):

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

view this post on Zulip Rob Lewis (Dec 13 2020 at 17:55):

Thank @Patrick Massot :smile:

view this post on Zulip Mario Carneiro (Dec 13 2020 at 17:55):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 13 2020 at 18:28):

The same happened to me BTW

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Dec 13 2020 at 21:25):

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

view this post on Zulip Patrick Massot (Dec 13 2020 at 21:30):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Rob Lewis (Dec 13 2020 at 21:34):

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

view this post on Zulip Damiano Testa (Dec 13 2020 at 21:34):

Agreed!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Jannis Limperg (Dec 13 2020 at 22:05):

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

view this post on Zulip Kevin Buzzard (Dec 13 2020 at 22:07):

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

view this post on Zulip 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)."

view this post on Zulip 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

view this post on Zulip Rob Lewis (Dec 13 2020 at 23:41):

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

view this post on Zulip 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).

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 11:36):

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

view this post on Zulip 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

view this post on Zulip Rob Lewis (Dec 26 2020 at 17:10):

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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Dec 27 2020 at 10:05):

Done.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Huỳnh Trần Khanh (Jan 04 2021 at 14:23):

The YouTube stream broke :/

view this post on Zulip Thomas Browning (Jan 04 2021 at 14:24):

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

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Jan 04 2021 at 14:24):

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

view this post on Zulip Rob Lewis (Jan 04 2021 at 14:24):

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

view this post on Zulip Gihan Marasingha (Jan 04 2021 at 14:33):

Will the slides be uploaded somewhere?

view this post on Zulip Kevin Buzzard (Jan 04 2021 at 14:34):

Floris already uploaded his in the stream I think

view this post on Zulip Alex J. Best (Jan 04 2021 at 14:36):

#Lean Together 2021

view this post on Zulip Adam Topaz (Jan 04 2021 at 14:50):

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

view this post on Zulip Tom Ellis (Jan 04 2021 at 14:50):

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

view this post on Zulip Tom Ellis (Jan 04 2021 at 14:51):

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

view this post on Zulip Rob Lewis (Jan 04 2021 at 14:51):

Please try to use the dedicated stream for LT2021 discussion:

#Lean Together 2021

view this post on Zulip 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

view this post on Zulip 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