Open Research Index

Formalization of norm-variation of multiple ergodic averages for commuting transformations

Floris van Doorn, Polona Durcik, Joris Roos, Lenka Slavíková, Christoph Thiele

Palomar Registrypalomar/PALOMAR-2026-09-15-000008Sep 15, 2026math.CAscore 0

This is a Lean 4 formalization of norm-variation of multiple ergodic averages for commuting transformations, including Tao's norm-convergence theorem. At the heart of the argument is an explicit real-variable estimate for twisted multilinear averages. This formalization is based on the blueprint available at arXiv:2608.27321. The statements of the main theorems have been hand-formalized, while the proof was autoformalized during a one-week period using coding agents under human supervision. This produced roughly 107k lines of code (excluding comments and blank lines) and includes proofs of…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-15-000008
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-15-000008/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-15-000008/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'