Erdős problem 138
If is the least such that every two-colouring of contains a monochromatic -term arithmetic progression, must ?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/138.leanTrue ↔ Filter.Tendsto (fun k => ↑(Erdos138.W k) ^ (1 / ↑k)) Filter.atTop Filter.atTopOpenStatement only, no proof
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
AI standalone
- Machine
AI collaborating with humans
- Machine
- People
argument
- Machine
- Reported outcome