Erdős problem 904
Let and let be the Turán number (the maximal number of edges in a graph on vertices with no ).
Sources
FormalConjectures/ErdosProblems/
904.lean
Retained formal statement
Let and let be the Turán number (the maximal number of edges in a graph on vertices with no ).
If is a graph with vertices and edges there exists a clique on vertices, say , such that
A conjecture of Bollobás and Erdős. This was conjectured in [Er75] only in the special case . Edwards [Ed78] proved the conjecture for (under the additional assumption that ). Faudree [Fa92] proved the conjecture for all provided . The full conjecture was proved by Bollobás and Nikiforov [BoNi05].
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