Schedule

Stream: ItaLean 2025

[Pietro Monticone]

Hi everyone, here is our tentative schedule for the conference.

Tuesday, December 9

Time	Event
08:30–09:15	Registration & Welcome talk
09:15–10:15	@Leonardo de Moura
10:15–10:45	Coffee break
10:45–11:45	A Practical Introduction to Lean (@Bhavik Mehta)
11:45–12:45	@Alex J. Best
12:45–14:00	Lunch
14:00–14:45	@Vikram Shanker / @Lawrence Wu (llllvvuu)
14:45–15:15	Coffee break
15:15–15:45	Projects organisation
15:45–17:00	Lean installation / GitHub tutorial (@Pietro Monticone, @Lorenzo Luccioli)
15:45–19:00	Project work

Wednesday, December 10

Time	Event
09:00–09:45	Number Theory in Mathlib (@Riccardo Brasca)
09:45–10:30	(Functional) Analysis in Mathlib (@Filippo A. E. Nuccio)
10:30–11:00	Coffee break
11:00–12:00	@Emily Riehl
12:00–12:45	Probability Theory in Mathlib (@Rémy Degenne)
12:45–14:00	Lunch
14:00–14:45	@Alex Kontorovich
14:45–15:15	Coffee break
15:15–19:00	Project work

Thursday, December 11

Time	Event
09:00–09:45	Differential Geometry in Mathlib (@Michael Rothgang)
09:45–10:30	Metaprogramming in Lean (@Damiano Testa)
10:30–11:00	Coffee break
11:00–12:00	@Maryna Viazovska
12:00–12:45	Yann Fleureau, @Jia Li
12:45–14:00	Lunch
14:00–14:45	@Jared Duker Lichtman / @Auguste Poiroux
14:45–15:15	Coffee break
15:15–19:00	Project work

Friday, December 12

Time	Event
09:00–09:45	The Carleson Project (@Michael Rothgang)
09:45–10:30	Formalising Polychromatic Colourings of Integers (@Bhavik Mehta)
10:30–11:00	Coffee break
11:00–12:00	Discussion Panel (@Alex J. Best, @Leonardo de Moura, @Auguste Poiroux, @Emily Riehl, @Simone Severini)
12:00–12:45	The Brownian Motion Project (@Rémy Degenne)
12:45–14:00	Lunch
14:00–14:30	@habemus-papadum
14:30–15:15	@Moritz Firsching
15:15–15:45	Coffee break
15:45–17:00	Project presentations

[Lorenzo Luccioli]

Hi everyone,

If you’re giving a talk or a tutorial and need any adjustments to the timing or day, feel free to let us know here so we can make changes before finalizing the program.

[Pietro Monticone]

The preliminary schedule for ItaLean 2025 is now online https://pitmonticone.github.io/ItaLean2025.

It includes the current draft of the talk programme, tutorials, project-work sessions, and all planned events. Minor adjustments may still happen as we finalise your availability and logistics, but the overall structure is already stable.

If you notice any issue or have comments, feel free to reply here. Thanks!

[Filippo A. E. Nuccio]

Thanks for all your work! :pray:

[Lorenzo Luccioli]

Hi everyone,
we have pushed a small update to the schedule on the website.
If you are giving a talk or a tutorial, please take a quick look at the current version and let us know if the timing still works for you.

Thanks a lot!

[Rémy Degenne]

That does not work for me: I'll have to leave early after lunch on Friday, so I can't give a talk at that time.

[Rémy Degenne]

Perhaps @Bhavik Mehta or @Michael Rothgang would accept to swap with their morning slot?

[Jared Duker Lichtman]

I am also hoping to swap for a morning slot (e.g. @Michael Rothgang ), as I will be speaking remotely from California (PST)

[Michael Rothgang]

I'm happy to swap my slot. I mildly prefer Remy's, as then I won't give two talks on one day.

[Bhavik Mehta]

I'm happy to swap with Jared's slot too

[Pietro Monticone]

Ok, we'll update the website soon. Thanks everyone.

[Riccardo Brasca]

Everything works for me, so if someone wants my slot no problem.

[Lorenzo Luccioli]

We could still move Rémy to the 9:45–10:30 slot and put Jared and Auguste at 9:00–9:45, while keeping Michael on Friday afternoon and Bhavik on Thursday afternoon.

This way Jared would not have to stay up too late.