Lean for the Curious Mathematician

Stream: general

[Johan Commelin]

Hello everyone! The first talk of the workshop will start in twenty minutes. All discussions/questions/announcements for this workshop take place on a dedicated stream: https://leanprover.zulipchat.com/#narrow/stream/238830-Lean-for.20the.20curious.20mathematician.202020

[Colleen Robles]

Are there any "Lean for the Curious Mathematician" type workshops/tutorials scheduled for 2024 in the US?

Why I ask: This summer I supervised a team of six undergraduates working on a Lean-based project ("Automated Theorem Proving and Proof Verification"). It was a great success, and I'm thinking of doing something similar next summer. The question of hosting week-long workshop/tutorial before the program was raised.

So I'm wondering: is something planned in the US for next year? And if not, is there an appetite for such a workshop?

[Johan Commelin]

Hi @Colleen Robles. Last year's LftCM was in the USA: https://icerm.brown.edu/topical_workshops/tw-22-lean/

I don't know of any plans to organise another edition in the USA, but I'm sure there would be appetite.

[Alex Kontorovich]

Hi @Colleen Robles, we ran a mini-workshop at Rutgers last May (with @Heather Macbeth and @Rob Lewis as the featured speakers), and will likely run another one, perhaps slightly bigger, at the end of this year. Please contact me directly if you'd like to be involved...

[Filippo A. E. Nuccio]

Hi @Colleen Robles there will be an edition of LFTCM in March 2024 in Marseille (France) and we hope to have some fundings to help young students. If they have some travel funding (and are willing to come) they can certainly apply; if not, although we cannot promise anything at the moment, their application will be taken into account.

[Jeremy Avigad]

@Colleen Robles I'll add my voice to the chorus by saying that more educational opportunities centered on Lean in the US would be great. Do you know about the NSF's recent "dear colleague letter" for REU sites? https://www.nsf.gov/pubs/2023/nsf23082/nsf23082.jsp

[Kevin Buzzard]

+1 to Jeremy. For some reason Lean is quite Europe-centred and my impression is that there is money and opportunities available from US institutions who would prefer to be funding people at US universities