Discussion: Carleson project

Stream: general

[Floris van Doorn]

This is a discussion thread for the Carleson project for everyone not in the #Carleson channel.

[Floris van Doorn]

The announcement is here: #announce > Carleson project

[Floris van Doorn]

An article about this project also appeared in the German popular science magazine Spektrum: https://www.spektrum.de/news/so-veraendern-computer-ki-und-beweispruefer-die-mathematik/2280992 (unfortunately behind a paywall)

[Henrik Böving]

Neben den ZFC-Axiomen gibt es auch andere Grundregeln, die als Fundament der Mathematik dienen können. Das Computerprogramm Lean fußt zum Beispiel auf der Homotopic Type Theory

They wrongly claim we are HoTT based

[Floris van Doorn]

Yeah, I also noticed that error. I did mention during the interview that the foundation of Lean was similar to HoTT, which the interviewer had already heard about. So I guess that's how it slipped in.

[Ruben Van de Velde]

How much are you planning to upstream?

[Floris van Doorn]

The ToMathlib folder contains ~10k (out of ~35k) lines of code, so approximately that much.
Upstreaming discussion is happening here: #Carleson > Porting to Mathlib

[Jakob von Raumer]

Floris van Doorn said:

An article about this project also appeared in the German popular science magazine Spektrum: https://www.spektrum.de/news/so-veraendern-computer-ki-und-beweispruefer-die-mathematik/2280992 (unfortunately behind a paywall)

For ze Germans who don't remember how to tear down walls: https://archive.is/AkjaJ

[Filippo A. E. Nuccio]

Jakob von Raumer said:

Floris van Doorn said:

An article about this project also appeared in the German popular science magazine Spektrum: https://www.spektrum.de/news/so-veraendern-computer-ki-und-beweispruefer-die-mathematik/2280992 (unfortunately behind a paywall)

For ze Germans who don't remember how to tear down walls: https://archive.is/AkjaJ

Danke!

[Jeremy Tan]

@Floris van Doorn I think you promised to include all of the authors of the blueprint paper in the other paper? (The other authors, including me, are not listed on https://arxiv.org/pdf/2508.05563)

[Kim Morrison]

Congratulations. :-)

So... who is going to start a project that needs the main theorem as a prerequisite? I want to see Mathlib grandchildren in action! :-)

[Floris van Doorn]

Jeremy Tan said:

Floris van Doorn I think you promised to include all of the authors of the blueprint paper in the other paper? (The other authors, including me, are not listed on https://arxiv.org/pdf/2508.05563)

This was never the plan. The plan is to write a paper specifically about the formalization, I'll start coordinating that in a couple of weeks. That paper will have as authors the authors of the formalization.
This paper is about the mathematical result, and only contains the fact that it is formalized as a remark.
I hope that clears things up.

[Jeremy Tan]

:squared_ok: