Skip to content

Erdős problem 904

Let r2r\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

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

904.lean

Retained formal statement1 of 1

Let r2r\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 mtr(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 2r82\leq r\leq 8 (under the additional assumption that nr2n\geq r^2). Faudree [Fa92] proved the conjecture for all r2r\geq 2 provided n>r14r2n>\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],rSet.Icc 1 (Erdos904.n V),      Erdos904.turanNumber (Erdos904.n V) rG.edgeFinset.cards, G.IsNClique r s ∧ 2 * r * G.edgeFinset.cardErdos904.n V * ∑ vs, 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.

Search problems.science

Find a Problem, Result, source, or page