Dynamical systems and ergodic theory · Result 150

Weak mixing of triangular billiards with an irrational angle

2 papersLean

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.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 2

Weak mixing of triangular billiards with an irrational angle

OpenAI · October 5, 2026

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.

Read PDF Download Source

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}
}

Ergodicity of triangular billiards with an irrational angle

OpenAI · September 25, 2026

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.

Read PDF Download Source

Cite

@misc{OAI:Ergodicity-of-triangular-billiards-with-an-irrational-angle-September-25-2026,
  author = {{OpenAI}},
  title = {{Ergodicity of triangular billiards with an irrational angle}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Ergodicity-of-triangular-billiards-with-an-irrational-angle-September-25-2026/Ergodicity-of-triangular-billiards-with-an-irrational-angle-September-25-2026.pdf}{OAI:Ergodicity-of-triangular-billiards-with-an-irrational-angle-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Ergodicity of triangular billiards with an irrational angle

Scope

The formalization proves that the unit-speed billiard flow in every nondegenerate Euclidean triangle with at least one angle irrational relative to \(\pi\) is ergodic for normalized area times uniform angular measure. 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. No genericity or Diophantine condition on the irrational angle is assumed.

Comparator links

Result	Comparator statement
Ergodicity of triangular billiards with an irrational angle	IrrationalTriangleBilliard.lean

Scope note on GitHub →