Radius of comparison equals half the mean dimension

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

For every minimal homeomorphism h of an infinite compact metrizable space X, the radius of comparison of \(C(X)\rtimes_h\mathbb Z\) equals \(\tfrac12\mathrm{mdim}(X,h)\), including infinite values. Zero mean dimension is equivalent to the small boundary property, Jiang–Su stability and finite nuclear dimension; in this case nuclear dimension is at most one.

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

In Radius of comparison equals half the mean dimension, 25 September 2026

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

Let h be a minimal homeomorphism of an infinite compact metrizable space X. Then

\rc\bigl(C(X)\rtimes_h\Z\bigr)=\frac12\mdim(X,h) \qquad\text{in }[0,\infty].

Corollary 1.2 (Zero mean dimension and crossed-product regularity)

In Radius of comparison equals half the mean dimension, 25 September 2026

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

Let h be a minimal homeomorphism of an infinite compact metrizable space X, and put A=C(X)\rtimes_h\Z. The following conditions are equivalent:

1.
\mdim(X,h)=0;
2.
(X,h) has the small boundary property;
3.
A\cong A\otimes\mathcal Z;
4.
\dim_{\mathrm{nuc}}(A)<\infty;
5.
\dim_{\mathrm{nuc}}(A)\le1.

In particular, if \mdim(X,h)\in(0,\infty], then A\not\cong A\otimes\mathcal Z and \dim_{\mathrm{nuc}}(A)=\infty.

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 (Torus compression) in Filtered products and boundary-preserving compression in complex cobordism, 25 September 2026.
Theorem 1.1 (Filtered products) in Filtered products and boundary-preserving compression in complex cobordism, 25 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.

Filtered products and boundary-preserving compression in complex cobordism

25 September 2026, current edition.

Read it here PDF

We prove that, in sufficiently large smash powers, an \(MU\)-null restriction to a finite pointed subcomplex becomes stably null on the entire union of products with a fixed positive proportion of restricted factors. This coherent vanishing theorem yields boundary-preserving compression of cube-valued maps on every compact metrizable input space. When the torus slot bundle embeds continuously into a trivial bundle of rank less than twice the source rank, the compression places a positive proportion of slots on their boundaries in arbitrarily large powers and fixes every original boundary slot exactly. An example at equality shows that the strict rank inequality cannot be removed.

Radius of comparison equals half the mean dimension

25 September 2026, current edition.

Read it here PDF

We prove the integer-action case of the Phillips–Toms conjecture: for every minimal homeomorphism of an infinite compact metrizable space, the radius of comparison of its crossed product equals one half of its mean dimension, including equality at infinity. For these systems, zero mean dimension and the small boundary property are equivalent to Jiang–Su stability and to finite nuclear dimension of the crossed product; in this case its nuclear dimension is at most one.

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

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.

Follow-up work by others

George A. Elliott, Zhuang Niu, Mean dimension and radius of comparison, 8 October 2026. Source
Elliott and Niu generalise OpenAI’s Z-action radius-of-comparison theorem to amenable group actions with the uniform Rokhlin property and open-set comparison, using the topological ideas of the OpenAI paper.

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 302 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 302 The release has no Lean statement for this family. Open the form