Erdős problem 138 · problems.science

If $W(k)$ is the least $N$ such that every two-colouring of $\{1, \dots, N\}$ contains a monochromatic $k$ -term arithmetic progression, must $W(k+1) - W(k) \to \infty$ ?

Sources

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

10 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

138.lean

Retained formal statement2 of 9

In [Er81] Erdős asks whether $W(k+1) - W(k) \to \infty$ .

The DeepMind prover agent has found a formal proof of this statement.

FormalConjectures/ErdosProblems/138.leanErdos138.erdos_138.variants.difference1 lineExact file

1True ↔ Filter.Tendsto (fun k => Erdos138.W (k + 1) - Erdos138.W k) Filter.atTop Filter.atTop

SolvedProof has a holeformal conjecturesexternal 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