Open Research Index

Pointwise a.e. convergence of ergodic averages with respect to two commuting transformations in Lean

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

Palomar Registrypalomar/PALOMAR-2026-10-18-000026Oct 18, 2026math.DSscore 0

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.

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-10-18-000026
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-18-000026/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-10-18-000026/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'