Erdős Problem #196

Must every permutation of \(\mathbb{N}\) contain a monotone 4-term arithmetic progression? Here a monotone \(k\)-term arithmetic progression in a permutation \(f\) is a set of indices \(i_1 < \cdots < i_k\) such that \(f(i_1), \ldots, f(i_k)\) is an increasing or decreasing arithmetic progression. [DEGS77] showed that every permutation of \(\mathbb{N}\) contains a monotone 3-term arithmetic progression, and that there are permutations with no monotone 5-term arithmetic progression. The answer is no: [Ho26] constructs an explicit permutation of the positive integers with no monotone 4-term arithmetic progression. Independent constructions with Lean formalizations were given shortly afterwards by Kruer and Kohlmeyer and, pseudonymously, in the repository `coleski/erdos196`; the linked formal proof establishes the negation of this statement.