The near-boundary Birkhoff conjecture

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

Resolves the near-boundary Birkhoff conjecture for smooth strictly convex planar billiards of positive curvature. Such a billiard is an ellipse whenever a full grazing annulus is continuously foliated by individually invariant essential curves. A continuous physical collar of smooth closed convex caustics also suffices.

The release has no Lean statement for this family, so there is no formal statement to compare with the result described above.

What the papers state

Theorem 1.1 (Phase-foliation rigidity)

In Continuous Phase Foliations Create Analytic Caustic Collars, 24 September 2026

The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.

Suppose a T-invariant open annulus U\subset M contains (\R/L\mathbb Z)\times(0,\eta) for some \eta>0. Suppose there is a homeomorphism

H:\mathbb S^1\times(0,1)\longrightarrow U

whose leaves are essential simple closed curves, each individually invariant under T. Then \Omega is an ellipse: there are c\in\R^2 and a real symmetric positive-definite matrix Q such that

\Omega=\{x\in\R^2:(x-c)^TQ(x-c)<1\}.

Circles are included.

Theorem 1.2 (Physical-collar rigidity, [Rigidity of Smooth Billiards with a Continuous…, Definition 1.1 and Theorem 1.2])

In Continuous Phase Foliations Create Analytic Caustic Collars, 24 September 2026

Possible match to OpenAI’s description, selected because it shares the most wording. No review confirming the selection is recorded.

A bounded strictly convex planar domain with C^\infty regular boundary of positive curvature and a continuous physical caustic collar is an ellipse.

The release does not say which paper theorem its catalogue describes. Both statements above are shown whole: the paper’s main theorem first, then the statement that shares the most wording with the description. The atlas has not reviewed either choice.

Two more possible matches

Theorem 1.3 (Regularity of a phase-foliated collar) in Continuous Phase Foliations Create Analytic Caustic Collars, 24 September 2026.
Theorem 1.2 in Rigidity of Smooth Billiards with a Continuous Caustic Collar, 24 September 2026.

Reported proof verification: The release has no Lean statement for this family. The papers are available to read and assess.
Papers and explanations: Two current papers, each readable here as a page beside its PDF.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

Continuous Phase Foliations Create Analytic Caustic Collars

24 September 2026, current edition.

Read it here PDF

For a smooth strictly convex planar billiard of positive curvature, a continuous foliation of a full grazing annulus by individually invariant essential curves forces an analytic boundary and a jointly analytic collar of smooth strictly convex caustics. The physical-collar rigidity theorem proved in the companion article then implies that the table is an ellipse.

Rigidity of Smooth Billiards with a Continuous Caustic Collar

24 September 2026, current edition.

Read it here PDF

We prove that a smooth strictly convex planar billiard with positive curvature is an ellipse whenever a full neighborhood of its boundary is continuously foliated by smooth closed convex caustics. No differentiability across the leaves is assumed. This resolves the near-boundary Birkhoff conjecture in the stated smooth class.

Lean statements

The release has no Lean statement for this family. Its papers remain available to read, and contributors can propose a formal statement of a result. Suggest a change

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

The release contains no Lean statement for this family, so there is no formal statement to compare with OpenAI’s description.

What these papers cite in the release, and what cites them

These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.

Within this family

Continuous Phase Foliations Create Analytic Caustic Collars cites Rigidity of Smooth Billiards with a Continuous Caustic Collar.

Papers elsewhere in the release that this family’s papers cite

This family’s papers cite no paper elsewhere in the release.

Papers elsewhere in the release that cite this family’s papers

No paper elsewhere in the release cites this family’s papers.

References outside the release

Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release

Explain a result, compare statements or propose a correction

Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.

Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.

Offer to write an explanation Suggest a source attribution Suggest a change

What people have said

Commentary on this family by others, dated and credited. It is commentary, not a finding.

An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “Major math journal”. The page says that nothing on it is verified.
Author not stated. Source

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Identify the theorem the catalogue describes

Family 147 The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means. Open the form

State the result in Lean

Family 147 The release has no Lean statement for this family. Open the form