Diagonal Ramsey below 3.7992: 3.7823, then 3.77213…
Gupta, Ndiaye, Norin and Wei prove R(k, k) ≤ 3.7992^(k+o(k)) and print one more round of their optimisation, proposed by ChatGPT 5.6 Sol, as "preliminary, unverified": 3.78233. Decided here on the paper's own Theorem 14, by two independent programs: it holds. The paper adds that "further improvements by performing additional iterations are possible"; five more rounds, each proposed here by a float optimiser and each decided in the region the round before it establishes, reach R(k, k) ≤ 3.7721307629…^(k+o(k)). Both numbers decide the paper's own iteration; neither is the best known bound — lower ones appeared in September 2026 and are not checked here (§5).
The paper: arXiv 2407.19026v2 (29 August 2026), pinned by sha256 in corpus/gnnw. What is decided is the numerical hypothesis of its Theorem 14 for this F; the theorem itself, Lemma 15 and Theorem 1 are the authors' (the paper reports its main results formalised in Lean). Not the record: R(k, k) ≤ 3.769^(k+o(k)) (Neisler, Shin and Sukhatankar, kernel-checked in Lean by its authors, 3 September 2026) and R(k, k) ≤ 3.69507^k (Lu and Wang, arXiv 2609.14525, 13 September 2026) are both lower than anything on this page; neither is checked here. Published, not peer-reviewed, not independently rerun. Nothing has been sent to the authors.
tl;dr
The finding.CERTIFIED. For F(λ) = (1+λ)ln(1+λ) − λ ln λ + G_AI(λ), with the paper's G_AI, a continuous M chosen here and Y taken from the region the paper's proved bound F₀.₀₃ gives (Lemma 15), all four conditions of Theorem 14 hold on (0, 1]. Its conclusion is R(k, ℓ) ≤ e^(F(ℓ/k)k + o(k)), and at ℓ = k the base is e^F(1) = 4·e^G_AI(1) = 3.78232877553731162174…; the paper's 3.78233 is its rounding. Five more rounds, CERTIFIED: the bases 3.782328 → 3.775471 → 3.772573 → 3.772275 → 3.772151 → 3.772130, the last 3.77213076290036638924…. A second program, written apart in another language and arithmetic, certifies every round and agrees to 25 digits.
The mechanism. The inequality holds with little room: its slack is about 6.31·10⁻⁵·λ as λ → 0 and 6.20·10⁻⁵·λ near λ = 0.93. It is decided on 415 intervals of λ, each enclosed in 40-digit decimal arithmetic with every rounding outward: below λ = 0.01 the slack divided by λ with its ln λ terms cancelled by hand, above it a mean-value bound with the derivative written out.
Check it.python3 verify/verify_gnnw_gai.py certs/gnnw-chain-certificate.json — one standard-library file, 175.8 s here · node instruments/gnnw/second.js certs/gnnw-chain-certificate.json — the second program, 35 min · python3 instruments/gnnw/battery.py — 27 checks, 7 forgeries refused.
base, the remark's round
3.7823
Printed as unverified; decided here. c = 3.78232877553731…
base, five rounds more
3.77213…
c = 3.77213076290036…, each round in the region of the one before; rounded, 3.7722, never 3.7721.
intervals decided
4,059
By the first program; the second, with its coarser method, used 181,977.
implementations
2
Python and Decimal with a written derivative; JavaScript and dyadic intervals with monotone bounds. They agree to 25 digits.
§1 · the claim
One more iteration, printed as unverified
We asked ChatGPT 5.6 Sol to perform an additional iteration of optimization in Theorem 14. A preliminary, unverified iteration suggests that Theorem 1 holds with G_AI(λ) = e^{−λ}(−0.3864λ + 0.8347λ^2 − 2.0156λ^3 + 2.7171λ^4 − 1.7541λ^5 + 0.4522λ^6). If verified it would improve the upper bound on the diagonal Ramsey numbers to R(k, k) ≤ (3.78233 . . .)^{k+o(k)}. Further improvements by performing additional iterations are possible, but we expect that lowering the base of the exponent below 3.7 and, likely, even below 3.75 would require new ideas.Gupta, Ndiaye, Norin and Wei, arXiv 2407.19026v2, after Remark 17
Their method turns a known upper bound on the off-diagonal numbers R(k, ℓ) into a better one: Theorem 14 takes a function F with F′ > 0, functions M, X, Y into (0, 1) with M continuous, X(λ) = (1 − e^−F′(λ))^(1/(1−M(λ)))·(1 − M(λ)), the pair (X(λ), Y(λ)) in the region R of pairs the known bounds allow, and
and concludes R(k, ℓ) ≤ e^(F(ℓ/k)k + o(k)). Their Theorem 1 is two rounds of this, ending at F₀.₀₃ and the base 3.7992. The remark's G_AI is a third round, and the remark names neither the M nor the Y that go with it.
§2 · the witness
An M, a Y, and an inequality that holds everywhere
Y is not chosen: it is Lemma 15's function Y_f for f = F₀.₀₃, which the paper's Remark 17 places in R — the region Theorem 1 already proves. It has three branches, where X is above b = B(1), between a = A(1) and b, and below a, with A(t) = e^−f′(t) and B(t) = e^(t f′(t) − f(t)); each is solved for its parameter t by an interval bracket.
M is chosen: M(λ) = λ·m(λ), m piecewise linear through 101 rational values — at each node the value that makes the slack largest, and at 0 the root μ = 1.505717 of 1/μ + 1/(e^0.3864 + μ) = 1, which maximises the slack's limit. Any continuous M into (0, 1) that passes is a witness; this one passes with the margin drawn below.
The slack of Theorem 14's inequality divided by λ, as decided: flat at 6.31·10⁻⁵ for small λ, lowest at 6.20·10⁻⁵ near λ = 0.93, and never below zero. The tight stretches — the flat left end and three dips between 0.6 and 0.95 — are where a coarser witness, or a slightly more ambitious G, would fail.
§3 · the decision
The remark's round: four hundred intervals
Below λ = 0.01. F carries −λ ln λ and the two logarithms carry +½ λ ln λ each (M ≈ 1.5λ, and Y through t ≈ 3λ); cancelled by hand, slack/λ is a smooth function of λ, enclosed on intervals that contain 0, with ln(1+z)/z and ln(1−z)/z bracketed by their series. 79 intervals, the smallest lower bound 4.72·10⁻⁶.
From 0.01 to 1. On each piece of m, slack on [a, b] lies inside slack(midpoint) plus slack′([a, b]) times half the width; slack′ is written out, with d log Y / d log X = −1/t, −1 or −t on the three branches (the paper's Appendix A). 336 intervals.
Along the way. F′ > 0 (at least 0.756), M below 0.3928, X in (0, 1); and for f = F₀.₀₃ the hypotheses of Lemma 15: strictly concave, increasing, A < B.
The controls. The derivative agrees with a central difference, the tail form with the direct slack, Y with an independent float solver. Moving the linear coefficient to −0.3870, starting M with slope 1.2, lowering the sixth coefficient by 0.002, letting M reach 1, or a proposer that lies about a branch parameter: each is refused. GNNW's own F₀.₀₃ passes in its own region.
§4 · further rounds
Five more rounds, each in the region of the last
Once F is established, it is a better bound on R(k, ℓ) than F₀.₀₃, and Lemma 15 turns it into a larger region — provided it is strictly concave, increasing, and 2F′(1) − F(1) > 0, which both programs decide on intervals before using it. Theorem 14 can then be applied again. Each new F is h + q(λ)e^−λ with q a polynomial of degree 9, found by a float optimiser here: minimise q(1) while the slack stays at least 5·10⁻⁵·λ on 215 points, with M chosen as before. The optimiser only proposes; every round is decided like the first. Round 1 is the remark's, in the region of F₀.₀₃; round k is in the region of round k − 1.
round
base e^F(1)
second program
1
3.7823287755
3.7823287755
2
3.7754710215
3.7754710215
3
3.7725734617
3.7725734617
4
3.7722750853
3.7722750853
5
3.7721515782
3.7721515782
6
3.7721307629
3.7721307629
In floats, the rounds converge: degree 6 settles near 3.7732 and degree 9 near 3.77213, so further rounds of this kind buy almost nothing. The authors expect that going below 3.75 would need new ideas; nothing here disagrees. The two newer upper bounds of §5, both with lower bases, change the method rather than add rounds: one collapses the iteration into a single self-consistent system over free-form rate functions, the other descends through retained sets.
§5 · limits
What this does and does not say
It is not the record. 3.7823 and 3.77213… decide the paper's own iteration. Two upper bounds on R(k, k) with lower bases than these appeared in September 2026: 3.769^(k+o(k)), by C. Neisler, R. M. J. Shin and S. Sukhatankar — a self-consistent bootstrap of the same book algorithm, with the whole proof, including the decimal bound R(k, k) ≤ 3.7690^k for all large k, kernel-checked in Lean 4 by its authors (wamlat/RamseyLean-bootstrap, doi:10.5281/zenodo.22263823, 3 September 2026); and 3.69507^k for all sufficiently large k, by Z. Lu and S. Wang, “Retained-Set Descent for Diagonal Ramsey Numbers” (arXiv 2609.14525, 13 September 2026; the arXiv comment points to a Lean 4 formalization and Python certificate checks). Neither is checked here; their public pages are pinned in corpus/sources/ramsey.
It rests on the paper. Theorem 14, Lemma 15 and Theorem 1 are the authors' and are used, not re-proved. What was missing, the numerical hypothesis for G_AI and a witness M, is supplied and decided here.
It is the paper's own next step. The authors expect that going below 3.75 would need new ideas. The certificate HorizonMath credits with 3.6961 does not satisfy this theorem; it is decided on the HorizonMath page.
It is not yet reviewed. Two programs agree, but they share an author and a reading of the paper; the authors' own check is the next step. The first verifier is one file with no dependencies, so anyone can run it.
Each round rests on the one before. Round k uses the bound round k − 1 establishes; the chain is only as good as its first link, the paper's Theorem 1.