Erdős problem 904 · problems.science

Let $r\geq 2$ and let $t_r(n)$ be the Turán number (the maximal number of edges in a graph on $n$ vertices with no $K_{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

1True ↔2  ∀ (V : Type u_1) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj],3    ∀ r ∈ Set.Icc 1 (Erdos904.n V),4      Erdos904.turanNumber (Erdos904.n V) r ≤ G.edgeFinset.card →5        ∃ 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

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Formalization
Erdős AI contributions wiki · 18 Apr, 2026
Machine
Aristotle
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science