Lean Together 2024

Stream: general

[Rob Lewis]

See the announcement: time for another round of Lean Together! Use this thread for discussion :octopus:

[Kevin Buzzard]

Does Friday 12th clash with one of the community meetings?

[Eric Rodriguez]

maybe that's deliberate?

[Patrick Massot]

Of course this meeting fits nicely into the Lean Together meeting.

[Rob Lewis]

There's now a website live (without much data yet). We'd appreciate help spreading the word outside of Zulip!

[Kevin Buzzard]

I don't see anywhere to register? Is that intentional or am I just being an old fool?

[Rob Lewis]

It was intentional, but I guess it doesn't hurt to create a form now: https://forms.gle/u6UkP925GzeUW88W6 (also on the website)

[Shreyas Srinivas]

I find it weird that I first need to be signed in to Google (i.e. Gmail address) and then enter another email address.

[Shreyas Srinivas]

(deleted)

[Mauricio Collares]

If I understand correctly, you only need to be signed into Google if you want to "save your progress". I was able to submit my form without a Google account. It would be good if there was an option to pre-fill your email address if you're logged in, but adding that in a way that allows users with no Google account to still use the form (as is currently the case) could conceivably be unsupported.

[Newell Jensen]

Will these meetings be recorded for those who can't attend?

[Notification Bot]

A message was moved here from #announce > Lean Together 2024 by Rob Lewis.

[Rob Lewis]

Yes, talks will be recorded (with the speakers' permission).

[Steven Clontz]

(deleted)

[Yury G. Kudryashov]

When should we expect to have a finalized schedule?

[Kevin Buzzard]

When [insert long list of people] have sent their titles in I guess?

[Patrick Massot]

This should be really close to final, but there may be a couple of permutations.

[Kevin Buzzard]

BTW both my phone and my laptop claim that all the times are -5 from the truth (eg it says Patrick starts at 9am). The schedule on researchseminars seems correct (it claims that Patrick starts at 2pm which sounds right for UK time). Is the claim really true that lt2024/schedule.html is displaying times in my local browser time zone?

[Rob Lewis]

I heard another report saying the same. A question for everyone: if you are not in EST, react :thumbs_up: to this message if the times on the workshop website are in your local time zone, and :thumbs_down: if they're not. If the first "Welcome" talk is at 9:00 then it's in EST.

[Rob Lewis]

Okay, clearly this is wrong. I'll look into it asap

[Tomas Skrivan]

This shows in CET but this shows in EST for me.

[Rob Lewis]

I think https://leanprover-community.github.io/lt2024/schedule.html should now be properly localized, could I get another round of :thumbs_up: / :thumbs_down: ?