---

Claim. The preprint The hypercube Ramsey number has linear order of the OpenAI mathematics release (dated 23 September 2026; its author line reads OpenAI, and the release's README says that its manuscripts were produced by an internal OpenAI model, which it does not name, and are at different stages of verification, not all with Lean formalizations) states as its Theorem 1.1 that there is an absolute constant $C>0$ with

$$R(Q_n)\le C\,2^n\qquad\text{for every integer }n\ge0,$$

where $Q_n$ is the graph on $\{0,1\}^n$ whose edges join vectors differing in one coordinate and $R(H)$ is the least $M$ such that every red-blue coloring of the edges of $K_M$ contains a monochromatic copy of $H$, not necessarily induced. This is the displayed statement of Problem 181, and the manuscript names the question of Burr and Erdős, whether the cubes form an $L$-set, as what it resolves. The manuscript is carded at openai_2026_hypercube_ramsey_number_has_linear_order, with the theorem paged at its Theorem 1.1 page. With the two-block lower bound $R(Q_n)\ge3\cdot2^{n-1}-1$ that the introduction records, the theorem determines the order of $R(Q_n)$; the manuscript says it gives no numerical value of $C$ and does not decide whether $R(Q_n)/2^n$ converges. Its introduction places the result after the bounds of Graham, Rödl and Ruciński, Shi, Fox and Sudakov, Conlon, Fox and Sudakov, Lee and Tikhomirov, the last three recorded on the problem page, and notes that the fixed-degeneracy theorem of Lee does not reach the cube because the degeneracy of $Q_n$ is $n$.

Method and read depth. By the introduction, the proof works with a hypothetical sequence of counterexamples having two disjoint host sides of size $N$ each with $N/2^n\to\infty$ at no prescribed rate, derives discrepancy from the absence of a cube in both colors, excludes a cluster structure, and embeds the cube through a tiling by subcubes fixed on initial coordinates, with piece sizes from retained patch masses, with a regime guide and a dependency diagram organizing eighteen sections. Claims checked for Theorem 1.1, for Lemma 2.1 (the reduction to a counterexample sequence), for the lower-bound paragraph of Section 1.1 and for the statements of the staging results the card lists; the proof (Sections 2--18) was read for its structure only, no step was checked, and nothing here is review.

Depends on. Nothing in this wiki; the manuscript's Section 3 supplies the finite tools its proof uses, resting on standard results it cites.

Formalization. None of the theorem. The release's Lean tree at the pinned revision holds OAI/Combinatorics/Ramsey/Hypercube.lean, linked above and imported by the root module, with no catalog entry and no comparator challenge. It defines the cube graph, and the Ramsey number through copies that need not be induced. It proves the elementary bounds $2^n\le R(Q_n)\le2^{2^n+2^n}$. It also proves the manuscript's Lemma 2.1 (counterexample_sequence_of_not_linear): if no $C>0$ has $R(Q_n)\le C2^n$ for every $n$, there are dimensions tending to infinity and red-blue colorings between two sides of size $N\le n2^n$, with $N/2^n\to\infty$, containing no monochromatic cube. It does not state or prove Theorem 1.1. Nothing was built or audited here.

Standing. Claimed. The manuscript is a release preprint with no journal record, no known independent review as of 2026-10-07, and no Lean proof of Theorem 1.1 in the release's tree (see Formalization). The site's page for Problem 181, accessed 2026-09-18, shows OPEN with an empty proof-claim tab. A refereed version or a documented independent acceptance would move the claim to accepted; until then the problem's standing is claimed through this page.