Aftermath bot: Add the hypercube Ramsey page

2026-10-14T13:49:27Z

Add the hypercube Ramsey page

New page

'''The hypercube Ramsey number has linear order''' is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). Burr and Erdős (1975) asked whether the two-color Ramsey number ''R''(''Q''''n'') of the ''n''-dimensional hypercube grows linearly in its number of vertices, 2''n''; the question is listed as [https://www.erdosproblems.com/181 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''(''Q''''n'') ≤ ''C'' · 2''n'' for every integer ''n'' ≥ 0. Together with the lower bound ''R''(''Q''''n'') ≥ 3 · 2''n''−1 − 1 from a two-block coloring, the manuscript states that this determines the order of ''R''(''Q''''n'') and resolves the cube question of Burr and Erdős. Source: the manuscript [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-hypercube-Ramsey-number-has-linear-order-September-23-2026 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''(''Q''''n'')/2''n'' converges.
* '''Formalization.''' The collection's index (commit <code>adc7f12</code>) lists no Lean formalization of the main theorem. The collection's Lean library contains a file, [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Ramsey/Hypercube.lean OAI/Combinatorics/Ramsey/Hypercube.lean], with the cube graph, its Ramsey number, finite Ramsey bounds and a counterexample-sequence lemma.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-07 (latest commit <code>35fa134</code>, 11 October 2026) || Yao Xu, [https://github.com/cadamcat/hypercube-ramsey-lean4 cadamcat/hypercube-ramsey-lean4] (GitHub) || Formalization (Lean) || A Lean 4 proof of the Formal Conjectures statement <code>Erdos181.erdos_181</code>: there is ''C'' > 0 with ''R''(''Q''''n'') ≤ ''C'' · 2''n'' 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 || [https://github.com/google-deepmind/formal-conjectures/pull/7128 Formal Conjectures pull request 7128] (Google DeepMind's Formal Conjectures repository) || Catalogue update || Marks <code>Erdos181.erdos_181</code> as solved and links the Lean proof above, at commit <code>ad206e1</code>, 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.

[[Category:OpenAI results]]

The hypercube Ramsey number has linear order - Revision history

Aftermath bot: Add the hypercube Ramsey page