{"id":"palomar/PALOMAR-2026-09-15-000008","url":"https://github.com/roos-j/lean-nct/tree/3e09aa52c478ec69abb02eb250c5e5ed06653c3a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-15-000008-v1.json","repo":"https://github.com/roos-j/lean-nct","tags":["math.CA","math.DS","msc:42B20","msc:42B15","msc:37A30","ergodic-theory","harmonic-analysis","lean-formalization"],"score":0,"title":"Formalization of norm-variation of multiple ergodic averages for commuting transformations","trust":"high","domain":"math.CA","source":"palomar","authors":["Floris van Doorn","Polona Durcik","Joris Roos","Lenka Slavíková","Christoph Thiele"],"reviews":0,"subject":"math.CA","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-15","reactions":{},"formalized":true,"formalizes":[{"title":"A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations","identifier":"arXiv:2608.27321","relationship":"formalizes"}]}