Formally verified AI-led

Pointwise convergence of ergodic averages along two commuting transformations

A Lean-checked proof that for two commuting measure-preserving transformations $T$ and $S$ of a probability space, the averages $N^{-1}\sum_{n<N} f(T^n x)\, g(S^n x)$ converge almost everywhere whenever $f \in L^p$ and $g \in L^q$ with $1/p + 1/q \le 1$ , found by a model asked to adapt OpenAI's recent triangular Hilbert transform result.

Lab: Independent
Model: GPT-6 Astra Pro (proof and blueprint); Claude Opus 5.5 (Lean formalization)
Field: Mathematics
Date: 2026-10-18
Human collaborators: Floris van Doorn, Polona Durcik, Joris Roos, Lenka Slavíková, Christoph Thiele

Sources

Original work

GitHubroos-j/lean-twocommuting, the Lean formalization↗arXivPointwise convergence of bilinear ergodic averages for commuting transformations (Guo, Xiao and Zhang)↗

What was found

Norm convergence of these bilinear averages has been known since Conze and Lesigne in the 1980s. Pointwise convergence was known when one transformation is a power of the other, by Bourgain's double recurrence theorem, and for distal systems by Donoso and Sun; the general commuting case is the standing pointwise question, and the triangular Hilbert transform is the singular integral long studied as its harmonic-analysis counterpart. According to the repository, GPT-6 Astra Pro was instructed to adapt OpenAI's preprint 'Annular variation of the triangular Hilbert transform at the symmetric point', released on 5 October 2026, solved the problem and wrote a blueprint, and Claude Opus 5.5 then generated the Lean formalization. The statement in Theorems.lean, written by the human authors, uses only Mathlib's definitions of measure-preserving maps, $L^p$ membership and limits, and the Palomar record replays the proof against it under the three standard axioms.

Novelty check

Searched arXiv and the web on 2026-10-20 for pointwise convergence of bilinear ergodic averages for commuting transformations. The sources found describe positive answers only for powers of one map and for distal systems. The search also found a second proof of the same theorem, by Guo, Xiao and Zhang (arXiv:2610.26388, posted 19 October 2026), by a different method built on matrix-energy estimates and Gaussian heat flow; its AI-use statement says ChatGPT (GPT-6) helped with the kernel, the proof strategy and one lemma, and it cites the same OpenAI preprint. Neither group refers to the other. This repository's commit history begins on 9 October and it was registered at Palomar on 18 October, so its priority rests on the repository rather than a dated preprint.

Caveats and known objections

Graded formal for the stated theorem on the Palomar registration, which replays the proof with two independent kernels against a 33-line Challenge statement built only from Mathlib definitions. That is the anchoring the Dedekind zeta entry treats as enough, and it is why this entry differs from Palomar results whose statements rest on their authors' own definitions. The grade certifies the theorem, not the blueprint or the account of how it was found: the repository says only README.md and Theorems.lean are human-authored, the formalization was generated by a model, and no mathematician is on record as having read the proof. The Palomar abstract names the model as GPT 6 Pro while the repository's AI statement at the registered commit says GPT 6 Astra Pro; the entry follows the repository. Autonomy is ai-led rather than autonomous because the humans chose the problem and supplied the approach, adapting one specific prior result, which is itself an unrefereed preprint from an unreleased model.

Independent checks

Zhuowen Guo, Rongzhong Xiao and Shuhao Zhang (independent second proof): Proved the same theorem, endpoint pairs included, by a method that uses neither the circle method nor characteristic-factor theory. The paper discloses GPT-6 assistance with the proof strategy, so it is independent of the authors here but not of AI. · link ↗

whataifound.org (statement reading): Read Challenge.lean at the registered commit: one theorem whose hypotheses are a probability measure, two commuting measure-preserving maps, and $f \in L^p$ , $g \in L^q$ with $1 \le p$ , $1 \le q$ and $p^{-1} + q^{-1} \le 1$ , and whose conclusion is that for almost every $x$ the averages have a limit in $\mathbb{C}$ . It uses no definitions beyond Mathlib's and matches the informal statement. · link ↗

Machine-checked elsewhere

PalomarPALOMAR-2026-10-18-000026

roos-j/lean-twocommuting at 5abb8fad6c99 · checked 2026-10-18

Provedpointwise_convergence_two_commuting

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.

Permitted axioms are exactly propext, Classical.choice and Quot.sound, replayed with the nanoda and con-ron kernels.

Disagree with these grades?

Bring a citation: a grade moves on evidence, not on argument.

Challenge this grade Submit a check

Or on GitHub: submit a check challenge the grade send a correction or send a pull request

Entry history (1 event)

2026-10-20AddedEntered the registry graded Formally 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 formally verified for verification and ai-led for autonomy. What these mean.

Cite this entry

Plain text

whataifound.org. (2026). Pointwise convergence of ergodic averages along two commuting transformations. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-18-two-commuting-ergodic-averages

BibTeX

@misc{whataifound-independent-2026-averages,
  title        = {Pointwise convergence of ergodic averages along two commuting transformations},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by Independent. Verification: Formally verified. Autonomy: AI-led.},
  url          = {https://whataifound.org/finding/2026-10-18-two-commuting-ergodic-averages}
}

Related findings

Author verifiedNorm-variation of multiple ergodic averages, including Tao's norm-convergence theorem, autoformalized in Lean in one weekIndependent · 2026-08-27 Formally verifiedErdős Problem 173: a two-coloring of the plane misses at most one triangle, which is equilateralPlasma AI · 2026-10-19 Formally verifiedErdős Problem 408: an unconditional normal order for the number of totient iterationsPlasma AI · 2026-10-19

ergodic-theory harmonic-analysis lean formalization argument

← All mathematics findings in the registry