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
\[ C^k\ll R_k(K_3)\ll k! \]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
\[ \ell 2^k+1\leq R_k(C_{2\ell+1})\leq 2\ell(k+2)!. \](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
\[ R_k(C_{2\ell+1})=\ell 2^k+1 \]for fixed \(k\) and sufficiently large \(\ell\).
(b) It says Day and Johnson proved that, for fixed \(\ell\), some \(c_\ell>0\) satisfies
\[ R_k(C_{2\ell+1})\geq 2\ell(2+c_\ell)^{k-1} \]for all sufficiently large \(k\). This is Theorem 4 of Day–Johnson, arXiv:1602.07607.
(b) Finally, it lists the current upper bound
\[ R_k(C_{2\ell+1})\leq (4\ell-2)^k k^{k/\ell}+1, \]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
\[ S(t+5)\geq 380S(t)+148. \]Since \(S(t)\leq R_t(K_3)-2\), iteration gives
\[ R_k(K_3)\geq c_0\gamma^k,\qquad \gamma=380^{1/5}=3.280625976051\ldots \]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_k:=R_k(K_3),\qquad B_{k,\ell}:=R_k(C_{2\ell+1}). \](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
\[ \frac{B_{k,\ell}}{A_k} \leq \frac{(4\ell-2)^k k^{k/\ell}+1}{c_0\gamma^k}. \]For each fixed \(\ell\),
\[ \frac1k\log\!\left( \frac{(4\ell-2)^k k^{k/\ell}}{\gamma^k} \right) = \log\frac{4\ell-2}{\gamma}+\frac{\log k}{\ell} \longrightarrow+\infty. \]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
\[ \chi^k k^{k/\ell}. \]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\),
\[ A_{p+q}-1\geq (A_p-1)(A_q-1). \]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
\[ s(k)\to\infty,\qquad k-s(k)\to\infty, \qquad B_{k,\ell}\leq A_{k-s(k)} \tag{IG} \]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
\[ \begin{aligned} \frac{B_{k,\ell}}{A_k} &\leq \frac{A_p}{1+(A_p-1)(A_{s(k)}-1)}\\ &\leq \frac1{A_{s(k)}-1}+\frac1{A_p-1}\\ &\leq 2^{-s(k)}+2^{-p}\longrightarrow0. \end{aligned} \]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
\[ B_{k,\ell}\leq C_\ell(\gamma-\varepsilon_\ell)^k \quad(\varepsilon_\ell>0) \tag{EB} \]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
\[ \binom{17}{5}\frac{4!}{2}=74\,256 \]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
\[ R_5(C_5)\geq69. \](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
\[ R_k(C_5)\geq 4\cdot 2^c\cdot17^m+1, \qquad k-1=4m+c,\quad 0\leq c<4. \]The verifier recomputes the following values:
| \(k\) | certified lower bound for \(R_k(C_5)\) |
|---:|---:|
| 1 | 5 |
| 2 | 9 |
| 3 | 17 |
| 4 | 33 |
| 5 | 69 |
| 6 | 137 |
| 7 | 273 |
| 8 | 545 |
| 9 | 1157 |
| 10 | 2313 |
| 11 | 4625 |
| 12 | 9249 |
| 13 | 19653 |
(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
\[ R_2(C_5)=9. \]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.