Browse › Dynamical systems and ergodic theory › 150 Weak mixing of triangular billiards with an irrational angle
Weak mixing of triangular billiards with an irrational angle
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We prove that the unit-speed billiard flow in every nondegenerate Euclidean triangle with at least one angle irrational relative to π is weakly mixing for normalized Liouville measure. Equivalently, the product of the flow with itself is ergodic.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI, Lean scope notes for family 150 (release repository, lean/docs/150.md, October 2026). Describes a formalization of the September ergodicity theorem (a.e. flow construction, flight-chain uniqueness, measure preservation); it does not state that weak mixing, the main theorem of this paper, is formalized. [family-level]
- OpenAI, IrrationalTriangleBilliard.lean (openai/math, lean/ComparatorChallenges, October 2026). Comparator statement
irrational_triangle_billiard(flow construction a.e., measure preservation, and invariant sets of measure 0 or 1); this file states the ergodicity theorem only, with the proof left assorry. [family-level]
Related prior literature mentioned by others
- Giovanni Forni and Nelson Moll, Cohomological equation for geodesic flows on flat surfaces (arXiv:2510.18128v1, 2025-10-20). Azmat’s exposition identifies this work as the analytic framework behind the family’s treatment of invariant functions and highlights the horizontal Sobolev regularity assumption that the September manuscript seeks to remove. [family-level]
Possibly relevant literature (found by the agent, not checked)
- Č. Lozej, G. Casati, T. Prosen, Quantum chaos in triangular billiards (arXiv:2110.04168, 2021). Large numerical study treating generic irrational triangles as presumed mixing and one-rational-angle triangles as presumed weakly mixing or non-ergodic; relevant to the paper's discussion of numerical evidence on weak mixing.
- J. Seaward, Ergodicity in Golden Billiards (arXiv:1910.14350, 2019). Comment on the Wang–Casati–Prosen numerics (cited as [WCP]) arguing that "strongly irrational" right triangles are likely ergodic; bears on the paper's remark on conflicting numerical observations.
- Z. Hwang, C. A. Marx, J. Seaward, S. Jitomirskaya, M. Olshanii, Growth of the Wang-Casati-Prosen counter in an integrable billiard (SciPost Phys. 14, 017 (2023); arXiv:2011.09467). Studies the counter on which the Wang–Casati–Prosen non-ergodicity evidence for irrational right triangles rests; related to the numerics the paper cites as [WCP].
- S. Troubetzkoy, Approximation and billiards (arXiv:math/0611599, 2006). Survey of transitivity, ergodicity and weak-mixing results for polygonal billiards obtained by the Katok–Zemlyakov approximation method, the genericity-type results the paper contrasts with its every-triangle statement.
Digests and expositions
- Azmat, Irrational Triangular Billiards: How OpenAI’s Proof Tackles a Decades-Old Ergodicity Mystery (Binary Verse AI, 2026-10-15). Explains the September manuscript’s Fourier-coefficient estimates, successive limits and quantum consequences, and identifies the October companion’s stronger weak-mixing claim while disclaiming independent verification of every analytic step. [family-level]
- heyprof, Triangular billiards — irrational angles mix (3D) (interactive exposition, undated; accessed 2026-10-21). Illustrates family 150 using trajectories, direction distributions and paired trajectories, noting that floating-point simulation cannot distinguish exact rationality from irrationality. [family-level]
Elsewhere
- Emergent Mind: family 150
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:Weak-mixing-of-triangular-billiards-with-an-irrational-angle-October-5-2026,
author = {{OpenAI}},
title = {{Weak mixing of triangular billiards with an irrational angle}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/Weak-mixing-of-triangular-billiards-with-an-irrational-angle-October-5-2026/weak-mixing-triangular-billiards.pdf}{OAI:Weak-mixing-of-triangular-billiards-with-an-irrational-angle-October-5-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/150.md. The Lean statements have not been checked by people against the paper's claims.
Family 150: Weak mixing of triangular billiards with an irrational angle
Proves that the billiard flow in every nondegenerate Euclidean triangle with at least one angle irrational relative to π is weakly mixing for normalized area times uniform direction. This strengthens ergodicity on the entire irrational-angle class, with no genericity or Diophantine restrictions.
Other papers in this family:
- Ergodicity of triangular billiards with an irrational angle · September 25, 2026