Skip to content

Erdős problem 582

Does there exist a graph GG which contains no K4K_4, and yet any 22-colouring of the edges produces a monochromatic K3K_3?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/582.lean

Formal Conjectures

FormalConjectures/ErdosProblems/582.leanErdos582.erdos_5821 lineExact file
True ↔ ∃ V x G, G.CliqueFree 4 ∧ Erdos582.EdgeRamseyTriangle G
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:582
  • PLBY Lean proofsErdosProblems.Erdos582

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