Photo Gallery

Stream: ItaLean 2025

[Pietro Monticone]

This thread is dedicated to sharing photos from the conference. A selection of images has already been published on the conference website, and participants are warmly encouraged to contribute additional photos by posting them here.

[Hang Lu Su]

Here's a picture of one of my favorite slides from the conference.

IMG_3874.HEIC

Edit: I worry I should've included the context. As a newcomer who wants to contribute to mathlib, I'm not sure which type I am yet but we were assured it was one of them, so I will be finding out :joy: .

[Kevin Buzzard]

6 months later we had completed LTE and were featured in Nature :-) Johan Commelin and Adam Topaz took a big gamble, putting aside their original research for 6 months to hack on Scholze's challenge, not knowing whether the mathematical community would even recognise the work, but they believed in Leo's vision.

[Kevin Buzzard]

I think this was a turning point -- I don't think it was immediately clear to people in the CS community in early 2021 that the mathematicians using Lean were doing anything different to anything else happening in any other formal mathematics communities. But we were targetting mathematics which the math experts were currently thinking about and this turned out to make a big difference.