Browse › Combinatorics › 171 The hypercube Ramsey conjecture
The hypercube Ramsey number has linear order
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We prove that the two-color Ramsey number of the n-dimensional binary cube is at most $C2^n$, where C is an absolute constant. This resolves positively the hypercube Ramsey conjecture of Burr and Erdős.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Comments and discussion
- mo271, ErdosProblems/181:
erdos_181is true (google-deepmind/formal-conjectures issue #6906, opened 7 October 2026, closed 11 October 2026). Argues that Theorem 1.1 of this paper matches the Lean statementerdos_181and proposes marking it solved; the issue says the comparison was prepared with AI assistance.
Formalization
- Yao Xu (cadamcat), hypercube-ramsey-lean4 (GitHub repository, 2026). An independent Lean 4/Mathlib formalization of Theorem 1.1, stated as
Erdos181.erdos_181, which takes the cube graph, Ramsey number, finite Ramsey bounds and Lemma 2.1 from OpenAI's Lean library and formalizes the rest of the paper (Sections 3–18); the README says it was "Developed with AI assistance; all proofs are verified by the Lean 4 kernel." [AI-generated per source] - cadamcat, feat(ErdosProblems/181): mark solved and link the formal proof (google-deepmind/formal-conjectures PR #7128, merged 11 October 2026). Marks the unchanged statement
erdos_181as solved and links Xu's v1.0.0 proof, reporting a fresh build, full kernel replay, Comparator statement checks and an axiom check limited topropext,Classical.choiceandQuot.sound. - google-deepmind/formal-conjectures, FormalConjectures/ErdosProblems/181.lean (Lean file, current main). States $R(Q_n)\le C2^n$ as
erdos_181, taggedresearch solved, linking the cadamcat formal proof and citing this paper; the proof body in this file itself issorry.
Related prior literature mentioned by others
- Thomas Bloom, erdosproblems.com, Problem 181 (last edited 16 October 2026). Cites Erdős [Er93] ("Some of my favorite solved and unsolved problems in graph theory") and an Erdős–Sós remark on whether $R(Q_n)/2^n\to\infty$; the paper's bibliography includes neither.
- Konstantin Tikhomirov, A remark on the Ramsey number of the hypercube (arXiv:2208.14568, 2022; revised 2024-03-02). Referenced in the Formal Conjectures entry and the manuscript; establishes the earlier bound $R(Q_n)=O(2^{(2-c)n})$ for an absolute $c>0$.
- Bernard Lidický and Florian Pfender, Semidefinite Programming and Ramsey Numbers (arXiv:1704.03592, 2017; revised 2020-09-11). Cited in Erdős Problem a Day's working report; determines $R(Q_3,Q_3)=13$, giving small-dimensional context for the paper's asymptotic bound.
Possibly relevant literature (found by the agent, not checked)
- D. Conlon, J. Fox and B. Sudakov, Recent developments in graph Ramsey theory (arXiv:1501.02474, 2015). A survey whose Section 2.3 states the cube conjecture $r(Q_n)=O(2^n)$ as Conjecture 2.14 and reviews the sequence of upper bounds recounted in the paper's introduction.
Digests and expositions
- Latent Seminar, Linear-order Ramsey numbers for hypercubes (2026-10-07). Explains the paper's patch decomposition, common-neighbor lists and final Hall-obstruction estimates, and states that its proof outlines are not an independent verification of the complete proof. [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 171
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:The-hypercube-Ramsey-number-has-linear-order-September-23-2026,
author = {{OpenAI}},
title = {{The hypercube Ramsey number has linear order}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/The-hypercube-Ramsey-number-has-linear-order-September-23-2026/paper.pdf}{OAI:The-hypercube-Ramsey-number-has-linear-order-September-23-2026}},
year = {2026}
}Family 171: The hypercube Ramsey conjecture
Resolves the Burr–Erdős hypercube Ramsey conjecture: the two-color Ramsey number of the n-dimensional cube is $\Theta(2^n)$. Thus every red-blue coloring of a complete graph on a universal constant times the cube's number of vertices contains a monochromatic copy of the cube.
This is the only paper in this family.