Skip to content

Erdős problem 188

What is the smallest kk such that R2\mathbb{R}^2 can be red/blue coloured with no pair of red points unit distance apart, and no kk-term arithmetic progression of blue points with distance 1?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

188.lean

Retained formal statement3 of 3

Old and new problems and results in combinatorial number theory by Erdős & Graham (Page 14, 15):

It has been shown that there is a large MM so that it is possible to partition E2\mathbb{E}^2 into two sets AA and BB so that AA contains no pair of points with distance 1 and BB contains no A.P. of length MM.

FormalConjectures/ErdosProblems/188.leanErdos188.erdos_188.variants.nonempty1 lineExact file
Erdos188.s.Nonempty
SolvedStatement only, no proof