theorem
Erdos75.erdos_75 :
True ↔ ∃ (V : Type) (G : SimpleGraph V),
G.chromaticCardinal = Cardinal.aleph 1 ∧ Cardinal.mk V = Cardinal.aleph 1 ∧ ∀ ε > 0,
∀ᶠ (n : ℕ) in Filter.atTop, ∀ (H : G.Subgraph),
H.verts.ncard = n → ∃ (I : Finset V), ↑I ⊆ H.verts ∧ G.IsIndepSet ↑I ∧ ↑I.card > ↑n ^ (1 - ε)
Is there a graph of chromatic number ℵ_ 1 with ℵ_ 1 vertices such that for all
ε > 0, if n is sufficiently large and H is a subgraph on n vertices,
then H contains an independent set of size > n ^ (1 - ε)?