Erdős problem 595
Erdős Problem 595 (250): Is there an infinite graph G which contains no and is not the union of countably many triangle-free graphs?
Sources
FormalConjectures/ErdosProblems/
595.lean
Retained formal statement
Folkman–Nešetřil–Rödl (finite version) [Fo70, NeRo75]: For every n ≥ 1, there exists a graph G (on a finite vertex set) that contains no and whose edges cannot be covered by n triangle-free graphs.
More precisely: for every n : ℕ with 1 ≤ n, there exist a finite type V and a graph G : SimpleGraph V with: 1. G.CliqueFree 4 (no ), and 2. For every family H : Fin n → SimpleGraph V of triangle-free graphs, G ≠ ⨆ i, H i.
This is the finite analogue of Problem 595. The proofs of Folkman [Fo70] and Nešetřil–Rödl [NeRo75] give different explicit constructions.
True ↔ ∀ (n : ℕ), 1 ≤ n → ∃ V x G, G.CliqueFree 4 ∧ ∀ (H : Fin n → SimpleGraph V), (∀ (i : Fin n), (H i).CliqueFree 3) → G ≠ ⨆ i, H iSolvedStatement only, no proof