Skip to content

Erdős problem 639

Is it true that if the edges of KnK_n are 2-coloured then there are at most n2/4n^2/4 many edges which do not occur in a monochromatic triangle?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/639.lean

Formal Conjectures

FormalConjectures/ErdosProblems/639.leanErdos639.erdos_6395 linesExact file
True ↔  ∀ᶠ (n : ℕ) in Filter.atTop,    ∀ (C : Sym2 (Fin n) → Fin 2),      {e | ¬e.IsDiag ∧ ∀ (x y : Fin n), e = s(x, y) → ¬∃ z, z ≠ x ∧ z ≠ y ∧ C s(x, z) = C e ∧ C s(y, z) = C e}.ncard ≤        n ^ 2 / 4
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:639
  • PLBY Lean proofsErdosProblems.Erdos639

Reported activity

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

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page