Erdős problem 1037

Let $G$ be a graph on $n$ vertices in which every degree occurs at most twice, and the number of distinct degrees is $>(\frac{1}{2}+\epsilon)n$ . Must $G$ contain a trivial (empty or complete) subgraph of size 'much larger' than $\log n$ ?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1037.lean

Retained formal statement2 of 2

Cambie, Chan, and Hunter have in the comment section given a simple construction of a graph on $n$ vertices with at least $\frac{3}{4}n$ distinct degrees, every degree appears at most twice, and the largest trivial subgraph has size $O(\log n)$ .

FormalConjectures/ErdosProblems/1037.leanErdos1037.erdos_1037.variants.cambie_chan_hunter6 linesExact file

1∃ C,2  ∀ᶠ (n : ℕ) in Filter.atTop,3    ∃ G,4      (∀ (d : ℕ), {v | (G.neighborSet v).ncard = d}.ncard ≤ 2) ∧5        3 / 4 * ↑n ≤ ↑(Set.range fun v => (G.neighborSet v).ncard).ncard ∧6          ∀ (s : Set (Fin n)), Erdos1037.IsTrivialSet G s → ↑s.ncard ≤ C * Real.log ↑n

SolvedStatement only, no proof