Erdős problem 196

Must every permutation of $\mathbb{N}$ , contain a monotone 4-term arithmetic progression?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

196.lean

Retained formal statement1 of 1

Must every permutation of $\mathbb{N}$ , contain a monotone 4-term arithmetic progression?

FormalConjectures/ErdosProblems/196.leanErdos196.erdos_1961 lineExact file

1True ↔ ∀ (f : ℕ ≃ ℕ), HasMonotoneAP (⇑f) 4

OpenStatement only, no proof