Lean Together 2025

Stream: general

[Riccardo Brasca]

Discussion thread for Lean Together 2025.

[Johan Commelin]

Thanks for organizing this!

Here is the announcement, for those that missed it: #announce > Lean Together 2025

[Rémy Degenne]

@Riccardo Brasca don't forget to add the event here: https://leanprover-community.github.io/events.html

[Riccardo Brasca]

Voilà https://github.com/leanprover-community/leanprover-community.github.io/pull/554

[Riccardo Brasca]

The website is now ready! (mostly empty atm)

[Martin Dvořák]

How should I understand the Level of Lean expertise? If I publish my first Lean paper, does it automatically make me an Expert? Or still Intermediate?

[Riccardo Brasca]

Feel free to answer whatever you find more appropriate

[Martin Dvořák]

Well, I'm asking because I don't know what's appropriate. What did the author of the question have in mind?

[Kevin Buzzard]

Riccardo is the author of the question and you have his answer. As an organizer I would add "it doesn't matter what you choose so toss a coin if you can't figure it out".

[Riccardo Brasca]

Yes, don't spend more than 5 seconds in thinking about it, it's only for statistical purposes.

[Martin Dvořák]

OK, I'm putting Intermediate — I don't think it will disqualify me from giving a talk.

[Riccardo Brasca]

surely not!

[Edward van de Meent]

impostor syndrome strikes once again

[Rob Lewis]

Last year, at least one mathlib maintainer and at least one FRO employee put "intermediate"...

[Marcus Rossel]

Should I have received an e-mail after filling out the registration form? I'm not sure if I entered my e-mail address correctly.

[Damiano Testa]

I don't remember receiving an email either after registering.

[Kevin Buzzard]

No, there's no email to send right now because there's no information to give other than what's on the website

[Yury G. Kudryashov]

For those who like I forgot about deadline, it's today.

[Leni Aniva]

When will the decision about who can give a talk be released?

[Riccardo Brasca]

Sorry, we are a little late. We will discuss this tomorrow (not 100% sure we will make a final decision).

[Kevin Buzzard]

Sorry, this is my fault: I've been travelling. I got back to London today.

[Shreyas Srinivas]

What’s the timezone for the times specified in the schedule?

[Jireh Loreaux]

It should be taking your local time zone.

[Shreyas Srinivas]

Thanks

[Kevin Buzzard]

NB there has been a late change to the schedule: Tuesday 1st talk is now Oliver Nash, and Jason Rute is Wed 5th talk -- the online schedule is currently correct.

[Abderrahim Adrabi]

Johan Commelin said:

Starting in 15 minutes $+ \varepsilon$

Could you please send the link? Thanks!

[Johan Commelin]

@Abderrahim Adrabi See #Lean Together 2025 > channel events

[Ching-Tsun Chou]

When will the video recordings appear on YouTube? Thanks!

[Jireh Loreaux]

There may be some small amount of work we need to do before uploading, but we will try to do it as soon as we can!

[Kevin Buzzard]

Current status: the files are now on my computer but I have to edit one of them and make dinner for my family!

[Ching-Tsun Chou]

Thanks! No hurry.

[Greg Shuflin]

huh I just learned this is happening. looks like all the talks are happening in the extreme early morning in pacific time :3

[Notification Bot]

A message was moved here from #announce > Lean Together 2025 by Kevin Buzzard.

[Kevin Buzzard]

@Greg Shuflin The talks are at varying start times throughout the week; Wednesday is not great for you for the first few talks but Thursday the talks are 8am-1pm Pacific time and Friday 7am-10:30, hopefully that's not too extreme for you! It's hard to please all of the people all of the time unfortunately; Thursday doesn't finish until 9pm for me and then I have to upload the videos to YouTube!

[Greg Shuflin]

ah yeah the next several days are better. I just learned this was happening adn was looking at the schedule and saw activity very early in the morning my time. can't do anything about the fact that the earth is spinning and different people live on different parts of it!