Gupta, Ndiaye, Norin and Wei prove R(k, k) ≤ 3.7992^(k+o(k)), and print one more iteration of their optimisation, proposed by ChatGPT 5.6 Sol, as "preliminary, unverified": if it held, the base would drop to 3.78233. Decided here with exact interval arithmetic, on the paper's own Theorem 14 and the region its Theorem 1 already proves: it holds. The inequality the theorem needs is true at every λ in (0, 1], with a witness chosen here, so R(k, k) ≤ 3.7823287755…^(k+o(k)) follows from the paper as written.
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). 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.
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-certificate.json — one standard-library file, 7.5 s here · python3 instruments/gnnw/battery.py — 18 checks, 5 forgeries refused.
base of the bound
3.7823
From the 3.7992 the paper proves; c = 3.78232877553731…
slack as λ → 0
6.31·10⁻⁵
Per unit λ: thin. Moving G_AI's linear coefficient from −0.3864 to −0.3870 already breaks it (a forgery the battery refuses).
intervals decided
415
79 on (0, 0.01], 336 on [0.01, 1].
seconds
7.5
The whole decision, re-run at every build of this page.
§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
Four hundred intervals, every rounding outward
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 · limits
What this does and does not say
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. A single program by one author, with its controls; a second independent implementation, or the authors' own check, is the next step. The verifier is one file with no dependencies, so anyone can run it.