#986: r(s,t) = t^(s−1)/(log t)^(s−2+o(1)) for every fixed s ≥ 5 — OpenAI's two Lean proofs kernel-replayed here; and the same library proves the s = 4 case directly, r(4,t) = t³/(log t)^(2+o(1)) — derived on paper from OpenAI's theorem by Chen and by Lin–Zhang on 11 and 13 October, stated in neither OpenAI paper

The problem (erdosproblems.com/986; [Er90b, p. 18], Chung–Graham 1998). "For any fixed s ≥ 3, R(s,k) ≫ k^s−1/(log k)^c for some constant c = c(s) > 0." The page (last edited 21 June 2026) credits Spencer (1977) with s = 3 and Mattheus–Verstraëte (Annals 2024: r(4,t) ≥ c t³/(log t)⁴) with s = 4, and records the problem as resolved by Bradač (arXiv:2605.28793, v3 of 16 June) with c = 2s − 4. Bradač's v3 says the step that raised his polynomial exponent from s − 2 to s − 1 "was found by an internal model at OpenAI and communicated to the author". The upper bound O(t^s−1/(log t)^s−2) is Ajtai–Komlós–Szemerédi 1980 (leading constant 1 + o(1): Li–Rousseau–Zang 2001). So after June the live question, for s ≥ 4, was the power of the logarithm: 2s − 4 below (Mattheus–Verstraëte's 4 at s = 4), s − 2 above.

The claim. Two preprints in the openai/math release (family 170 in OpenAI's numbering), both dated 24 September 2026 by their authors and first public in the repository's initial commit on 6 October 2026 (adc7f12, 21:58:50 UTC; every family-170 file is unchanged at today's head 1581d4c): The sharp logarithmic exponent of r(5,t) (41 pp) and Sharp logarithmic exponents for fixed off-diagonal Ramsey numbers (53 pp, s ≥ 6). Each Theorem 1.1: there is C_s such that, for every ε > 0 and all large t, t^s−1/(log t)^s−2+ε ≤ r(s,t) ≤ C_s t^s−1/(log t)^s−2, hence ((s − 1) log t − log r(s,t))/log log t → s − 2. The log power is determined; both papers say they do not claim a constant-factor lower bound at the upper bound's order.

The argument. The graph is Bradač's ordered incident-flag graph, sampled as a stream: N ≈ q^d log q independent uniform flags (a_i, b_i) of PG(d,q) — a point in a hyperplane, q prime — with positions i < j adjacent when a_i ⊥ b_j but a_j ⊥̸ b_i (a ⊥ b: the point a lies on the hyperplane b). Linear independence rules out K_d+1. An independent set is a "consistent" flag sequence, and the proof rules out one of length k ≈ q(log q)^1+η by entropy compression. A selected consistent sequence of length ℓ = Θ(k) would carry entropy at least dσℓ + ηℓ log σ − O(k) (σ = log q; a max-atom bound, so it survives a bounded number of conditionings on events of probability bounded below). But it can be compressed: mark all but O(q log q) positions inside known domains of size O(q^d), describe the sparse point–hyperplane incidence structures that remain from public random tables (rich-line and rich-plane bounds by the polynomial method, every degree kept below the characteristic — which is why q is prime), and pass to a shorter consistent subsequence. The first such description still costs far more than the surplus; after a bounded number of rounds (about 8/η) a decoder rebuilds a subsequence of length Θ(k) from dσℓ + O(k). The ηℓ log σ surplus is the whole margin, so every log σ in the message has to be paid for. A prime chosen afresh for each t gives all large t; the upper bound is reproved from a triangle-free independence bound and sampling.

The Lean, and our replay. The release carries a Lean proof of each Theorem 1.1 — OAI.SharpRamseyFive.main and OAI.SharpLogRamsey.main (s) (hs : 6 ≤ s) — in 858 modules (123,565 lines; 450 in the s = 5 tree and 408 in the s ≥ 6 tree, 32 of which the s = 5 proof also imports; Lean 4.34.1, Mathlib d13f23b7), importing nothing but Mathlib. A source audit of the whole closure found no axiom, sorry, native_decide, set_option or metaprogramming outside the two comparator-challenge files, where the one sorry each is the challenge itself. We compiled all 858 modules from source against Mathlib's published build cache at the lowest priority, beside solvers that have been running for a month: 0 errors, 55 minutes of wall time on three workers (8,645 module-seconds; no process above 6.9 GiB). #print axioms on the compiled library shows both main theorems depending only on propext, Classical.choice and Quot.sound. Their statements, printed in full (pp.all) together with the four definitions they are stated in, are identical to the comparator challenges elaborated on their own — an instrument we mutation-tested on both of its checks (one token of a hypothesis changed ⇒ MISMATCH; sorryAx added to an axiom list ⇒ flagged). Sanity checks: the s ≥ 6 theorem does not apply at s = 5 (a type error on its hypothesis), and a planted sorry shows sorryAx. leanchecker --fresh then re-checked every declaration in each import closure, Mathlib included: rc 0 after 3,498 s (s ≥ 6) and 3,579 s (s = 5); a missing-module control exits 1. We found no other published replay (arXiv, Formal Conjectures, the problem page and forum, the Palomar registry, Hacker News, MathOverflow).

What the library also proves: s = 4. Paper B fixes "an integer d ≥ 5" in Theorem 1.2 (§1), at the start of §2 and in the proof of Theorem 1.2 (§7), and our referee seat on its §§5–7 found no step that uses it (Paper A works only in dimension 4). The Lean agrees. Its construction is the theorem LowerTransfer.actual_prime_construction (i : ℕ) : PrimeConstruction (i+3) — every dimension from 3 up, with no hypothesis on i; the paper-facing wrapper prime_construction (d) (hd : 5 ≤ d) uses hd only to rewrite d − 3 + 3 = d; and the short assembly main_of_primeConstruction uses its 6 ≤ s only for side conditions that 4 ≤ s also gives. Our probe — that assembly copied verbatim with 4 ≤ s, fed actual_prime_construction (s − 4) — compiles to MainBounds 4 ∧ MainLimit 4, whose #print axioms lists only the three standard axioms, in OpenAI's own definitions:

t³/(log t)^2+ε ≤ r(4,t) ≤ C t³/(log t)² for every ε > 0 and all large t,

which takes Mattheus–Verstraëte's log power from 4 to 2 + o(1). The same route proves the s = 5 lower bound without Paper A. The library's construction starts at d = 3, so this route says nothing at s = 3, which is classical anyway (r(3,t) ≍ t²/log t: Ajtai–Komlós–Szemerédi above, Kim 1995 below). The r(4,t) statement itself is not new. Kaizhe Chen (arXiv:2610.15293, 11 October) and Qizhong Lin and Qiuyang Zhang (arXiv:2610.17891, 13 October) derived it on paper from OpenAI's result by passing one clique size down (Lin–Zhang through Shearer's 1995 independence bound; Chen through the recent proof of the Ajtai–Erdős–Komlós–Szemerédi bound, itself from two further OpenAI preprints), each using OpenAI's theorem as an input it did not re-prove (Lin–Zhang: "we take as an external input"). Neither mentions the Lean or the three-dimensional construction. What we add is that the statement is a kernel-checked theorem of OpenAI's library, by a different route: the construction in PG(3,q) directly, with no descent. We found no public statement of that (same search as above). Whether Paper B's text also goes through at d = 3 and 4 is a question for its authors; the formal proof does not need the text.

The bridge to Formal Conjectures (ours). Formal Conjectures' Erdos986.erdos_986 — for every s ≥ 3 there are c, C > 0 with classicalRamsey s k ≥ C k^s−1/(log k)^c eventually — has been research solved since 19 September, linking a Lean proof of Bradač's bound (plby/lean-proofs). Our Bridge986.lean copies FC's two definitions and its statement verbatim up to the namespace, an open SimpleGraph, an unused binder name and the theorem restated as a Prop, and proves: classicalRamsey s k equals OpenAI's ramsey s k in both of OpenAI's encodings; FC's statement holds at every s ≥ 4 by the library (c = s − 1 and C = 1, from ε = 1); and FC's whole statement is equivalent to its s = 3 instance. Every theorem in it lists only the standard axioms under #print axioms. Controls: a definition mutated to K_k+1 fails at the clique-size goal (a first version of this control failed on an unresolved name instead — it tested nothing and was redone); a planted sorry shows; and, as a sanity check, the library's s ≥ 4 route does not typecheck at s = 3. leanchecker in its default mode (re-checking the named module's own declarations against the compiled imports) exits 0 on both bridge files — Bridge986Main also carries the s = 4 probe's theorems — and a missing-module control exits 1. The bridge closes nothing — FC's statement already has a formal proof — and it compiles against OpenAI's Mathlib, not FC's pin. What it checks is that OpenAI's ramsey is the Ramsey number Formal Conjectures means.

What the seats found. Six tool-equipped AI referee seats, each briefed to refute and to quote what it objects to, plus four helper passes — every one served by Claude Opus 5.5 (per the session transcripts; per-agent counts in the bundle's seats/MODEL_RECEIPTS.txt) — read the two papers, the Lean and the sources. Paper B, §§2–4 (foundations, the description and validation theorems, the projection, the polynomial-method rich-line bounds, the learning step): holds with fixes, all expository. The projection silently assumes the smaller side is the point system (the Lean takes the dual explicitly); the high-moment bound, the hardest count in the learning step, is only sketched — the seat reconstructed it and found no error; and the prime hypothesis is essential and should be said to be (every polynomial degree stays below a constant times q^41/80, far under the characteristic q; over 𝔽_p² the characteristic would be √q and the argument would meet the Ellenberg–Hablicsek obstruction — the seat's small check: in characteristic 7 the non-planar surface z = x⁷ passes every flatness test). Paper B, §§5–7 and the entropy lower bound (§2): holds as read, given §§3–4. The marking step modifies Bradač's Claim 2.13 rather than transcribing it (the state is updated only at expensive positions, so the decoder can rebuild it; the seat simulated both scans on PG(3,5), PG(3,7) and PG(2,11) with no violation); the lower bound tolerates far more conditioning than the paper states; the ledger of every log σ closes; and the d ≥ 5 above. The formal statements: the standard Ramsey number with no junk-value escape (an empty set's sInf would make the lower bound false, not vacuous, and the Lean proves non-emptiness anyway); C is chosen before ε, as in the papers; the limit is a corollary of the bounds; and in the s ≥ 6 tree the message-length accounting charges dσ + O(1) per retained position and the extra domain cost only on O(q log q) positions — the place an entropy-compression proof is likeliest to hide a lost log σ is closed formally. Paper A (s = 5): one seat read §§1–3, §§5–8 (including the predictor setup, the rich-line geometry and the overlap lemmas) and §11 line by line and found everything it reached to hold. That seat, the seat on the s = 5 Lean and the formal-statement seat were all cut off by a session limit at 12:31 UTC before finishing, with all four helper passes; their partial reports are in the bundle as they stand. Paper A's §§9–10 (the Poisson score and the completion of the predictor) were read by no one, and §4, which states the predictor, was compared with its Lean statement by a helper pass but not read as mathematics. Sources: of the pin-cites the world seat checked — five to Bradač's v3, Mubayi–Verstraëte, Mattheus–Verstraëte, Bohman–Keevash, Nie–Wang, Ellenberg–Hablicsek, Ellenberg–Oberlin–Tao, Alon–Rödl — all match but one: Paper A cites Kollár's Theorem 2 for the positive-characteristic incidence estimate, which in arXiv:1405.2243v3 is Theorem 4 (Theorem 2 is over ℂ³). One wording note: Paper B attributes the ordered flag graph to Bradač's §2.5, where the flags are randomly ordered; sampling an i.i.d. stream is OpenAI's variant. Classical motivating citations (Dvir, Guth–Katz, Kim, Spencer and others) were not checked; Ajtai–Komlós–Szemerédi and Li–Rousseau–Zang could not be read (paywalled), and neither is used, since both papers reprove the upper bound.

Provenance. The construction the papers build on — Bradač's §2.5 with its s − 1 polynomial exponent — is the step Bradač's v3 credits to an internal OpenAI model; the OpenAI papers credit §2.5 to Bradač and do not mention that. As far as the world seat's search reached (arXiv, the problem page and forum, Formal Conjectures, the teorth database, Bradač's versions, OpenAI's earlier Ramsey publications), no public statement of a log power below 2s − 4 for any s ≥ 5 predates the 6 October release. The 24 September date is the authors' own and has no external anchor.

The world, 20 October. The problem page is unchanged since 21 June, still states 2s − 4 as the best lower log power, and cannot take new comments or proof claims (frozen since 6 October); Formal Conjectures links Bradač's bound; Bloom's 8 October post on the release lists #986 (added on 9 October) and says the proofs and formalizations were not checked. We found no public referee report, reproduction or rebuttal of the s − 2 + o(1) exponent (arXiv title and abstract sweeps, the problem page and forum, Formal Conjectures, the teorth database, Palomar, Hacker News, MathOverflow) — and two notes already build on it.

Labels. r(s,t) = t^s−1/(log t)^s−2+o(1) for every fixed s ≥ 5, with the upper bound at the AKS order: (d) computer-assisted — OpenAI's Lean, kernel-replayed here on the three standard axioms, statements matched to the challenges. The same for s = 4: (d), through OpenAI's library and our probe. The bridge to Formal Conjectures' statement: (d), ours. The papers' arguments as written: (c) — AI referee seats only, no human check on record, and parts of Paper A unread.

Whose. The theorems and both Lean proofs are OpenAI's (an internal model, per the release), on Bradač's construction. The r(4,t) statement was first written down, conditionally on OpenAI's, by Chen and by Lin–Zhang. Ours: the replay and its controls, the observation that the library proves s = 4 directly (found independently by two of our seats, the formal one and the one on Paper B's §§5–7) and the probe that checks it, the bridge, and the referee reports. Nothing here is a human referee's verdict.