Papers With

← All papers
First page of Formalizing Carleson's Theorem in Lean

Formalizing Carleson's Theorem in Lean

Lars Becker, María Inés de Frutos-Fernández, Leo Diedering, Floris van Doorn, Sébastien Gouëzel, Evgenia Karunus, Edward van de Meent, Pietro Monticone, Jasper Mulder-Sohn, Jim Portegies, Joris Roos, Michael Rothgang, James Sundstrom, Jeremy Tan

math.CA Sep 25, 2026 · v1 cs.LO
formalization analysis mathlib
Read PDF arXiv abstract Code
TL;DR
Formalizes Carleson's theorem and its metric-space generalization in Lean via a collaborative blueprint-driven effort building on Mathlib.
Abstract
We present the formalization of Carleson's theorem in the proof assistant Lean. This paper describes the mathematical content, organization of the project, the blueprint, and the main design decisions behind the formalization. It is the result of a large collaborative effort, written and developed in public.
Problem

Carleson's theorem, on almost-everywhere convergence of Fourier series of square-integrable functions, has long, highly technical proofs. No state-of-the-art harmonic analysis result had been formalized in a proof assistant.

Approach

A recent generalization to doubling metric measure spaces (the metric space Carleson theorem) and the deduction of Carleson's original statement were formalized in Lean. A detailed blueprint divided the proof into 179 lemmas, enabling a public collaboration of 28 contributors. Design decisions included making all constants explicit, using finitary arguments in the main proof with limiting steps at the end, and relying on Mathlib's Bochner integral and measure theory.

Results

The metric space Carleson theorem and its deduction of Carleson's theorem were fully formalized. Foundational harmonic analysis results are being submitted to Mathlib, and the explicit-constant approach let the authors improve the constant from 2^{443a^3} to 2^{46a^3}.