Erdős problem 596
Erdős Problem 596 (Erdős–Hajnal, [Er87]). For which graph pairs is it true that
Sources
FormalConjectures/ErdosProblems/
596.lean
Retained formal statement
The empty graph on Fin 0 is Free of any nontrivial subgraph (vacuous). This is the simplest non-trivial witness to G₁.Free H appearing in HasFiniteRamseyProperty.
(SimpleGraph.cycleGraph 4).Free ⊥TestStatement only, no proof