Erdős Problem #986
PROVEDdatabase updated 2026-06-21
The statement as posed is true, and a proof exists.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
For any fixed \(s\geq 3\), \[R(s,k) \gg \frac{k^{s-1}}{(\log k)^c}\] for some constant \(c=c(s)>0\). According to Chung and Graham [ChGr98] this was first conjectured by Erdős in 1947. Proved by Bradač [Br26], with \(c=2s-4\). The linked formal proof (Codex and GPT-5.6 Sol) gives `k ^ (s - 1) / (log k) ^ c = O(R(s, k))` for a natural `c > 0`, with the Ramsey number defined through `CliqueFree`/`IndepSetFree`; this implies the statement below.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/986.Newer public claim (6 Oct 2026): OpenAI's internal-model release claims, for this problem, r(s,t) = t^(s−1)/(log t)^(s−2+o(1)) for s ≥ 5 — refereed here 20 Oct; both Lean proofs (858 modules) kernel-replayed on our machine, statements matched; the same library proves s = 4, r(4,t) = t³/(log t)^(2+o(1)), through its d = 3 construction (stated in neither paper; derived on paper by Chen and Lin–Zhang on 11 and 13 Oct) — see /day/986-openai-sharp-log-exponent-off-diagonal-ramsey-refereed — family 170 at
github.com/openai/math, OpenAI's own Lean proves both Theorems 1.1 (s = 5, and every s ≥ 6) — kernel-replayed on our machine on 20 Oct 2026 (858 modules, 0 errors, standard axioms, statements matched to the comparator challenges under pp.all, leanchecker --fresh rc 0 on both closures); the library's construction is stated for every d ≥ 3, and a verbatim copy of OpenAI's assembly with 6 ≤ s relaxed to 4 ≤ s proves the s = 4 case too (our probe, standard axioms; derived on paper by Chen and Lin–Zhang on 11 and 13 Oct) — see our /day entry. Bloom calls these claims, not endorsements.
Prizenone
Solution in Leanno
FULL WRITE-UP BY THIS SITE · OCT 20, 2026
Erdős asked whether R(s,k) ≫ k^(s−1)/(log k)^c for some c; Bradač answered yes in June with c = 2s − 4, and the problem page records it as resolved — nothing here closes it again. Two OpenAI preprints released on 6 October claim much more for s ≥ 5: the log power is s − 2 + o(1), the Ajtai–Komlós–Szemerédi upper bound's own power, so the exponent is determined. Both come with Lean proofs (858 modules). We rebuilt every module from source on our machine, printed only the three standard axioms for both main theorems, matched both statements to OpenAI's comparator challenges, and re-checked both import closures with leanchecker --fresh. The library states its construction for every dimension d ≥ 3, not Paper B's d ≥ 5 (Paper A is the single case d = 4); a verbatim copy of OpenAI's assembly with 6 ≤ s relaxed to 4 ≤ s (the hypothesis is used only for side conditions) gives r(4,t) = t³/(log t)^(2+o(1)), past Mattheus–Verstraëte's t³/(log t)⁴, on the standard axioms. Chen (11 October) and Lin–Zhang (13 October) had derived that r(4,t) statement on paper, taking OpenAI's s ≥ 5 theorem as an input. A bridge, also kernel-checked, carries the library to Formal Conjectures' own statement of #986 at every s ≥ 4. Six AI referee seats read the papers and the Lean and found no gap in what they read; three were cut off before finishing, and parts of the s = 5 paper went unread.
CLOSED