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.

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

905.lean

Retained formal statement1 of 1

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

A conjecture of Bollobás and Erdős. This was proved independently by Edwards (unpublished) and Khadzhiivanov and Nikiforov [KhNi79].

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.

Sources

Search problems.science