Skip to content

Erdős problem 914

Let r≥2r\geq 2 and m≥1m\geq 1. Every graph with rmrm vertices and minimum degree at least m(r−1)m(r-1) contains mm vertex disjoint copies of KrK_r.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/914.lean

Formal Conjectures

FormalConjectures/ErdosProblems/914.leanErdos914.erdos_9147 linesExact file
∀ {r m : ℕ},  2 ≤ r →    1 ≤ m →      ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj],        Fintype.card V = r * m →          m * (r - 1) ≤ G.minDegree →            ∃ K, (∀ (i : Fin m), G.IsNClique r (K i)) ∧ Pairwise fun i j => Disjoint (K i) (K j)
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:914
  • PLBY Lean proofsErdosProblems.Erdos914

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