Rokhlin's multiple-mixing problem for one transformation

Comments and discussion

• Bryna Kra, quoted in ‘Breathtaking,’ ‘Devastating’: Mathematics Reels After New OpenAI Release (AI Europe reproduction of New York Times reporting, 2026-10-09). Kra singles out result 145 as of particular interest and says the manuscript's writing prevents her from understanding it.

Formalization

• OpenAI, Rokhlin’s multiple-mixing problem: Lean scope notes (OpenAI math release, lean/docs/145.md, 2026-10-06). The scope note states that the formalization proves mixing of every order k ≥ 3 for one invertible mixing probability-preserving transformation, with convergence as every successive time gap diverges, and links the Rokhlin comparator statement. [AI-generated per source]
• OpenAI math release, Comparator statement Rokhlin.lean (openai/math commit adc7f12, 2026). The challenge file defines IsMixing, MixingOfOrder, layoutTime and timeMap, and states OAI.Rokhlin.mixing_all_finite_orders with the proof left as sorry, which is how a comparator challenge is written.
• OpenAI math release, OAI/Dynamics/MultipleMixing/Main.lean (openai/math commit adc7f12, 2026). This file contains the release's proof of mixing_all_finite_orders, the Lean counterpart of Theorem 1.1.
• Carlos Toledo, OpenAI's math release: what it claims beyond what it checks (cert-machine audit of release commit fd4aeeb2ee4f, accessed 2026-10-21). The audit reports that the Rokhlin challenge passed Lean and nanoda checks, that all four displayed definition bodies matched, and that the solution theorem transferred to the displayed statement; it discloses that agents produced its checkers and readings. [AI-generated per source]
• punk01-shaka, OpenAI's Comparator configs leave 62 fully-written definitions unchecked (definition holes) (GitHub issue, 12 Oct 2026). Its table lists the Rokhlin comparator config with 4 of 4 definitions declared as holes, whose bodies Comparator does not check. The issue states: "This does not show that any of these results is wrong." [family-level]

Possibly relevant literature (found by the agent, not checked)

• V. V. Ryzhikov, Around Kalikow's theorem on multiple mixing (arXiv:2607.11852, July 2026). A survey of joinings and multiple mixing that includes a proof of Kalikow's twofold-implies-threefold theorem for rank-one maps, which the paper's introduction cites as Kalikow 1984.
• V. V. Ryzhikov, Unsolved problems on joinings, multiple mixing, spectrum, and rank (arXiv:2405.03641, May 2024). Discusses a hypothetical automorphism in MSJ(2)\MSJ(3) without multiple mixing; Theorem 1.1 would rule out any such mixing automorphism.
• V. V. Ryzhikov, Multiple mixing in ergodic theory (arXiv:2404.06476, April 2024, in Russian). A Russian-language account of the history and status of Rokhlin's k-fold mixing problem, which the paper's introduction recounts.

Digests and expositions

• Latent Seminar, Rokhlin's multiple-mixing problem and ordered joining arrays (2026-10-06). This exposition follows the finite-alphabet reduction, ordered joining arrays, conditional operators and cancellation argument, while explicitly distinguishing its selected proof explanations from independent verification of the complete proof.