Erdős problem 609 — wave 6f

Date: 2026-07-27 (UTC)

0. Mandatory live-page gate

I fetched both the actual problem page and its discussion thread through the

Bright Data browser path on 2026-07-27. The first two proxy connections were

closed upstream; a clean retry loaded both pages and saved screenshots. I did

not infer the statement from tracker metadata or from the problem number.

Live page: <https://www.erdosproblems.com/609>

Verbatim current statement

> Let \(f(n)\) be the minimal \(m\) such that if the edges of

> \(K_{2^n+1}\) are coloured with \(n\) colours then there must be a

> monochromatic odd cycle of length at most \(m\). Estimate \(f(n)\).

The live page fields are:

• status: OPEN;
• claimed proofs: 0;
• interested in collaborating: None;
• currently working on this problem: None;
• formalised statement: No;
• comments: 1.

Thus none of the mandatory stop conditions applies.

The page's complete mathematical remarks are:

> A problem of Erdős and Graham. The edges of \(K_{2^n}\) can be

> \(n\)-coloured to avoid odd cycles of any length. It can be shown that

> \(C_5\) and \(C_7\) can be avoided for large \(n\).

>

> Chung [Ch97] asked whether \(f(n)\to\infty\) as \(n\to\infty\). Day and

> Johnson [DaJo17] proved this is true, and that

> \[ > f(n)\geq 2^{c\sqrt{\log n}} > \]

> for some constant \(c>0\). The trivial upper bound is \(2^n\).

>

> Girão and Hunter [GiHu24] have proved that

> \[ > f(n)\ll\frac{2^n}{n^{1-o(1)}}. > \]

> Janzer and Yip [JaYi25] have improved this to

> \[ > f(n)\ll n^{3/2}2^{n/2}. > \]

> See also the entry in the graphs problem collection.

The sole comment, by zach hunter at 12:25 on 22 October 2025, says:

> today a very very lovely paper came out, which dramatically improves the

> upper bounds to some related problems:

> https://arxiv.org/abs/2510.17981. and its only 4 pages!!

It makes no proof claim about Problem 609. Section 2 below checks that paper

rather than inferring relevance from the comment.

1. Scope and claim labels

Write \(L(k)=f(k)\). Equivalently, \(L(k)\) is the maximum, over all

\(k\)-edge-colourings of \(K_{2^k+1}\), of the least length of a

monochromatic odd cycle. The maximum exists because every such colouring

has a monochromatic odd cycle. (a)

The labels required in the task are used as follows:

• (a) elementary-rigorous: proved here without an external theorem;
• (b) rigorous-modulo-named-theorem: the deduction is explicit and the

named primary source was checked;

• (c) plausible/structural-unverified: not used as a conclusion;
• (d) computational-only: finite exhaustive claim checked by the

companion code and proof traces.

The concrete result of this run is the exact initial table

The first two entries are elementary (a). The new output of this run is

the proof-carrying exhaustive determination \(f(3)=5\), conservatively

labelled (d). This is finite progress only; it does not settle the

asymptotic estimation problem.

2. Primary-source literature audit

Original question and Chung's formulation

Erdős and Graham, On partition theorems for finite graphs, in *Infinite and

Finite Sets* (Keszthely, 1973), Colloquia Mathematica Societatis János Bolyai

10 (1975), 515–527, is available in the

Rényi archive. Section 6,

question (iii), asks for the least odd circuit forced when the edges of

\(K_{2^n+1}\) are decomposed into \(n\) subgraphs, after observing the

\(K_{2^n}\) bipartite decomposition. This verifies the attribution and

parameters in the live statement. (b)

Fan Chung, Open problems of Paul Erdős in graph theory, Journal of Graph

Theory 25 (1997), 3–36, DOI

10.1002/(SICI)1097-0118(199705)25:1<3::AID-JGT1>3.0.CO;2-R,

is available from the

author's page. Problem 75 defines the

same \(f(n)\) and explicitly asks whether it is unbounded. (b)

Lower bound

Day and Johnson, Multicolour Ramsey Numbers of Odd Cycles, Journal of

Combinatorial Theory B 124 (2017), 56–63, DOI

10.1016/j.jctb.2016.12.005,

arXiv:1602.07607, prove in Theorem 2

that arbitrarily large odd girth occurs. Their Corollary 6 gives, after

inversion of its displayed parameter relation,

This verifies the live page's lower bound. (b)

Direct upper bounds

Girão and Hunter, *Monochromatic odd cycles in edge-coloured complete

graphs*, arXiv:2412.07708, Theorem 1.2,

prove that for every fixed \(\varepsilon>0\) and all sufficiently large \(k\),

which is the page's \(2^k/k^{1-o(1)}\) bound. (b)

Janzer and Yip, Short monochromatic odd cycles,

arXiv:2506.14910, now published in

Mathematical Proceedings of the Cambridge Philosophical Society, DOI

10.1017/S0305004125101801,

prove in Theorem 1.4 that

Their more general Theorem 1.5 gives a cycle of length at most

\(4k^{3/2}\delta^{-1/2}\) in \(K_{(1+\delta)2^k}\); setting

\(\delta=2^{-k}\) gives the stated bound at \(2^k+1\) vertices. (b)

The paper in the comment

Axenovich, Cames van Batenburg, Janzer, Michel, and Rundström,

An improved upper bound for the multicolour Ramsey number of odd cycles,

arXiv:2510.17981, exists and proves

Its Theorem 1.2 also controls a short odd cycle when the complete graph has

more than \(b^k\) vertices for fixed \(b>2\). Crucially, the authors

explicitly remark that this gives no nontrivial result for the

Erdős–Graham regime \(2^k+1\), where \(b-2\) is exponentially small. Thus

the comment is accurately described as concerning related problems; it

does not improve the current direct upper bound for \(L(k)\). (b)

Exact-title, exact-phrase, citation, arXiv, and publisher searches through

2026-07-27 found no later primary source improving either side of

This last sentence is an honest report of the searches performed, not a

theorem that no unindexed result exists.

3. Elementary baseline and the first two values

Bipartition-vector lemma

If all \(k\) colour graphs in an edge-colouring of \(K_N\) are bipartite,

choose a bipartition of every component of every colour graph. Label each

vertex by its \(k\) side bits. The endpoints of an edge of colour \(i\)

differ in bit \(i\), so two vertices can never have the same full label.

Consequently \(N\le 2^k\). Conversely, labelling the vertices of

\(K_{2^k}\) by binary strings and colouring an edge by any coordinate in

which its endpoints differ makes every colour graph bipartite. (a)

It follows that every \(k\)-colouring of \(K_{2^k+1}\) has a monochromatic

odd cycle, and the exact elementary upper bound from this argument is

The live page's phrase “the trivial upper bound is \(2^n\)” is therefore an

asymptotic suppression of the \(+1\), not a literal small-\(n\) inequality:

the exact value \(f(2)=5>4\) below is a counterexample to the literal

reading. (a)

For \(k=1\), \(K_3\) itself is a monochromatic triangle, so \(f(1)=3\).

(a)

For \(k=2\), colour the edges of a 5-cycle red and its complement (also a

5-cycle) blue. There is no monochromatic triangle, hence \(f(2)\ge5\).

The bipartition-vector lemma forces some monochromatic odd cycle in every

2-colouring of \(K_5\), and such a cycle has length at most 5. Therefore

This proof is elementary and is also checked directly by the companion

program. (a)

4. Exact computation: \(f(3)=5\)

4.1 Explicit lower certificate

On vertices \(0,\ldots,8\), use the following symmetric colour matrix; the

diagonal dots are not edges:

The from-scratch cycle enumerator checks all 84 triangles and finds no

monochromatic one. It also checks all 1512 undirected 5-cycles and finds

respectively \(6,6,3\) in colours \(0,1,2\). Thus the colouring has odd

girth exactly 5, proving

The finite verification of (3) is labelled (d).

4.2 Exact upper encoding

Suppose, for contradiction, that a 3-colouring of \(K_9\) has no

monochromatic \(C_3\) or \(C_5\). For every edge \(e\) and colour

\(c\in\{0,1,2\}\), introduce a Boolean variable \(x_{e,c}\).

For each of the 36 edges, the encoding has one “at least one colour” clause

and three pairwise “at most one colour” clauses. For every simple

\(\ell\)-cycle \(C\), where \(\ell\in\{3,5\}\), and every colour \(c\), add

The number of undirected \(\ell\)-cycles in \(K_9\) is

so there are 84 triangles and 1512 five-cycles. The CNF therefore has

The correspondence is exact: satisfying assignments are precisely the

3-edge-colourings of \(K_9\) avoiding monochromatic \(C_3,C_5\). (a)

4.3 Complete symmetry normalization

At vertex 0, let \((d_0,d_1,d_2)\) be the three colour degrees. Permute the

colour names so \(d_0\ge d_1\ge d_2\), then permute vertices \(1,\ldots,8\)

so the incident edges of each colour occur in consecutive blocks. Every

hypothetical colouring is thereby mapped to exactly one of the following

ten degree patterns:

These are simply all nonincreasing triples of nonnegative integers summing

to 8. Adding the eight normalized incident-edge unit clauses gives 4940

clauses per case. Thus unsatisfiability of all ten cases is a complete

exhaustion, not an assumed symmetry heuristic. (a)

There is also an elementary pruning observation: in a colouring avoiding

\(C_3,C_5\), every colour degree at every vertex is at most 4. Indeed, the

edges within five neighbours joined to \(v\) in colour \(c\) cannot have

colour \(c\); the red/blue \(K_5\) argument proving (2) then produces a

triangle or 5-cycle in one of the other two colours. Thus only the first

four patterns in (7) are actually needed. The verifier nevertheless checks

all ten, avoiding dependence on this pruning in the computational result.

(a)

4.4 Proof-carrying UNSAT check

For each normalized CNF:

1. CaDiCaL 1.9.5 independently returns UNSAT.

2. Glucose 4.2 returns UNSAT and emits a DRUP trace.

3. A separate watched-literal checker, implemented from scratch in the

companion file, verifies every RUP clause addition.

4. Proof deletion hints are ignored by retaining those already proved

clauses. This is sound: retaining logical consequences only strengthens

the unit-propagation database.

5. The checked derivation ends with the empty clause.

The proof checker does not trust the solver's UNSAT answer. For a proposed

clause \(C\), it assigns the negation of every literal of \(C\) and performs

unit propagation. A conflict proves that the current formula entails

\(C\). Induction over the checked additions, ending in the empty clause,

proves unsatisfiability of the original normalized CNF. (d)

The clean run checked 52,718 DRUP lines in total: 10,575 RUP additions and

42,143 deletion hints. Per-case results were:

| degree pattern | proof lines | checked RUP additions | CNF SHA-256 |

|---|---:|---:|---|

| (3,3,2) | 16521 | 7479 | 376672db937dafbe0f2935e39af46b7f7edb756723c43c22c1c1ae73964e9fc0 |

| (4,2,2) | 5171 | 1002 | 0ac54773ec2d5f1c994fe8c5780c808b503ea1f2ec220c32c6f544fec908c3c3 |

| (4,3,1) | 4960 | 911 | 1f282c8251434db05c2aea278123f842da38f01cf5cd9589af10e11afd732d46 |

| (4,4,0) | 4864 | 477 | 0a2e50b0dddda9f60822491182175609bc3704f7201887c3111c1076e33569c1 |

| (5,2,1) | 3391 | 45 | f361cb5c8b16d08c0c887cffd27324bd456a9dfb0fe1057777ae4fd89f284780 |

| (5,3,0) | 3952 | 442 | f33ff1718e0c03390f0a97b4ebf57782759dbf9fb143270ab0939df42ff466d0 |

| (6,1,1) | 3402 | 44 | f4261adf70b0b9727abf9480987bb4f61368bf5a9ed596e24c0bd92a087b9997 |

| (6,2,0) | 3585 | 129 | 4dcef180691a2b47b52e53402bad85d4c2e70220ac1554d9b43e6efc133e895a |

| (7,1,0) | 3429 | 23 | a08103385d8f2ba37defe7baef350eb7e0905ef24528f4bc04f38d06b08adb8a |

| (8,0,0) | 3443 | 23 | 0f50cfa91a2ed10846700ead806024d0afb58f80f385578f6294ebf603fc707e |

Therefore every 3-colouring of \(K_9\) contains a monochromatic triangle or

5-cycle, so \(f(3)\le5\). Together with (4),

This exact conclusion remains labelled (d) because its upper half is an

exhaustive computational proof.

5. Reproduction

The standalone verifier is

erdos609_wave6f_verify.py, SHA-256

9da08367d4ba589ea119d53d88eb3c2451fc6737ae6810928288b58a7818092e.

It needs Python 3 and python-sat only to generate the DRUP traces; cycle

enumeration, CNF construction, normalization, and RUP proof checking are in

the file itself.

Run from the repository root:

python3 runs/erdos609_wave6f_verify.py

The clean run took 7.77 seconds and ended:

variables: 108
base clauses: 4932
forbidden cycle counts: {3: 84, 5: 1512}
all K9 odd-cycle counts: {3: 84, 5: 1512, 7: 12960, 9: 20160}
lower-certificate monochromatic counts:
  {3: (0, 0, 0), 5: (6, 6, 3), 7: (4, 2, 1), 9: (2, 0, 0)}
total RUP additions checked: 10575
VERIFIED: f(1)=3, f(2)=5, and computationally f(3)=5

6. What remains and the precise wall

The direct asymptotic gap is still

Janzer and Yip's upper bound uses the Lovász theta function of the complement:

it is normalized on complete graphs, submultiplicative under edge unions, and

close to 2 for graphs of large odd girth. Their concluding section identifies

an exact barrier. For an odd cycle \(C_g\), the theta value is already

\(2+\Theta(g^{-2})\), and vertex-transitivity forces equality in the relevant

product inequality. Hence merely sharpening their theta estimate can improve

their \(2^{k/2}\) bound by at most a polynomial factor. They explain that a

genuinely better upper bound would require, for example, a new upper bound on

the Shannon capacity of complements of high-odd-girth graphs that beats theta;

even the corresponding odd-cycle capacity bound is not known. (b)

On the lower-bound side, Day and Johnson's rooted-round construction is

unbalanced across colours and yields only

\(2^{\Omega(\sqrt{\log k})}\). The missing object is a uniform family of

\(k\)-colourings of \(K_{2^k+1}\) in which every colour graph has much larger

odd girth, together with a proof valid for all \(k\); finite SAT examples do

not supply that uniformity. (c)

Even the next exact case grows sharply. Testing whether \(f(4)\le7\) by the

same direct encoding means forbidding \(C_3,C_5,C_7\) in a 4-colouring of

\(K_{17}\). There are respectively

such undirected cycles. The naive CNF has 544 colour variables and

28,305,816 clauses, containing about \(1.98\times10^8\) literal occurrences:

roughly a 1 GB DIMACS file and several GB in a solver, before proof logging.

A realistic first budget for a symmetry-broken or lazy-constraint certified

UNSAT search is 10–100 single-core hours, with potentially much larger proof

storage; this was deliberately not run under the task's few-minute compute

limit. Exact \(f(4)\), or a substantially more compressed structural

argument, is the next finite computation needed. The clause and literal

counts are exact (a); the runtime and storage budget is an engineering

estimate (c), not a measured lower bound.

PARTIAL: Live status is OPEN with no worker or claimed proof; primary sources leave \(2^{\Omega(\sqrt{\log n})}\le f(n)\le O(n^{3/2}2^{n/2})\), while a proof-carrying exhaustive computation establishes the exact initial table \(f(1)=3,f(2)=5,f(3)=5\) and exposes that the page's “trivial \(2^n\)” bound suppresses an essential \(+1\) in small cases.