ERDŐS/DAILY

← back to the ledger

ERDőS #597 · PARTIAL

Erdős problem 597 — live audit, a one-sum closure theorem, and the finite block reduction

Date of audit: 2026-07-27 (UTC).

Claim labels

1. Mandatory live-page gate

I fetched the rendered body of the canonical live page, <https://www.erdosproblems.com/597>, through the Bright Data browser on 2026-07-27. This was a genuine browser load, not a direct datacenter curl.

The page showed:

Thus the requested stop condition was not triggered.

The statement below is verbatim from the page's LaTeX source (only Markdown quotation marks have been added):

> Let \(G\) be a graph on at most \(\aleph_1\) vertices which contains no \(K_4\) and no \(K_{\aleph_0,\aleph_0}\) (the complete bipartite graph with \(\aleph_0\) vertices in each class). Is it true that

> \[ > \omega_1^2 \to (\omega_1\omega, G)^2? > \]

> What about finite \(G\)?

The known-result paragraph on the same live page says, verbatim:

> Erdős and Hajnal proved that \(\omega_1^2 \to (\omega_1\omega,3)^2\). Erdős originally asked this with just the assumption that \(G\) is \(K_4\)-free, but Baumgartner proved that \(\omega_1^2 \not\to (\omega_1\omega, K_{\aleph_0,\aleph_0})^2\).

No claimed proof, comment, or activity marker was hidden elsewhere in the rendered body. The standalone verifier repeats this browser audit with --source-audit.

2. Interpretation and primary-source audit

Put

\[ \alpha=\omega_1^2=\omega_1\cdot\omega_1,\qquad \beta=\omega_1\omega=\omega_1\cdot\omega. \]

For a graph \(F\), write

\[ \mathsf P(F)\quad\Longleftrightarrow\quad \alpha\to(\beta,F)^2. \]

Thus every red/blue coloring of \([\alpha]^2\) has either a red set of inherited order type \(\beta\), or a (not necessarily induced) blue copy of \(F\).

What the cited sources actually say

1. [b] Erdős 1987. Paul Erdős, Some problems on finite and infinite graphs, Contemporary Mathematics 65 (1987), 223–228, is available in the Rényi archive. On p. 224 it records the triangle result, asks the \(K_4\)-free graph question, explicitly says it is open even for finite \(G\), reports Baumgartner's \(K_{\aleph_0,\aleph_0}\) counterexample, and proposes adding the absence of that biclique. The fetched PDF had SHA-256

b22809ce28667517eb39249bf54bff2140c548475306070989f3f8964870cb71.

2. [b] Triangle base theorem. P. Erdős and A. Hajnal, Ordinary partition relations for ordinal numbers, Periodica Mathematica Hungarica 1 (1971), 171–185, is available in the Rényi archive. Its Theorem 5 states

\[ \omega_{\xi+1}^{(t+1)(k+1)} \to(\mu,t+2)^2 \quad\text{for every }\mu<\omega_{\xi+1}^{k+2}, \]

for \(k<\omega\) and \(1\le t<\omega\). Taking

\(\xi=0,\ k=0,\ t=1,\ \mu=\omega_1\omega\) gives exactly

\[ \mathsf P(K_3): \qquad \omega_1^2\to(\omega_1\omega,3)^2. \]

The fetched PDF had SHA-256

b69fdc5cd09bde547e464667874f369f8524f3f6c20156b155ca6db4ab98a8bd.

3. [b] The cited 1999 booklet. Some of Paul's Favorite Problems, produced for the 1999 Budapest conference, is available as a primary scan. Item 7.84 asks the related multicolor question

\[ \omega_1^2\to\bigl(\omega_1\omega,(3)_k\bigr)^2 \quad\text{for every }k<\omega. \]

It is not a claim that problem 597 was solved. The fetched scan had SHA-256

31a119a87c1300b8acca67686dfd0a1623d0f7748214054b2b6823d4d581ddcd;

page 8 was independently rendered and OCR located item 7.84.

4. [b] Compactness theorem used below. N. G. de Bruijn and P. Erdős, A colour problem for infinite graphs and a problem in the theory of relations, Proc. Koninklijke Nederlandse Akademie van Wetenschappen, Series A 54 (1951), 371–373, proves that an infinite graph is \(q\)-colorable, for finite \(q\), if all its finite subgraphs are. The title, authors, year, journal, volume, and pages were checked against the Eindhoven University primary bibliographic record.

Search for a later resolution

[c] I searched the exact Unicode and ASCII forms of

@@S45@@, the phrase from Erdős's paper

“open even if \(G\) is assumed to be finite,” and combinations with

Baumgartner, K4, and K(aleph_0,aleph_0). I also checked the publisher

record and bibliography of Péter Komjáth's 2025 *The Erdős–Hajnal Problem

List* (Bull. Symbolic Logic 31, 418–461, DOI

10.1017/bsl.2025.1). The exact searches returned the live problem page,

the cited 1987 paper, the 1999 multicolor problem, and general partition

calculus sources, but no later paper claiming this graph relation. The

2025 survey's full text was access-restricted in this environment, so I do

not claim that it omits the question. The live page, edited in January

2026, remains the best current status evidence.

[c] I did not locate a published primary proof of Baumgartner's

\(K_{\aleph_0,\aleph_0}\) negative relation. The contemporaneous primary

source Er87 says “Baumgartner just showed” it, and the live page repeats

the result. I therefore attribute no unverified paper or arXiv identifier

to that result.

3. New finite progress

Main theorem

[b] Theorem. If \(G\) is a finite \(K_4\)-free block graph, then

\[ \omega_1^2\to(\omega_1\omega,G)^2. \]

Here a block graph is a graph in which every block (maximal

2-connected piece, with bridges counted as \(K_2\) blocks) is a clique.

Equivalently in the \(K_4\)-free case, every nontrivial block is \(K_2\)

or \(K_3\).

This includes every finite forest, every finite friendship/windmill

graph, arbitrary finite trees of edge and triangle blocks, the paw, and

disjoint unions of such graphs. It is an infinite family, rather than a

finite list of examples.

The key reusable statement is stronger.

One-vertex amalgamation lemma

Let \((H,r)\) and \((J,s)\) be nonempty finite rooted graphs. Write

\[ H\vee J \]

for their one-sum: take disjoint copies and identify \(r\) with \(s\).

[b] Lemma (one-sum closure).

\[ \mathsf P(H)\ \text{and}\ \mathsf P(J) \quad\Longrightarrow\quad \mathsf P(H\vee J). \]

Before proving it, one elementary ordinal fact is needed.

Finite indivisibility of \(\omega_1^2\)

[a] Lemma. If a set of order type \(\alpha=\omega_1^2\) is partitioned

into finitely many pieces, one piece has order type \(\alpha\).

Proof. Split \(\alpha\) into its consecutive blocks

\[ B_\xi=[\omega_1\xi,\omega_1(\xi+1)),\qquad \xi<\omega_1. \]

Each \(B_\xi\) has order type \(\omega_1\). In a finite coloring of

\(B_\xi\), some color occurs uncountably often and hence on a subset of

order type \(\omega_1\). Choose one such color for each \(\xi\). A fixed

color is chosen for \(\omega_1\) many indices, because a finite union of

countable sets is countable. Along those \(\omega_1\) blocks, its

uncountable slices have combined order type

\(\omega_1\cdot\omega_1=\alpha\). \(\square\)

[a] Corollary. If \(U\subseteq\alpha\) has

\(\operatorname{otp}(U)<\alpha\), then

\(\operatorname{otp}(\alpha\setminus U)=\alpha\).

Apply the lemma to the two-piece partition

\(\{U,\alpha\setminus U\}\).

Proof of one-sum closure

[b] Proof. Fix a red/blue coloring of \([\alpha]^2\), and suppose

for contradiction that it has neither a red set of type \(\beta\) nor a

blue \(H\vee J\).

Let \(h=|V(H)|\), and define

\[ U=\{x<\alpha:\text{some blue copy of }H \text{ maps its root }r\text{ to }x\}. \]

For each \(x\in U\), choose one witness \(C_x\), the vertex set of such

a rooted blue \(H\)-copy.

If \(\operatorname{otp}(U)<\alpha\), the corollary gives

\(\operatorname{otp}(\alpha\setminus U)=\alpha\). There is no blue copy

of \(H\) inside \(\alpha\setminus U\), since the image of its root would

belong to \(U\). Applying \(\mathsf P(H)\) on that complement gives a red

set of type \(\beta\), a contradiction.

It remains to treat \(\operatorname{otp}(U)=\alpha\). Define the

conflict graph \(D\) on \(U\) by

\[ xy\in E(D) \quad\Longleftrightarrow\quad y\in C_x\setminus\{x\} \ \text{or}\ x\in C_y\setminus\{y\}. \]

For every finite \(S\subseteq U\),

\[ |E(D[S])|\le (h-1)|S|. \tag{1} \]

Indeed, orient a witnessing arc from \(x\) to each member of

\(C_x\setminus\{x\}\). There are at most \(h-1\) arcs leaving each

\(x\), and every edge of \(D[S]\) is witnessed by an arc whose two ends

are in \(S\).

Every nonempty finite induced subgraph of \(D\) consequently has a

vertex of degree at most \(2(h-1)\); otherwise its degree sum would

exceed \(2(h-1)|S|\), contradicting (1). Repeated deletion gives a

\((2h-1)\)-coloring of every finite subgraph. By the de

Bruijn–Erdős compactness theorem, all of \(D\) is \((2h-1)\)-colorable.

Finite indivisibility of \(\alpha\) now gives a \(D\)-independent set

\(W\subseteq U\) of order type \(\alpha\). There cannot be a blue copy

of \(J\) in \(W\). If there were one, let \(x\in W\) be the image of its

root \(s\). For every other vertex \(y\) of that copy, \(D\)-independence

implies \(y\notin C_x\). Hence \(C_x\) and this \(J\)-copy meet exactly

at \(x\), and together form a blue \(H\vee J\), contrary to assumption.

Thus \(W\) is blue-\(J\)-free. Applying \(\mathsf P(J)\) to \(W\) gives

a red set of type \(\beta\), the final contradiction. \(\square\)

The exact constants matter: finiteness of \(H\) produces the uniform

bound \(h-1\) in (1), hence a finite coloring of the conflict graph.

Disjoint-union closure

[a] Lemma. For finite graphs \(H,J\),

\[ \mathsf P(H)\ \text{and}\ \mathsf P(J) \quad\Longrightarrow\quad \mathsf P(H\sqcup J). \]

Proof. In a coloring with no red \(\beta\), first take a blue \(H\).

Delete its finitely many vertices; the remaining ordered set still has

type \(\alpha\). There take a blue \(J\). The copies are vertex-disjoint,

and extra cross-edges do not matter because graph copies are not

required to be induced. \(\square\)

Block reduction and proof of the theorem

[a] \(\mathsf P(K_1)\) is immediate, and

\(\mathsf P(K_2)\) is immediate because in the absence of a blue edge

all pairs are red.

[b] \(\mathsf P(K_3)\) is the Erdős–Hajnal theorem verified above.

[a] The block-cut graph of a finite connected graph is a tree. By

rooting it at one block and adding its other blocks outwards, the graph

is obtained by repeated one-sums of its blocks. Different connected

components are then combined by disjoint unions.

[b] A \(K_4\)-free block graph has only \(K_2\) and \(K_3\) as

nontrivial blocks. The two closure lemmas therefore prove the main

theorem.

Exact reduction of the remaining finite question

[b] Corollary (clean reduction). The assertion

\[ \mathsf P(G)\quad\text{for every finite \(K_4\)-free graph \(G\)} \]

is equivalent to the same assertion restricted to finite

2-connected \(K_4\)-free graphs.

The forward implication is immediate. For the reverse implication,

apply the assumed result to every nontrivial block and then use one-sum

and disjoint-union closure. Thus cutvertices and disconnectedness are

not part of the remaining difficulty.

On four vertices, the first two 2-connected \(K_4\)-free blocks beyond

\(K_3\) are

\[ C_4\qquad\text{and}\qquad K_4-e\ \text{(the diamond)}. \]

The argument above does not prove their partition relations; it

isolates them as the first missing cases.

4. Independent finite verification

The standalone checker is

verify_erdos597_wave6f.py. It uses no

third-party package for graph computation.

Two independent structural algorithms were compared on every labeled

graph with at most six vertices:

1. Tarjan biconnected-component decomposition followed by the test that

every block is \(K_2\) or \(K_3\);

2. recursive reversal of disjoint unions, pendant-\(K_2\) one-sums, and

pendant-\(K_3\) one-sums.

They agreed on every input.

[d] Exact labeled counts:

| \(n\) | all labeled graphs | \(K_4\)-free | \(K_4\)-free block graphs covered |

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

| 1 | 1 | 1 | 1 |

| 2 | 2 | 2 | 2 |

| 3 | 8 | 8 | 8 |

| 4 | 64 | 63 | 54 |

| 5 | 1,024 | 958 | 536 |

| 6 | 32,768 | 27,626 | 7,132 |

[d] Exact unlabeled counts:

| \(n\) | all | \(K_4\)-free | covered | not covered by this theorem |

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

| 1 | 1 | 1 | 1 | 0 |

| 2 | 2 | 2 | 2 | 0 |

| 3 | 4 | 4 | 4 | 0 |

| 4 | 11 | 10 | 8 | 2 |

| 5 | 34 | 29 | 17 | 12 |

At \(n=4\), the script canonically identifies the two uncovered

isomorphism types as:

C4:             [(0,2),(0,3),(1,2),(1,3)]
diamond (K4-e): [(0,1),(0,2),(0,3),(1,2),(1,3)]

“Not covered” means only that the proved closure theorem does not reach

the graph. It is not a computational counterexample to the ordinal

partition relation.

[d] Local proof checks. For all labeled blue host graphs on at most

six vertices which avoid the indicated one-sum, the checker independently

chooses rooted witnesses, constructs the conflict graph, checks (1) on

every vertex subset, produces the stated degeneracy coloring, and verifies

that every conflict-independent set avoids the second rooted graph. The

numbers of target-free hosts checked were:

K2∨K2:     119
K2∨K3:   6,403
K3∨K3:  21,052

These finite checks are sanity checks of the local combinatorics, not the

proof of the uncountable assertion.

Reproduction

cd /home/exedev/MathDyad
python runs/verify_erdos597_wave6f.py
python runs/verify_erdos597_wave6f.py --source-audit

The first command completed in about 22 seconds on this VM. The second

also refetched the three cited scans, checked the de Bruijn–Erdős

bibliographic record, and reloaded the live page through Bright Data. Its

final output was:

SOURCE Er87 sha256=b22809ce28667517eb39249bf54bff2140c548475306070989f3f8964870cb71
SOURCE EH71 sha256=b69fdc5cd09bde547e464667874f369f8524f3f6c20156b155ca6db4ab98a8bd
SOURCE Va99 sha256=31a119a87c1300b8acca67686dfd0a1623d0f7748214054b2b6823d4d581ddcd; OCR item 7.84 found
SOURCE de Bruijn-Erdos 1951 bibliographic record found
SOURCE LIVE: OPEN; 0 claims/comments; no worker/collaborator

ALL CHECKS PASSED

5. Precise wall

The first missing lemma

[c] The natural next target is a two-root amalgamation lemma.

Both first missing graphs have such a description:

two endpoints;

The one-root proof indexes witnesses by vertices and obtains a conflict

graph with at most \(h-1\) outgoing witness conflicts per vertex. With

two roots, witnesses are indexed by pairs. Compatibility becomes a

finite set mapping on \([\alpha]^2\), and the bounded-outdegree graph

coloring argument no longer produces a set \(W\) of type \(\alpha\) on

which a second pair-rooted copy can be installed.

A lemma strong enough to prove either

\[ \mathsf P(P_3)\Longrightarrow\mathsf P(C_4) \quad\text{or}\quad \mathsf P(K_3)\Longrightarrow\mathsf P(K_4-e) \]

under the corresponding two-root gluing would advance the first open

finite cases. No such lemma was proved here.

Why the classical clique theorem stops

[b] In Erdős–Hajnal Theorem 5, \(t=1,k=0\) gives the required

triangle relation at \(\omega_1^2\). To request a blue \(K_4\), one sets

\(t=2\), and the first left-hand ordinal supplied by that theorem is

\[ \omega_1^{(2+1)(0+1)}=\omega_1^3, \]

not \(\omega_1^2\). This does not prove that a \(K_4\) statement at

\(\omega_1^2\) is false; it pinpoints why that standard theorem does not

supply it. The Va99 item 7.84 multicolor-triangle route is itself an open

strengthening, so assuming it would only trade problem 597 for another

open partition relation.

Why the infinite-\(G\) case is untouched

[a] The one-sum proof uses

\[ |E(D[S])|\le(|H|-1)|S| \]

with finite \(|H|\), leading to a finite chromatic bound and then finite

indivisibility of \(\omega_1^2\). For an infinite witness \(H\), that

finite constant disappears. The hypothesis “no

\(K_{\aleph_0,\aleph_0}\)” does not by itself restore a uniform finite

bound on witness conflicts. Thus the proof gives no result for the

general \(G\) of size at most \(\aleph_1\).

Finite host enumeration cannot repair either gap: the assertion is about

all colorings of an uncountable ordinal, and the needed free-set or

two-root amalgamation statement is a uniform infinitary lemma. Extending

the brute-force host check from \(n=6\) to \(n=7\) would already require

examining \(2^{21}=2{,}097{,}152\) labeled graphs and would yield only a

larger sanity check, not such a lemma.

PARTIAL: proved \(\omega_1^2\to(\omega_1\omega,G)^2\) for every finite \(K_4\)-free block graph and reduced the full finite question exactly to 2-connected \(K_4\)-free blocks; the first unresolved-by-this-method cases are \(C_4\) and \(K_4-e\).

This is the AI working report, labelled by outcome — not an independently verified claim unless marked PROVED. ← ledger