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

arXiv · 2609.31334

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

View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

math.CA cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

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. 2026-09-25. Formalizing Carleson's Theorem in Lean. https://arxiv.org/abs/2609.31334

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Exceptional sets for length under restricted families of projections onto lines in $\mathbb{R}^3$

It is shown that if $A \subseteq \mathbb{R}^3$ is a Borel set of Hausdorff dimension $\dim A>1$, and if $ρ_θ$ is orthogonal projection to the line spanned by $( \cos θ, \sin θ, 1 )$, then $ρ_θ(A)$ has positive length for all $θ$ outside a set of Hausdorff dimension at most $\frac{3-\dim A}{2}$.

math.CA↗

arXiv2026

Some one-dimensional elliptic problems with constraints

Given $m \in \mathbb{N} \setminus \{0\}$ and $ρ> 0$, we find solutions $(λ,u)$ to the problem \begin{equation*} \begin{cases} \bigl(-\frac{\mathrm{d}^2}{\mathrm{d} x^2}\bigr)^m u + λG'(u) = F'(u)\\ \int_{\mathbb{R}} K(u) \, \mathrm{d}x = ρ\end{cases} \end{equation*} in the following cases: $m=1$ or $2G(s) = K(s) = s^2$. In the former, we follow a bifurcation argument; in the latter, we use variational methods.

math.CA↗

arXiv2026

Besicovitch-Federer projection theorem for measures

In this paper we prove a Besicovitch-Federer type projection theorem for general finite Borel measures in $\mathbb{R}^n$. Assuming only that the conditional measures along typical affine $(n-m)$-planes are purely atomic, we characterize concentration on a purely $m$-unrectifiable set in terms of the singularity of the projected measure and the $μ$-almost everywhere injectivity of typical orthogonal projections. No regularity or absolute-continuity assumption on the projected measures is imposed, and the result is new even for measure of the form $μ=\mathcal H^m\llcorner E$. In this extended version, we further develop applications of the projection theorem to currents. First, we obtain a rectifiability criterion for Radon measures in terms of atomic disintegrations. We then use this criterion to prove that a finite-mass classical Federer-Fleming current satisfying the intrinsic integer-valued push-forward condition is rectifiable, and hence a real flat chain, without assuming any a priori flat-chain or metric-current structure. We also show that a Euclidean metric current is rectifiable whenever its slices are atomic along a set of projections of positive Grassmannian measure, with no assumption on the mass of its boundary. Finally, the projection theorem extends to separable locally compact metric spaces.

math.CA↗