{"id":"palomar/PALOMAR-2026-10-18-000026","url":"https://github.com/roos-j/lean-twocommuting/tree/5abb8fad6c99fe19850cbdabe3096ed7745dda11","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000026-v1.json","repo":"https://github.com/roos-j/lean-twocommuting","tags":["math.DS","math.CA","msc:37A30","msc:42B20","ergodic-theory","harmonic-analysis","lean"],"score":0,"title":"Pointwise a.e. convergence of ergodic averages with respect to two commuting transformations in Lean","trust":"high","domain":"math.DS","source":"palomar","authors":["Floris van Doorn","Polona Durcik","Joris Roos","Lenka Slavíková","Christoph Thiele"],"reviews":0,"subject":"math.DS","summary":"This is a Lean 4 formalization of the pointwise a.e. convergence theorem for ergodic averages with respect to two commuting transformations. This theorem was proved by GPT 6 Pro when it was instructed to adapt the recent breakthrough on the triangular Hilbert transform made public by OpenAI. The formalization was generated by Claude Opus 5.5 Medium.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-18","reactions":{},"formalized":true,"formalizes":[{"title":"Commuting averages: Proof audit and a self-contained formalization blueprint","identifier":"https://github.com/roos-j/lean-twocommuting/blob/33b69ccacc013c703a151421658187ea4d2029fb/blueprint/commuting_ergodic_blueprint.tex","relationship":"formalizes"},{"title":"Annular variation of the triangular Hilbert transform at the symmetric point","identifier":"OpenAI Math Release preprint, October 5, 2026; https://github.com/openai/math/tree/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Annular-variation-of-the-triangular-Hilbert-transform-at-the-symmetric-point-October-5-2026","relationship":"adapts"}]}