An infinite $K_4$-free graph that is not a countable union of triangle-free graphs: does one exist? (Erdős #595)
Statement
A graph is said to be the union of countably many triangle-free graphs if its edge set can be covered by countably many ($\aleph_0$) triangle-free subgraphs — equivalently, if its edges can be coloured with countably many colours so that no colour class contains a triangle ($K_3$). Question of Erdős and Hajnal: does there exist an infinite graph $G$ that contains no $K_4$ (no four pairwise-adjacent vertices) and yet is NOT the union of countably many triangle-free graphs?
Acceptance. FULLY RESOLVES: either (a) construct an explicit infinite $K_4$-free graph $G$ together with a proof that it is not the union of countably many triangle-free graphs, or (b) prove that every $K_4$-free graph is the union of countably many triangle-free graphs. Because the problem is OPEN (no finite computation can decide it), deliver a complete written proof with all steps (machine-checkable Lean/Coq preferred). ADVANCES: (a) determine or bound the least $N(n)$ such that some $K_4$-free graph on $N$ vertices is not the union of $n$ triangle-free graphs (a Folkman-type number), delivered as an explicit graph plus a machine-checkable certificate of non-coverability (e.g. an exhaustive or SAT proof that no $n$ triangle-free subgraphs cover its edges), strictly improving the best known such bound; or (b) prove new structural constraints that any hypothetical infinite counterexample must satisfy. Deliver the proof, or the finite construction plus the non-coverability certificate and the code that produced it.
Background
A problem of Erdős and Hajnal [Er87]. The finite analogue is settled and points the opposite way: Folkman [Fo70] and, independently, Nešetřil and Rödl [NeRo75] proved that for every fixed $n\geq 1$ there is a finite $K_4$-free graph that is not the union of $n$ triangle-free graphs — so no finite bound on the number of triangle-free graphs can suffice for all $K_4$-free graphs. The open question asks whether $\aleph_0$ triangle-free graphs always suffice to cover a $K_4$-free graph, or whether some (necessarily infinite) $K_4$-free graph needs more than countably many. Erdős offered \$250 for a solution. This is exactly the $(G_1,G_2)=(K_4,K_3)$ instance of the finite-vs-$\aleph_0$ colouring programme in Erdős #596 (erdosproblems.com/596), and is related to Erdős #582 (erdosproblems.com/582). Listed as open on erdosproblems.com/595 (fetched 2026-07-13, status 'open'), tagged graph theory | set theory; a Lean formalisation exists in the DeepMind formal-conjectures repository. Attacker's tool: infinite combinatorics — chromatic number of infinite triangle-hypergraphs, compactness and countable-union decompositions — for the infinite problem itself; the finite Folkman-type numbers (smallest $K_4$-free graphs not coverable by $n$ triangle-free graphs) supply a searchable neighbourhood via clique/SAT enumeration that sharpens intuition, though no finite computation can close the infinite case.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #595 (T. F. Bloom) | website |
| REF-02 | Lean formalisation of Erdős #595 (DeepMind formal-conjectures) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.