Erdős problem 1037 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1037.lean

Retained formal statement1 of 2

A question of Chen and Erdős.

The answer is no - 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_10379 linesExact file

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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science