Skip to content

Erdős problem 1037

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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/1037.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1037.leanErdos1037.erdos_10379 linesExact file
False ↔  ∀ (ε : ℝ),    0 < ε →      ∀ (C : ℝ),        ∀ᶠ (n : ℕ) in Filter.atTop,          ∀ (G : SimpleGraph (Fin n)),            (∀ (d : ℕ), {v | (G.neighborSet v).ncard = d}.ncard ≤ 2) →              (1 / 2 + ε) * ↑n < ↑(Set.range fun v => (G.neighborSet v).ncard).ncard →                ∃ 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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:1037
  • PLBY Lean proofsErdosProblems.Erdos1037

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page