Ergodicity and weak mixing of irrational triangular billiards
From OpenAI Aftermath
Ergodicity and weak mixing of irrational triangular billiards concern the billiard flow in a Euclidean triangle, a point moving at unit speed and reflecting specularly at the sides, with the natural measure given by area times uniform direction. If every angle is a rational multiple of π, the phase space splits into invariant directional surfaces and the full flow is not ergodic; for triangles with an irrational angle, ergodicity was previously known only for generic or specially approximable tables. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math), dated 25 September and 5 October 2026, claim ergodicity and then weak mixing for every triangle with at least one irrational angle, with a Lean formalization of the ergodicity theorem. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper or a formal proof is not presented here as independent verification.
Background
- As recounted in the introductions of the manuscripts:
- Zemlyakov and Katok connected polygonal billiards to flat geometry by unfolding. For rational polygons, Kerckhoff, Masur and Smillie proved unique ergodicity in almost every direction, and their work also gives ergodicity of the full flow for a dense Gδ family of tables, without asserting it for each irrational triangle.
- Vorobets gave a sufficient condition requiring exceptionally fast simultaneous rational approximation of the angles, with explicit ergodic examples including irrational right triangles, and Chaika and Forni proved weak mixing of the full flow for a dense Gδ set of n-gons for each fixed n. Numerical studies of irrational right triangles and of isosceles triangles had raised doubts about ergodicity. The analytic framework of Forni and Moll for flat surfaces with cone points is the starting point of the proofs.
The original results
- Claim (ergodicity). Theorem 1 of Ergodicity of triangular billiards with an irrational angle states that the unit-speed billiard flow in every nondegenerate triangle with at least one angle irrational relative to π is ergodic for normalized area times uniform angular measure, after discarding the null set of trajectories that hit a vertex. No genericity or Diophantine condition is imposed. A corollary derives, from known theorems, quantum ergodicity of Dirichlet and Neumann eigenbases and nodal-domain counts tending to infinity along density-one subsequences.
- Claim (weak mixing). Theorem 1.1 of Weak mixing of triangular billiards with an irrational angle states that the same flow is weakly mixing; equivalently, the product of the flow with itself is ergodic.
- Method, as described: following Forni and Moll, an invariant function is expanded in angular Fourier modes, whose coefficients satisfy Cauchy–Riemann-type recurrences on the doubled flat surface. A measurable invariant function or eigenfunction gives only the derivative along the flow, and the missing transverse derivative cannot be assumed. The ergodicity manuscript removes this regularity obstacle for invariant functions by coefficient-energy estimates and long averages on orbit segments away from the cone points. The weak-mixing manuscript extends the method to every real spectral parameter λ and proves the sharp bound that the squared norms of the two derivatives sum to at most λ2 times the squared norm of the function, so the transverse derivative vanishes. On the triangle an eigenfunction is then a plane wave with a direction-dependent amplitude; reflection in the two sides through an irrational vertex makes the amplitude constant, reflection in the third side excludes every nonzero frequency, and the standard spectral criterion gives weak mixing.
- Sources (openai/math repository, commit
7ef5c0c): Ergodicity of triangular billiards with an irrational angle (25 September 2026); Weak mixing of triangular billiards with an irrational angle (5 October 2026). - Formalization, as described by the repository. The scope note lean/docs/150.md states that the formalization proves the ergodicity theorem: it constructs the flow outside the null set of exceptional trajectories, proves uniqueness of the flight chain there, and establishes measure preservation and the flow law almost everywhere. The scope note does not mention weak mixing. The Comparator statement is
IrrationalTriangleBilliard.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 30 October 2026) |
|---|---|---|---|---|
| 2026-10-06 | Ergodicity and weak mixing of irrational triangular billiards, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains the phase space of a triangular billiard, the two statements, the rational obstruction, the flat double and the missing derivative, the two limits and transverse rigidity, the exclusion of nonzero eigenfrequencies by reflection, and the spectral consequences, with proof outlines. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit 94c6630, 28 October 2026) |
Review (fidelity of the formal statements) | Rates this family "weaker statement": the Lean statement gives ergodicity, together with almost-everywhere existence and uniqueness of flight chains, measure preservation and the flow law, while weak mixing, the family's headline, is strictly stronger and is not stated. It records a Comparator pass on cloud machines for IrrationalTriangleBilliard on 8 October 2026. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38051470892 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the IrrationalTriangleBilliard solution, in 322 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list IrrationalTriangleBilliard, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee reviews rank_139 (ergodicity manuscript) and rank_369 (weak-mixing manuscript) in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap in either manuscript. For the ergodicity manuscript it adds one minor note, which it states is not a demonstrated gap: the analytic rigidity proposition does not use irrationality and would apply to every compact flat cone surface, which would give a new elementary proof of the theorem of Kerckhoff, Masur and Smillie and settle the ergodicity of flat cone surfaces with an irrational cone angle. Given the strength of this consequence, the reviewer asks that an independent specialist verify the argument, in particular the lemma bounding the modes of bounded invariant functions. The weak-mixing manuscript has no note. | Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0. |
| 2026-10-16 | AI Proved What?, episode 150 No hidden rhythm?, remade version of 26 October 2026 | Reading (exposition) | Video explainer of the two claims and their history. The episode states that neither manuscript claims mixing, rates, unique ergodicity or anything about individual orbits, and that nothing is claimed beyond triangles. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as preprints: OpenAI, two preprints, 12 and 13 pages, dated September 25 and October 5, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: only the ergodicity theorem. |
Notes
- The background summarizes the manuscripts' own account of earlier work.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
