Dynamical systems and ergodic theory·OpenAI Math·Result 150·Lean formalisation listed
Weak mixing of triangular billiards with an irrational angle
One of the 372 results in OpenAI's public mathematics catalogue, filed under dynamical systems and ergodic theory: 2 preprints, the latest dated 5 October 2026. This page quotes OpenAI's own summary of the claim, links the papers and abstracts, and embeds the animation.
What OpenAI claims
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)
Papers (2)
Weak mixing of triangular billiards with an irrational angle
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.
Ergodicity of triangular billiards with an irrational angle
We prove that the unit-speed billiard flow in every nondegenerate Euclidean triangle with at least one angle irrational relative to π is ergodic for normalized area times uniform angular measure. No genericity or Diophantine condition is required. The flow is considered outside the null set of trajectories that hit a vertex.
Status
Preprint. The papers have not been independently reviewed. Treat the result as OpenAI's claim until other mathematicians have checked it. If a video exists, it illustrates the statement; it is not the proof.
Videos about this result
Related results in Dynamical systems and ergodic theory
- 151A C1 counterexample to the entropy conjectureLean
- 152Zero entropy does not guarantee a smooth positive-volume modelLean
- 153Arithmetic classification and non-Pisot singularity for Bernoulli convolutions
- 154Pointwise multiple ergodic averages for mixing transformations
- 143Hilbert's sixteenth problem: uniform bounds for limit cyclesVideoLean
- 144Banach’s simple Lebesgue-spectrum problemLean