Skip to content

Erdős problem 645

If ℕ is 22-coloured then there must exist a monochromatic three-term arithmetic progression x,x+d,x+2dx,x+d,x+2d such that d>xd>x.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/645.lean

Formal Conjectures

FormalConjectures/ErdosProblems/645.leanErdos645.erdos_6451 lineExact file
∀ (c : ℕ → Bool), ∃ x d, 0 < x ∧ x < d ∧ ∃ C, c x = C ∧ c (x + d) = C ∧ c (x + 2 * d) = C
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:645
  • PLBY Lean proofsErdosProblems.Erdos645

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