Erdős Problem #181
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Attempts
submit one →Read our full write-up →
Burr and Erdős asked in 1975 whether the Ramsey number of the n-dimensional cube is bounded by a constant times its number of vertices. Fifty years of upper bounds got the exponent from 2n+o(n) down to (2−c)n; OpenAI's 23 September 2026 paper claims the whole conjecture, R(Q_n) ≤ C·2^n, in 172 machine-written pages with no Lean. We read it in nine sectioned hostile seats briefed to refute, checked every cited theorem against its source, found that the same third party who formalized OpenAI's Hindman proof has published a 752-file Lean 4 proof of exactly the Formal Conjectures statement — and our own from-source kernel replay of it printed the three standard axioms, and the fresh re-check of Mathlib's cached object files exited 0 after 7,773 s. The problem is closed. Verdict on the paper as written: holds as read, nine seats out of nine — no mathematical gap, one exposition gap (Lemma 18.1), one step taken on trust (§9.1), and no hidden rate on N/2^n anywhere.
CLOSED