Skip to content

Erdős problem 904

Let r≥2r\geq 2 and let tr(n)t_r(n) be the Turán number (the maximal number of edges in a graph on nn vertices with no Kr+1K_{r+1}).

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

904.lean

Retained formal statement1 of 1

Let r≥2r\geq 2 and let tr(n)t_r(n) be the Turán number (the maximal number of edges in a graph on nn vertices with no Kr+1K_{r+1}).

If GG is a graph with nn vertices and m≥tr(n)m\geq t_r(n) edges there exists a clique on rr vertices, say x1,…,xrx_1,\ldots,x_r, such that d(x1)+⋯+d(xr)≥2rmn.d(x_1)+\cdots+d(x_r)\geq \frac{2rm}{n}.

A conjecture of Bollobás and Erdős. This was conjectured in [Er75] only in the special case r=3r=3. Edwards [Ed78] proved the conjecture for 2≤r≤82\leq r\leq 8 (under the additional assumption that n≥r2n\geq r^2). Faudree [Fa92] proved the conjecture for all r≥2r\geq 2 provided n>r−14r2n>\frac{r-1}{4}r^2. The full conjecture was proved by Bollobás and Nikiforov [BoNi05].

FormalConjectures/ErdosProblems/904.leanErdos904.erdos_9045 linesExact file
True ↔  ∀ (V : Type u_1) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj],    ∀ r ∈ Set.Icc 1 (Erdos904.n V),      Erdos904.turanNumber (Erdos904.n V) r ≤ G.edgeFinset.card →        ∃ s, G.IsNClique r s ∧ 2 * r * G.edgeFinset.card ≤ Erdos904.n V * ∑ v ∈ s, G.degree v
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.