Erdős problem #554 — wave 6a audit

Access date: 2026-07-27 UTC Standalone verifier: runs/erdos554_wave6a_verify.py

Claim labels

Every substantive claim below is marked as requested:

• (a) elementary-rigorous: proved here from definitions, or a direct live-page observation.
• (b) rigorous-modulo-named-theorem: depends on the cited primary source.
• (c) plausible/structural-unverified: a search miss, heuristic, or explicitly non-rigorous estimate.
• (d) computational-only: established by the reproducible computation/certificate, not by a supplied paper proof.

Step 0: authoritative live-page check

(a) I fetched the live page through the Bright Data browser path, not datacenter curl. The response was the rendered problem page titled “554 | Erdős Problems”; the page said it was last edited 08 February 2026.

(a) Verbatim live statement:

Let \(R_k(G)\) denote the minimal \(m\) such that if the edges of \(K_m\) are \(k\)-coloured then there is a monochromatic copy of \(G\). Show that \[ > \lim_{k\to\infty}\frac{R_k(C_{2n+1})}{R_k(K_3)}=0 > \] for any \(n\geq 2\).

(a) The displayed status was OPEN. The page had 0 comments, 0 claimed proofs, “Interested in collaborating: None”, and “Currently working on this problem: None”. The additional markers “looks difficult”, “looks tractable”, “results could be formalisable”, and “working on formalising” were also all “None”; the two likes were woutercvb and Alfaiz. Thus none of the mandatory stop conditions applied.

(b) The live page calls this a problem of Erdős and Graham, cites Erdős’s 1981 paper On the combinatorial problems which I would most like to see solved, and says the problem remains open even for \(n=2\), i.e. for \(C_5\).

Results listed on the live page

Here and below I use \(\ell\) for the page’s \(n\), to avoid confusing cycle half-length with graph order.

(b) The page lists Schur’s bounds

for an absolute \(C>0\), and records Erdős’s conjecture \(R_k(K_3)\leq C^k\) for some absolute \(C\).

(b) It lists the Bondy–Erdős / Erdős–Graham bounds

(b) It says Jenssen and Skokan proved the lower bound sharp for fixed \(k\) and all sufficiently large \(\ell\). This agrees with Theorem 1.1 of Jenssen–Skokan, arXiv:1608.05705, which states

for fixed \(k\) and sufficiently large \(\ell\).

(b) It says Day and Johnson proved that, for fixed \(\ell\), some \(c_\ell>0\) satisfies

for all sufficiently large \(k\). This is Theorem 4 of Day–Johnson, arXiv:1602.07607.

(b) Finally, it lists the current upper bound

and hence \(R_k(C_{2\ell+1})\leq (C\ell)^k(k!)^{1/\ell}\) for a suitable absolute \(C>0\). This is Theorem 1.1 of Axenovich–Cames van Batenburg–Janzer–Michel–Rundström, arXiv:2510.17981, now published as JCTB 179 (2026), 293–298.

Primary-source literature audit

(b) Ageron, Casteras, Pellerin, Portella, Rimmel, and Tomasik construct Schur templates satisfying

Since \(S(t)\leq R_t(K_3)-2\), iteration gives

for some \(c_0>0\). See Corollary 2.9 of New lower bounds for Schur and weak Schur numbers, arXiv:2112.03175. This improves the older \(3.199\ldots\) base quoted in Day–Johnson.

(b) The February 2026 preprint Attwa–López Vidal–Morris, arXiv:2602.02155 is not a new lower bound in the parameter regime of #554: its headline asymptotic lets clique size \(t\to\infty\) with the number of colours fixed, whereas #554 fixes \(t=3\) and sends the number of colours to infinity.

(b) The recent paper Suk–Zeng, arXiv:2411.15649 explicitly still treats whether \(R_k(K_3)\) is merely exponential as open and relates it to an ordered 3-uniform Ramsey problem; it does not supply the denominator estimate needed here.

(b) The finite fact \(R_3(C_5)=17\) is known, but is not an asymptotic advance on #554. A primary source is Yang and Rowlinson, On the Third Ramsey Numbers of Graphs with Five Edges, JCMCC 11 (1992), 213–222; their proof uses computer enumeration.

(c) Targeted searches for the exact quotient, for papers citing the 2025 odd-cycle upper bound, and for work after the live page’s February 2026 edit found no primary source claiming a proof or falsification of #554. This is only a documented search miss, not a theorem that no such source exists.

Why the best published bounds do not meet

Put

(a), using the named results in (b). Combining the strongest verified lower bound for \(A_k\) above with the current upper bound for \(B_{k,\ell}\) gives only

For each fixed \(\ell\),

Thus this upper estimate for the quotient becomes worse than useless; this calculation does not say that the actual quotient grows.

(a) The factorial upper bound on \(A_k\) cannot be used in the denominator of an upper bound for \(B_{k,\ell}/A_k\). A denominator lower bound is needed. Conversely, the Day–Johnson exponential lower bound on \(B_{k,\ell}\) constrains possible cycle bounds but does not upper-bound the quotient.

(a) The Axenovich et al. proof exposes the precise loss. Its Lemma 2.1 bounds a \(k\)-local colouring by

For a \(C_{2\ell+1}\)-free colour graph they take \(\chi=4\ell-2\). The \(k^{1/\ell}\) factor per colour comes from selecting one of \(\ell\) breadth-first layers whose weight growth is at most \(k^{1/\ell}\). No result in that paper replaces this \(k\)-dependent growth factor by a constant for fixed \(\ell\).

A clean sufficient reduction

(a) Product lemma for triangles. For all positive integers \(p,q\),

Indeed, take a triangle-free \(p\)-colouring on \(A_p-1\) vertices and replace every vertex by a triangle-free \(q\)-coloured clique on \(A_q-1\) vertices, using disjoint palettes inside and between fibres. A monochromatic triangle would either lie in one fibre or project to one in the first factor.

(a) Colour-index-gap reduction. Fix \(\ell\geq2\). It would suffice to prove that there is an integer function \(s=s(k)\) with

for all sufficiently large \(k\). To see this, set \(p=k-s(k)\). The product lemma and the elementary construction \(A_t-1\geq2^t\) give

This proves #554 from (IG) without assuming that the exponential growth rate of \(A_k\) is finite.

(a) Alternative sufficient lemma. The verified Schur-template base gives another concrete route: for each fixed \(\ell\), an upper bound

would immediately imply the desired limit. Neither (IG) nor (EB) follows from current results. These are sufficient targets, not claimed equivalent reformulations.

Reproducible finite certificates

Explicit four-colour \(K_{17}\) of odd girth at least seven

(a) Start with the red \(C_5\) and its blue complementary \(C_5\) on \(K_5\), rooted at one vertex. This is a \((5,5)\) rooted-round-colouring. Implementing Day–Johnson Lemma 5 once produces a \((7,5,9)\) rooted-round-colouring of \(K_9\); applying it again to the remaining 5-round colour produces a \((7,7,9,9)\) rooted-round-colouring of \(K_{17}\).

(d) The verifier checks every edge, every asserted round partition, all \(\binom{17}{3}=680\) vertex triples, and all

undirected \(5\)-cycles. It finds no monochromatic \(C_3\) or \(C_5\). In lexicographic edge order, the colour-byte SHA-256 is 2a1969473bdf7e0f0a0d9da3c18469ad5a6b56cea0d690c9a060e472712ff17b.

Explicit five-colour \(K_{68}\) with no monochromatic \(C_5\)

(a) Replace every vertex of the verified \(K_{17}\) colouring by a one-coloured \(K_4\), using the four old colours between fibres and a new colour within fibres. A \(C_5\) in the new colour cannot fit in a four-vertex fibre. A \(C_5\) in an old colour would project to a closed odd walk of length five in the \(K_{17}\) factor, hence would contain a \(C_3\) or \(C_5\), which the factor avoids. Therefore

(d) A separate bounded DFS checks every colour graph of this \(K_{68}\) certificate for a simple \(C_5\). Its colour-byte SHA-256 is 7068b357fce8ba9e19ee7d923396b3cdf653eb8c6121c4cd75caea8514543ee1.

(a) Iterating the same product gives the explicit Day–Johnson \(C_5\)-free construction

The verifier recomputes the following values:

(a) This construction has exponential base \(17^{1/4}=2.0305\ldots\), far below the currently certified triangle base \(380^{1/5}=3.2806\ldots\). It is a checked reconstruction of known Day–Johnson machinery, not a new asymptotic lower bound.

Exact two-colour check

(d) The verifier independently certifies

For \(K_8\), Glucose supplies a model and the verifier directly checks all 672 undirected \(C_5\)'s. For \(K_9\), the Boolean CNF has 36 edge variables and \(2\cdot1512=3024\) clauses. Glucose emits a DRUP proof; the from-scratch watched-literal checker in the standalone script validates every step independently. In the recorded run the proof had 1917 additions and 2601 deletions and SHA-256 6bc0bf11719becc6b33d3b781a79f87721e6a0d406e86032b7405ef37ce3b74b.

Failed finite attack and computation wall

(a) A direct one-hot SAT encoding of a three-colour \(C_5\)-free \(K_{17}\) has 408 Boolean variables. Exact-one constraints contribute 544 clauses, and the 74,256 undirected \(C_5\)'s contribute \(3\cdot74,256=222,768\) clauses, for 223,312 clauses in total.

(d) CaDiCaL did not resolve this CNF in a 60-second probe. Fixing the incident colour-degree case \((6,5,5)\) at one vertex also exceeded 60 seconds. Adding the necessary condition that a chosen densest colour has at least 46 edges produced a 1,376-variable, 233,461-clause totalizer encoding and likewise did not resolve in 60 seconds. These timeouts are not evidence of satisfiability or unsatisfiability.

(b) Yang–Rowlinson’s 1992 proof of \(R_3(C_5)=17\) enumerates dense maximal \(C_5\)-free graphs and compatible two-colour complements rather than attacking the raw labelled CNF. Reproducing that historical enumeration with modern canonical augmentation, or using symmetry-aware SAT plus a checkable DRAT/LRAT proof, is the appropriate finite computation.

(c) A realistic planning allowance for rebuilding that already-known \(K_{17}\) enumeration is roughly 10–100 core-hours plus certificate checking and storage; this is a deliberately broad engineering estimate, not a proved runtime bound. Spending it would only reprove a known finite value and would not address the uniform \(k\to\infty\) step in #554.

(a) No finite table of \(R_k(C_5)\) values can establish the requested limit by itself. The exact missing ingredient is uniformity: a structural theorem yielding an unbounded colour saving such as (IG), or a fixed-base exponential cycle upper bound such as (EB). The present local-neighbourhood method loses \(k^{k/\ell}\), while the best certified denominator lower bound is only \(3.2806^k\); that is the precise quantitative impasse.

Reproduction

(a) From the repository root:

python runs/erdos554_wave6a_verify.py

(d) On this VM the complete run took about 23 seconds and ended with ALL CHECKS PASSED. The script uses only the Python standard library plus the installed python-sat package; it regenerates rather than trusts the SAT proof and independently checks that proof.

WALL: The live problem is open with no claimant or worker; current bounds miss by a \(k^{k/\ell}\) factor, and the report proves a precise colour-index-gap reduction plus fully checked finite certificates, but no uniform lemma establishing the required limit.