Skip to content

Erdős problem 904

Start work

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}).

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/904.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:904
  • PLBY Lean proofsErdosProblems.Erdos904

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry