TY  - RPRT
TI  - Formalizing Carleson's Theorem in Lean
AU  - Lars Becker
AU  - María Inés de Frutos-Fernández
AU  - Leo Diedering
AU  - Floris van Doorn
AU  - Sébastien Gouëzel
AU  - Evgenia Karunus
AU  - Edward van de Meent
AU  - Pietro Monticone
AU  - Jasper Mulder-Sohn
AU  - Jim Portegies
AU  - Joris Roos
AU  - Michael Rothgang
AU  - James Sundstrom
AU  - Jeremy Tan
PY  - 2026
UR  - https://arxiv.org/abs/2609.31334
ID  - 2609.31334
ER  -