Norm-variation of multiple ergodic averages, including Tao's norm-convergence theorem, autoformalized in Lean in one week
A Lean 4 proof of about 107,000 lines of a new norm-variation estimate for multiple ergodic averages of commuting transformations, which strengthens Tao's 2008 norm-convergence theorem, was produced by coding agents in one week from a human-written blueprint and hand-formalized statements.
- Lab
- Independent
- Model
- Coding agents, models not stated
- Field
- Mathematics
- Date
- 2026-08-27
- Human collaborators
- Floris van Doorn, Polona Durcik, Joris Roos, Lenka Slavíková, Christoph Thiele
What was found
The companion arXiv paper (2608.27321) is a blueprint for a forthcoming traditional paper by the same authors. It proves r-variation bounds in L^2 for multiple ergodic averages of n commuting measure-preserving transformations, strengthening Tao's norm-convergence theorem and, per its abstract, resolving an open question, through an explicit real-variable estimate for twisted multilinear averages tied to singular Brascamp-Lieb inequalities. In the repository the statements of the three main theorems, nCT.main_ergodic_theorem, nCT.tao_norm_convergence and nCT.main_twisted_theorem, were formalized by hand, and the proofs were autoformalized over one week by coding agents under human supervision, about 107,000 lines excluding comments and blank lines. That includes prerequisites not in Mathlib: multilinear complex interpolation, the Calderón transference principle and properties of Wiener space functions.
Novelty check
The formalized mathematics is the human authors', not the models': the blueprint's abstract attributes the new estimate to the authors and says the formalization was completed largely automatically using frontier large language models. Only the blueprint's abstract, the repository and this registry were checked; no search for earlier formalizations of Tao's theorem was made, and that is the first gap to close. The 2026-09-28 watch run surfaced this through its Palomar registration.
Caveats and known objections
Which models were used is not stated in the repository, the Palomar abstract or the arXiv abstract, which say only coding agents and frontier large language models, and the model field records exactly that. Graded author verified: the statements were formalized by hand by the authors and the proof carries a Palomar registration, but no third party has audited the statements or rebuilt the development. Autonomy is ai-led on the same reading as this registry's Fermat's Last Theorem entry, with the models writing essentially all of the proof code while the humans wrote the blueprint, formalized the statements and supervised; it is not autonomous because the mathematics being formalized is the authors'. The traditional paper the blueprint accompanies had not appeared at entry, and the new estimate is unrefereed.
Machine-checked elsewhere
PalomarPALOMAR-2026-09-15-000008
roos-j/lean-nct at 3e09aa52c478 · checked 2026-09-15
ProvednCT.main_ergodic_theoremnCT.tao_norm_convergencenCT.main_twisted_theorem
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Author verified and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded author verified for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Norm-variation of multiple ergodic averages, including Tao's norm-convergence theorem, autoformalized in Lean in one week. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-08-27-norm-variation-ergodic-averages-leanBibTeX
@misc{whataifound-independent-2026-lean,
title = {Norm-variation of multiple ergodic averages, including Tao's norm-convergence theorem, autoformalized in Lean in one week},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Author verified. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-08-27-norm-variation-ergodic-averages-lean}
}