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
- [a] elementary-rigorous: proved below from definitions.
- [b] rigorous-modulo-named-theorem: the stated deduction is rigorous, conditional only on the explicitly named published theorem.
- [c] plausible/structural-unverified: a search conclusion or proposed route, not a theorem.
- [d] computational-only: an exhaustive finite check; it is not promoted to an infinite theorem.
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:
OPEN;0 comments on this problem;0 claimed proofs for this problem;Interested in collaborating None;Currently working on this problem None;- last edited
23 January 2026.
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:
- \(C_4\) is two copies of the length-two path \(P_3\) glued at their
two endpoints;
- the diamond is two triangles glued along their common edge.
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\).