Iterating the Gupta–Ndiaye–Norin–Wei method: a computer-verified bound R(k) ≤ 3.7698^(k+o(k))

Gupta, Ndiaye, Norin and Wei (arXiv:2407.19026) proved R(k) ≤ 3.7992^(k+o(k)) for diagonal Ramsey numbers by two applications of an inductive theorem (their Theorem 14), and reported an unverified AI-suggested third application giving 3.78233. We observe that the free function M can be optimised pointwise, that the best output exponent is the least solution of an explicit differential inequality, and that Theorem 14 needs only F in C^1 with locally Lipschitz derivative. We construct an explicit chain of eight applications and verify all hypotheses on the whole range 0 < λ ≤ 1 by interval arithmetic, with a hand-proved estimate as λ → 0. The verification was carried out twice, by independent programs (mpmath intervals, mean-value form; Arb balls, direct evaluation). This gives R(k) ≤ 3.76973^(k+o(k)) and confirms the 3.78233 bound. Numerically, iterating the optimal step converges to about 3.7690, suggesting this is close to the limit of the method in its present form. The deposit includes the preprint, code, certified data, and Lean 4 proofs of two auxiliary lemmas. AI use: the software, computations and an initial draft were produced with the AI assistant Claude (Anthropic) under the author's direction.