Carleson at HIM

Stream: Carleson

[Kim Morrison]

I heard that Christoph Thiel spoke (enthusiastically!) about the Carleson project while making the opening remarks for this week's HIM workshop.

As Johan said to me earlier today, just a few years ago it's hard to imagine we'd be here now, with this level of enthusiasm about Lean + Mathlib + formalization.

[Floris van Doorn]

Yes, I also heard that from Johan. Unfortunately I didn't attend it myself, since I was at the math department.

Christoph Thiele is pushing this project forward very hard, and it wouldn't be possible without him. He wrote a great and detailed blueprint together with his team, and has been an evangelizer for Lean in Harmonic Analysis circles.

(He also reads a surprising amount of the messages in this stream :wink: )