Erdős problem 905 · problems.science

Every graph with $n$ vertices and $>n^2/4$ edges contains an edge which is in at least $n/6$ triangles.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/905.lean

Formal Conjectures

FormalConjectures/ErdosProblems/905.leanErdos905.erdos_9052 linesExact file

1∀ (n : ℕ) (G : SimpleGraph (Fin n)) [inst : DecidableRel G.Adj],2  ↑n ^ 2 / 4 < ↑G.edgeFinset.card → ∃ e ∈ G.edgeFinset, ↑n / 6 ≤ ↑(G.trianglesContaining e).card

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:905
PLBY Lean proofsErdosProblems.Erdos905

Reported activity

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

Formalization
Erdős AI contributions wiki · 7 Apr, 2026
Machine
Aristotle, GPT-5.4
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