Erdős problem 1037
Let be a graph on vertices in which every degree occurs at most twice, and the number of distinct degrees is . Must contain a trivial (empty or complete) subgraph of size 'much larger' than ?
Sources
FormalConjectures/ErdosProblems/
1037.lean
Retained formal statement
Cambie, Chan, and Hunter have in the comment section given a simple construction of a graph on vertices with at least distinct degrees, every degree appears at most twice, and the largest trivial subgraph has size .
∃ C, ∀ᶠ (n : ℕ) in Filter.atTop, ∃ G, (∀ (d : ℕ), {v | (G.neighborSet v).ncard = d}.ncard ≤ 2) ∧ 3 / 4 * ↑n ≤ ↑(Set.range fun v => (G.neighborSet v).ncard).ncard ∧ ∀ (s : Set (Fin n)), Erdos1037.IsTrivialSet G s → ↑s.ncard ≤ C * Real.log ↑nSolvedStatement only, no proof