Short··0:12·Dynamical systems and ergodic theory
Triangular Billiards: Weak Mixing
Watch on YouTubeAbout the problem →
About this video
Weak mixing of triangular billiards with an irrational angle
One irrational angle changes the billiard flow. OpenAI, the company behind ChatGPT, reports in its manuscript weak mixing for the unit-speed billiard flow in every nondegenerate Euclidean triangle with at least one angle irrational relative to pi. The measure is normalized area times uniform direction. Here weak mixing means that the product of the flow with itself is ergodic. This is not a claim of exponential trajectory separation or strong mixing.
Paper: Weak mixing of triangular billiards with an irrational angle
github.com/openai/math/blob/main/preprints/Weak-mixing-of-tri…
About the animation: A single ray follows five numerically computed specular flights in a triangle with angles pi/sqrt(8), 0.4*pi and the remaining angle. Five mirrored copies unfold the zigzag into a straight path, using exact reflections across each encountered edge. The unfolded path is collinear to floating-point tolerance. Three-dimensional hinges, camera motion and variable playback speed are presentation choices; the billiard is planar. This finite unfolding illustrates a construction discussed in the manuscript, not a proof or numerical verification of weak mixing. The linked formalization scope describes a weaker ergodicity companion statement.
GitHub repository: github.com/openai/math
Related formalization scope: github.com/openai/math/blob/main/lean/docs/150.md
The linked formalization scope documents ergodicity, the weaker companion result, rather than the weak-mixing statement selected for this animation. The stronger weak-mixing statement has not been independently machine-verified in this production.
Source-reported result. Selected theorem statements and scope were read; this is not an independent proof audit.
'Catalyst' by Scott Buckley - released under CC-BY 4.0. www.scottbuckley.com.au
scottbuckley.com.au/library/catalyst/
Licence: creativecommons.org/licenses/by/4.0/
Music edits: excerpted, crossfaded for looping, and gain adjusted.
About the problem
Dynamical systems and ergodic theory·OpenAI Math·Result 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. (Lean)
Topics
weak mixingtriangular billiardsirrational angleergodic theorydynamical systemsspecular reflectionOpenAI math3D math animationChatGPT
