What was already known
Norm convergence was known. Pointwise results covered special settings, including powers of one transformation and distal systems. The new argument adapts the announced OpenAI triangular-Hilbert-transform breakthrough to the general two-commuting-map problem.
AI involvement
The project records GPT-6 Astra Pro solving the problem after being asked to adapt a specific OpenAI triangular-Hilbert-transform result. Claude Opus 5.5 generated the Lean proof, with Codex cleanup. Floris van Doorn, Polona Durcik, Lenka Slavíková, Joris Roos and Christoph Thiele selected the problem/approach and authored the statement; task-only autonomy is not established.
Importance
Resolves the stated general pointwise-convergence problem, beyond the earlier special cases.
Limitations
The original research date is not separately documented; the statement and checking record were registered on 18 October. The blueprint and proof are model-generated; the human authors supplied the formal statement and problem/approach. Guo, Xiao and Zhang subsequently give another AI-assisted proof of the same theorem, not a check or explanation of this argument.
Technical verification
Palomar reports protected statement comparison and Lean, NanoDa and con-ron kernel acceptance on 18 October 2026. The compared theorem uses Mathlib probability, measure-preserving maps and Lp definitions; no mixing or invertibility hypothesis is added.
Formal checking
Palomar reports protected statement comparison and Lean, NanoDa and con-ron kernel acceptance on 18 October 2026. The compared theorem uses Mathlib probability, measure-preserving maps and Lp definitions; no mixing or invertibility hypothesis is added.
- Checker
- Palomar: Lean, NanoDa and con-ron
- Scope
- Almost-everywhere convergence of N^-1 sum_{n<N} f(T^n x)g(S^n x) for commuting measure-preserving maps of a probability space, p,q in [1,infinity] and 1/p+1/q<=1; only the three standard Lean axioms.
- Basis
- Reported by the linked checker
- Check date
- 2026-10-18
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The project identifies the human-authored statement, but no named human account explaining the model-generated central proof was established. Few is the documentation default; the later separate proof does not explain this proof.
Correction and publication history
Added the sourced contribution with its stated hypotheses, AI role, prior work and checking limits.
Read this published revision