Erdős problem 188

What is the smallest $k$ such that $\mathbb{R}^2$ can be red/blue coloured with no pair of red points unit distance apart, and no $k$ -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 statement1 of 3

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

FormalConjectures/ErdosProblems/188.leanErdos188.erdos_1881 lineExact file

1IsLeast Erdos188.s sorry

OpenStatement only, no proof