Erdős problem 595 · problems.science

Erdős Problem 595 (250): Is there an infinite graph G which contains no $K_4$ and is not the union of countably many triangle-free graphs?

Sources

Browse retained paths and inspect the exact material available for this Problem.

7 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

595.lean

Retained formal statement4 of 7

**The complete graph ⊤ on Fin 4 is not $K_4$ -free**: ⊤ on Fin 4 equals the complete graph $K_4$ , so it contains $K_4$ as a subgraph and is not $K_4$ -free.

This sanity check confirms the $K_4$ -free hypothesis of Problem 595 is non-trivial.

FormalConjectures/ErdosProblems/595.leanErdos595.erdos_595.variants.K4_not_cliqueFree1 lineExact file

1¬⊤.CliqueFree 4

TextbookStatement only, no proof

Sources

Search problems.science