Meeting series: What's new in lean?

Stream: lean4

[Mario Carneiro]

The mathlib porting meeting is no more, but it would be nice to use a meeting as a place to talk about what's new in lean more generally and how we are adapting to changes, and looping in more of the FRO team, maybe turning it into something with short presentations/announcements and a lot of time for questions. I'm thinking a once-a-month meeting (right after a new stable?) with short presentations or announcements followed by a lot of time for questions, kind of restarting the public lean 4 dev meetings.

[Mario Carneiro]

cc: @Leonardo de Moura @Sebastian Ullrich @Scott Morrison @Mac Malone

[Patrick Massot]

Indeed I wondered whether the FRO team wanted to setup something like this. Getting the frequency right is slightly tricky since we don't want to consume too many resources preparing such events.

[Mario Carneiro]

Even if the FRO isn't involved I'm willing to keep doing AMA's like in the porting meeting, but indeed the hope is that we can have an actual agenda and some preparation for these meetings, which is why once-a-month sounds about right, longer than that and we'll start to lose track of new things.

[Mario Carneiro]

But I would definitely prefer if they lead it, it makes more sense from an outreach perspective

[Mario Carneiro]

I think we should also include "what's new in major libraries in the lean ecosystem (read: std / mathlib)" things, depending on how much material we end up with

[Mario Carneiro]

as well as new libraries that people want to advertise

[Leonardo de Moura]

@Mario Carneiro This is a great idea. We will restart the monthly meetings + Q&A soon. We will keep you posted.

[Scott Morrison]

We have some more people joining the FRO in October, and so would like to start up the regular monthly meetings "officially" then. If Mathlib wants to get the ball rolling with a meeting in September more specifically about Mathlib/Std, that might be a good idea.

[Johan Commelin]

It does seem challenging to find a time that is somewhat reasonable for USA, EU, and AUS...

[Johan Commelin]

The porting meetings were pretty late for my schedule. But moving them 1hr earlier, or even 30 mins, would mean that Scott has to get out of bed at a really early hour.

[Mario Carneiro]

I was thinking of moving them around to mitigate this effect

[Mario Carneiro]

but this is also hard to put on a calendar