Erdős problem 914 · problems.science

Let $r\geq 2$ and $m\geq 1$ . Every graph with $rm$ vertices and minimum degree at least $m(r-1)$ contains $m$ vertex disjoint copies of $K_r$ .

Sources

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

914.lean

Retained formal statement1 of 2

Let $r\geq 2$ and $m\geq 1$ . Every graph with $rm$ vertices and minimum degree at least $m(r-1)$ contains $m$ vertex disjoint copies of $K_r$ .

When $r=2$ this follows from Dirac's theorem. Corrádi and Hajnal [CoHa63] proved this when $r=3$ . Hajnal and Szemerédi [HaSz70] proved this for all $r\geq 4$ .

A shorter proof was given by Kierstead and Kostochka [KiKo08].

FormalConjectures/ErdosProblems/914.leanErdos914.erdos_9147 linesExact file

1∀ {r m : ℕ},2  2 ≤ r →3    1 ≤ m →4      ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj],5        Fintype.card V = r * m →6          m * (r - 1) ≤ G.minDegree →7            ∃ 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.

Sources

Search problems.science