Erdős Problem 195

References:

• erdosproblems.com/195
• [Ad22] Adenwalla, S., Avoiding Monotone Arithmetic Progressions in Permutations of Integers. arXiv:2211.04451 (2022).
• [Ge19] Geneson, Jesse, Forbidden arithmetic progressions in permutations of subsets of the integers. Discrete Math. (2019), 1489-1491.

theorem Erdos195.erdos_195 : sorry = sSup {k : ℕ | ∀ (f : ℤ ≃ ℤ), HasMonotoneAP (⇑f) k}

What is the largest $k$ such that in any permutation of $\mathbb{Z}$ there must exist a monotone $k$-term arithmetic progression $x_1 < \cdots < x_k$?

theorem Erdos195.erdos_195.variants.leq_5_bound : 5 ≥ sSup {k : ℕ | ∀ (f : ℤ ≃ ℤ), HasMonotoneAP (⇑f) k}

Geneson [Ge19] proved that k ≤ 5.

theorem Erdos195.erdos_195.variants.leq_4_bound : 4 ≥ sSup {k : ℕ | ∀ (f : ℤ ≃ ℤ), HasMonotoneAP (⇑f) k}

Adenwalla [Ad22] proved that k ≤ 4.