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

Abstract

Gupta, Ndiaye, Norin and Wei (GNNW) recast the Campos–Griffiths–Morris–Sahasrabudhe method as an inductive theorem that turns a known bound on off-diagonal Ramsey numbers into a better one. With two applications they obtained R(k) ≤ (3.7992...)^(k+o(k)). They also reported an unverified, AI-suggested third application giving 3.78233.... We make three observations about their framework. (i) The free function M can be optimised pointwise. (ii) For a fixed input, the best output exponent is the least solution of an explicit first-order differential inequality. (iii) GNNW's Theorem 14 needs only F in C^1 with locally Lipschitz derivative. We then construct an explicit chain of eight applications and verify every hypothesis by interval arithmetic on the whole range 0 < λ ≤ 1, with a hand-proved estimate covering λ → 0. The verification was done twice, with independent code, libraries and enclosure strategies. This proves R(k) ≤ 3.76973^(k+o(k)), and in particular confirms GNNW's 3.78233. Numerically, iterating the optimal step converges to about 3.7690, which suggests this is close to the limit of the GNNW method in its present form. Code, certified data and Lean files: doi:10.5281/zenodo.23895553. AI use: the software, computations and a first draft were produced with the AI assistant Claude (Anthropic) under the author's direction.

Keywords