Problem

erdos:1034

False ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), ↑n ^ 2 / 4 < ↑G.edgeSet.ncard → ∃ T, G.IsNClique 3 T ∧ ∃ Y, Erdos1034.JoinedToTwo G T Y ∧ (1 / 2 - ε) * ↑n < ↑Y.card

Open Current State

Declared status: disproved (Lean)
Formalization: formalized
Subjects: graph theory
OEIS: possible
Sources: source:erdos-ai-contributions-wikisource:erdos-problemssource:formal-conjecturessource:jayyhk-erdos-leansource:plby-lean-proofs
Statement: www.erdosproblems.com

Matching claims

0

No direct claims

This problem has no directly related claim record.

Browse this Repository’s Claims