This repository contains formalizations for some of the basic Lebesgue space theory of spherical maximal functions with an emphasis on restricted dilation sets. It includes in particular a formalization of Bourgain's circular maximal theorem.
Completed:
- Stein's spherical maximal theorems and Bourgain's circular maximal theorem:
Spherical.eLpNorm_sphericalMaximal_le - Lacunary spherical maximal theorem:
Spherical.RestrictedDilations.eLpNorm_lacunarySphericalMaximal_le -
$L^p \to L^p$ bounds for restricted dilation sets: Seeger-Wainger-Wright '08:Spherical.RestrictedDilations.eLpNorm_restrictedSphericalMaximal_le - Power weights, Thm. 1.1 of Fraccaroli-Roos-Seeger '26:
Spherical.PowerWeights.closure_typeSet_eq - Thm. 2 of arXiv:1909.05389 (Sharpness examples for
$L^p$ improving) - Thm. 1 of arXiv:1909.05389 (
$L^p \to L^q$ bounds for fractal dilation sets, non-endpoint range):Spherical.FractalDilations.hasFractalSphericalStrongType_of_mem_Rand its representative-independent formSpherical.FractalDilations.hasFractalSphericalLpExtension_of_mem_R
To build and verify the formalization locally follow these steps:
-
Install Lean 4 following instructions here.
-
Clone this repository using
git clone https://github.com/roos-j/lean-spherical
-
Open the repository folder in VSCode, open a terminal and run
lake exe cache get!
This is not strictly necessary, but will significantly speed up the build process by fetching pre-built dependencies such as Mathlib.
- Open the file
LeanSpherical.leanin VSCode. To verify a theorem move your cursor to the corresponding line, e.g. for Stein's spherical maximal theorem
#print axioms eLpNorm_sphericalMaximal_le
After some time, the Lean InfoView window should then display the message
'Spherical.eLpNorm_sphericalMaximal_le' depends on axioms: [propext, Classical.choice, Quot.sound]
This means that Lean has successfully certified correctness of the theorem assuming only the standard set of axioms.
Alternatively, run
lake build
from the terminal in VSCode.
Almost all of the ~370k lines of code in this project were machine-generated by coding agents, mainly Codex/gpt-5.6-terra-ultra, and Claude/opus-5-high.
This project maintains strict separation of machine-generated code from human-generated code. All machine-generated code is located in the Auto subfolder and lives in the Auto namespace in Lean.
Only the definitions necessary to state the main theorems and the statements of the main theorems were human generated.
These are located in Definitions.lean.
and Theorems.lean, respectively.
The formalization proceeded in several stages. First, Stein's spherical maximal theorem and its necessary prerequisites were formalized. Many of these prerequisites are not currently in Mathlib, though some of them are contained in existing projects such as the Carleson project. These include Marcinkiewicz interpolation, weak (1,1) boundedness of the Hardy-Littlewood maximal function, Fourier decay of the surface measure of the sphere, and other basic things.
The next stage began an attempt to autoformalize arXiv:1909.05389 and successfully finished the lower bounds Thm. 2. The process was paused before Thm. 1 could be finished, but Thm. 1 of arXiv:1909.05389 was completed in a later session with Claude/opus-5.
In the next stage, the main theorem of arXiv:2602.17613 was formalized, with the additional assumption d >= 3. This took a single session with Codex/gpt-5.6-terra-ultra that ran for ~25h.
At this point the formalization had grown to about ~180k lines of code.
In the next stage, Bourgain's circular maximal theorem was formalized. This is a significantly deeper result than anything that had been done so far in this repository. The first step was to generate a blueprint using gpt-5.6-sol-pro. It was given the instructions to follow the standard argument via Mockenhaupt-Seeger-Sogge's local smoothing estimate for the wave equation. It then took several days worth of running Codex/5.6-terra-ultra continuously before the MSS theorem, and Bourgain's theorem were both formalized. Perhaps unsurprisingly, the main bottleneck were the combinatorial Kakeya-type estimates for plates.
In a final stage, the remaining theorems in the repository were also generalized to the planar case. The main obstruction here was the type set characterization theorem of Fraccaroli-Roos-Seeger which relies on an input from an older paper of Duoandikoetxea-Vega that had to be formalized as well to fully finish the planar case. This was done using Claude/opus-5-high and took about 6 hours.
A drawback of autoformalization is that the generated code contains a lot of bloat in the form of unnecessary abstractions, wrappers and redundancies (for example, the repository contains several redundant versions of various interpolation theorems). It is also not written at an appropriate level of generality.
Lean certifies correctness1 of the human-written theorems, so the machine-generated proofs never have to be trusted or reviewed by a human2.
- Many standard theorems in harmonic analysis are contained in the machine-generated code. They should be cleaned up and presented in convenient, reusable form:
- Mikhlin multiplier theorem
- Hardy-Littlewood maximal function
- Rademacher functions / Khinchine's inequality
- Littlewood-Paley theory
- interpolation theorems (several redundant versions currently)
- Stationary phase estimates, surface measure Fourier decay
- Mockenhaupt-Seeger-Sogge local smoothing estimate
- Cotlar-Stein lemma
- Calderon-Vaillancourt theorem
- Hardy-Littlewood-Sobolev inequality
Footnotes
-
Assuming soundness of the Lean 4 kernel, a non-trivial assumption. ↩
-
Within reason. The code still had to be reviewed sufficiently to ensure that coding agents followed instructions and did not attempt to act adverserially, for example by writing adverserial meta programs or otherwise trying to compromise the user's system. The degree to which machine-generated code has to be looked at can be further minimized by relying on a correctness judge like Lean Comparator. ↩