Ergodicity of billiards in every triangle with an irrational angle
For a Euclidean triangle with angles , consider the unit-speed billiard flow on with specular reflection, discarding the null set of trajectories that hit a vertex, and the measure . When all angles are rational multiples of the flow splits into invariant directional surfaces and is not ergodic. Zemlyakov-Katok's unfolding and Kerckhoff-Masur-Smillie gave ergodicity for a dense set of polygons, Vorobets for angles with exceptionally fast rational approximation, and Chaika-Forni weak mixing for a dense set; numerical studies of some irrational right and isosceles triangles even suggested nonergodicity. Is the billiard flow ergodic in every triangle with at least one angle irrational relative to ?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Ergodic theory; polygonal billiards
- Posed by
- Classical problem of polygonal billiards (setting of Zemlyakov and Katok; surveyed by Masur and Tabachnikov)
- Year posed
- —
- Years open
- —
- Solved
- 2026-09-25
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 48 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1 (September 25): the unit-speed billiard flow in every nondegenerate triangle with at least one angle irrational relative to is ergodic for normalised area times uniform angle, off the null set of vertex-hitting trajectories; consequences include quantum ergodicity and growth of nodal domain counts. The October 5 companion proves the stronger weak mixing (the product flow is ergodic). Neither proves mixing, unique ergodicity, or any statement about individual orbits (for example existence of periodic orbits in obtuse triangles), and polygons with more sides are not treated.
What the AI did
The release README says the results were produced by an unreleased internal OpenAI model with a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result, and that some outputs build on earlier model results. This result is not among the README's exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region). The manuscript is authored 'OpenAI' and names no human author. The family has two manuscripts: ergodicity (September 25, 2026, this entry's principal) and weak mixing (October 5, 2026), which extends the ergodicity paper's coefficient-energy method to eigenfunctions.
Verification
No independent mathematician has checked this yet. Checked here: Theorem 1.1 of the ergodicity manuscript was read against the question; it gives ergodicity for every nondegenerate triangle with at least one irrational angle, no genericity or Diophantine condition. The challenge lean/ComparatorChallenges/IrrationalTriangleBilliard.json and its solution module OAI.Dynamics.TriangleBilliards.Main exist at the pinned commit (found via lean/docs/150.md) but are not in the formalization catalogue. The statement was read here: for every triangle with an irrational angle it asserts a normalised phase measure, almost-everywhere existence and uniqueness of complete flight chains avoiding vertices with specular reflection, measure preservation and the flow law almost everywhere, and that every flow-invariant measurable set has measure 0 or 1. That states the headline ergodicity claim. Not rebuilt here. Permitted axioms: propext, Quot.sound, Classical.choice. Weak mixing is not formalised.