ItaLean discussion thread

Stream: general

[Floris van Doorn]

Discussion thread for #announce > ItaLean 2025: Bridging Formal Mathematics and AI.

The schedule seems really nice!
Are all talks live streamed?
What is the difference between the red and the blue talks?
(@Pietro Monticone)

[Rémy Degenne]

Blue are tutorials

[Rémy Degenne]

They are talks with titles like "Topic X in Lean". Mine is probability in Lean.

[Pietro Monticone]

Thank you, @Floris van Doorn!

All talks will certainly be recorded, but live streaming seems unlikely at the moment.

Regarding the colours on the schedule:

• Red is for research talks (e.g. The Carleson Project).
• ⁠Blue is for tutorial talks (e.g. Differential Geometry in Mathlib).

[Joachim Breitner]

Thanks! What is the address of the venue?

[Eugenio Cainelli]

Joachim Breitner said:

(Someone ought to move this to a discussion topic)

Thanks! What is the address of the venue?

The venue is in Via Filippo Re 10, Bologna

[Pietro Monticone]

Joachim Breitner said:

Thanks! What is the address of the venue?

All logistical details for speakers, participants, and on-site activities will be coordinated in the dedicated private Zulip channel #ItaLean 2025 and, once finalised, published on the website. We have already been working there with the invited speakers and participants will be added shortly.

[Pietro Monticone]

We will likely have limited capacity for remote participation via Zoom. If you are interested in attending the talks, the project-work sessions, or both, please feel free to contact me via DM with your preferred email address. If possible, I will add you to the dedicated channel and to the mailing list.

[Pietro Monticone]

I’ve just added all currently confirmed participants I've found on Zulip to the #ItaLean 2025 channel.

[Fabrizio Montesi]

This really needs the Leaning Pisa tower as logo, or at the very least the Asinelli tower. :⁠-⁠)

[Sidharth Hariharan]

Hi everyone! The Sphere Packing maintainers are thrilled to announce an autoformalisation challenge in partnership with the ItaLean organisers. See the relevant announcement at #announce > ItaLean 2025: Bridging Formal Mathematics and AI @ 💬

[Marijn Stollenga]

Will these talks be recorded and presented online?

[Notification Bot]

A message was moved here from #announce > ItaLean 2025: Bridging Formal Mathematics and AI by Kevin Buzzard.

[Pietro Monticone]

The conference channel #ItaLean 2025 is now public.