The hypercube Ramsey number has linear order
The hypercube Ramsey number has linear order is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math). Burr and Erdős (1975) asked whether the two-color Ramsey number R(Qn) of the n-dimensional hypercube grows linearly in its number of vertices, 2n; the question is listed as Erdős problem 181. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original result
- Claim. There is an absolute constant C > 0 such that R(Qn) ≤ C · 2n for every integer n ≥ 0. Together with the lower bound R(Qn) ≥ 3 · 2n−1 − 1 from a two-block coloring, the manuscript states that this determines the order of R(Qn) and resolves the cube question of Burr and Erdős. Source: the manuscript The hypercube Ramsey number has linear order, dated 23 September 2026, Theorem 1.1.
- Scope. The manuscript states that it gives no numerical value for C and does not determine whether R(Qn)/2n converges.
- Formalization. The collection's index (commit
adc7f12) lists no Lean formalization of the main theorem. The collection's Lean library contains a file, OAI/Combinatorics/Ramsey/Hypercube.lean, with the cube graph, its Ramsey number, finite Ramsey bounds and a counterexample-sequence lemma.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 14 October 2026) |
|---|---|---|---|---|
2026-10-07 (latest commit 35fa134, 11 October 2026) |
Yao Xu, cadamcat/hypercube-ramsey-lean4 (GitHub) | Formalization (Lean) | A Lean 4 proof of the Formal Conjectures statement Erdos181.erdos_181: there is C > 0 with R(Qn) ≤ C · 2n for every n. The README states that the formal proof follows the manuscript and takes the cube, its Ramsey number, finite Ramsey bounds and the manuscript's counterexample-sequence lemma from OpenAI's Lean library. The repository's verification notes record a second-kernel check of version 1.0.0. |
Author-reported; the README states that the work was developed with AI assistance, and the repository's attribution file states that it formalizes the theorem and does not claim a new mathematical solution. |
| 2026-10-11 | Formal Conjectures pull request 7128 (Google DeepMind's Formal Conjectures repository) | Catalogue update | Marks Erdos181.erdos_181 as solved and links the Lean proof above, at commit ad206e1, as its formal proof. |
Merged on 11 October 2026. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.