Motivation

A permutation of $\mathbb{Z}$ in the sense of Erdős and Graham is a one-sided arrangement $a_0, a_1, a_2, \ldots$ in which every integer appears exactly once. Erdős Problem 195 (erdosproblems.com/195) asks for the largest $k$ such that every such arrangement contains a monotone $k$-term arithmetic progression: indices $i_1 < \cdots < i_k$ for which $a_{i_1}, \ldots, a_{i_k}$ is an increasing or a decreasing arithmetic progression. The question sits in the Ramsey-type study of how much arithmetic structure an ordering is forced to preserve, alongside its companion Problem 196 for permutations of $\mathbb{N}$.

Timeline of the known results:

• 1977. Davis, Entringer, Graham and Simmons (Acta Arith. 34) proved that every permutation of the positive integers contains a monotone 3-term progression, and that the positive integers can be permuted to avoid monotone 5-term progressions. Since the positive entries of a permutation of $\mathbb{Z}$ form a permutation of the positive integers, every permutation of $\mathbb{Z}$ contains a monotone 3-term progression.
• 2019. Geneson (Discrete Math. 342) constructed a permutation of $\mathbb{Z}$ with no monotone 6-term progression, so the answer is at most 5.
• 2022–2024. Adenwalla (arXiv:2211.04451, Discrete Math. 347 (2024) 114183) constructed a permutation of $\mathbb{Z}$ with no monotone 5-term progression, so the answer is at most 4.
• 2026. Ho (arXiv:2609.12780) constructed a permutation of $\mathbb{N}$ with no monotone 4-term progression, settling Problem 196, with a complete Lean 4 proof (github.com/boonsuan/4ap). Geneson (arXiv:2608.12604) proved $\beta_{\mathbb{Z}}(4)=1$: there are sets of integers with lower density arbitrarily close to $1$ that can be permuted to avoid monotone 4-term progressions.

The answer to Problem 195 is therefore $3$ or $4$, and it is $3$ exactly when some permutation of $\mathbb{Z}$ avoids monotone 4-term progressions.

Setting

A permutation of $\mathbb{Z}$ is a bijection $f : \mathbb{N} \to \mathbb{Z}$. A list of values is an arithmetic progression of length $k$ if it equals $a, a+d, \ldots, a+(k-1)d$ or the same list reversed. The function $f$ has a monotone $k$-AP if there are indices $b_1 < \cdots < b_k$ such that $f(b_1), \ldots, f(b_k)$ is an arithmetic progression of length $k$. For a bijection the common difference is automatically nonzero when $k \ge 2$.

Auxiliary objects used by the milestones:

1. For $\varepsilon : \mathbb{N} \to \{\mathrm{true},\mathrm{false}\}$, the $\varepsilon$-order $\prec_\varepsilon$ on $\mathbb{Z}$: for $x \ne y$, let $k = \nu_2(y-x)$ be the lowest binary position at which the two's-complement expansions of $x$ and $y$ differ; then $x \prec_\varepsilon y$ iff the $k$-th digit of $x$ is $1$ exactly when $\varepsilon(k)$ is true. With $\varepsilon \equiv \mathrm{true}$ this is the extension to $\mathbb{Z}$ of the order used by Ho.
2. For a relation $R$ and a finite duplicate-free word $P$ of integers, the completion $C(P)$ lists $P$ first, in order, followed by all other integers ordered by $R$. The word $P$ is safe if $C(P)$ has no monotone 4-term progression.
3. (No3AP): $R$ has no monotone 3-term progression. (Star): $a \mathrel{R} a+r \iff a+2r \mathrel{R} a+3r$ for every $a$ and every $r \ne 0$.

Formalization targets

Goal

$$\exists f : \mathbb{N} \simeq \mathbb{Z},\ f \text{ has no monotone 4-term arithmetic progression.}$$

Together with the known bounds this is equivalent to the answer to Problem 195 being $3$. A disproof would show that the answer is $4$.

Literature milestones

$$\forall f : \mathbb{N} \simeq \mathbb{Z},\ f \text{ has a monotone 3-AP}, \qquad \exists f : \mathbb{N}\simeq\mathbb{Z} \text{ with no monotone 5-AP}, \qquad \exists f : \mathbb{N} \simeq \mathbb{N} \text{ with no monotone 4-AP},$$

and the reduction: the supremum in the formal-conjectures statement equals $3$ iff the goal holds.

Structural milestones

The $\varepsilon$-orders are strict total orders with no monotone 3-term progression that satisfy (Star). They have no endpoints when $\varepsilon$ is not eventually constant. In every $\varepsilon$-order, a word listed in reverse order is safe. Conversely, a least element blocks every exhaustive chain of safe words, and the two's-complement order has least element $-1$.

Significance

A proof of the goal resolves Problem 195, determines the answer as $3$, and completes the classification of monotone progressions in one-sided permutations of $\mathbb{N}$ and $\mathbb{Z}$. A disproof gives the answer $4$ and is the first known statement separating the two problems. The formal-conjectures repository (195.lean) records the problem as open with an unspecified answer. The literature milestones have pen-and-paper proofs. Among them, only Ho's theorem for $\mathbb{N}$ has a machine-checked proof, in an external repository, so porting it is part of the work.

Difficulty

The natural first attempt transfers Ho's construction for $\mathbb{N}$ to $\mathbb{Z}$. Ho's argument builds the permutation as a limit of finite safe words. Each extension step uses that all values are nonnegative: for a progression $a, b, c, d$ with $c$ and $d$ not yet placed, the bound $d = 2c - b \le 2c$ controls which elements are forced. On $\mathbb{Z}$ this bound is lost. With the two's-complement completion order the obstruction is concrete: $-1$ is the least element, and once it is placed no later element can be the maximum or minimum of a safe word, so no chain of safe words can exhaust $\mathbb{Z}$. Any approach along these lines must therefore change the completion order between stages, for example through orders without endpoints, or use a different construction entirely.

Formalization scope

Permutations are f : ℕ ≃ ℤ. HasMonotoneAP, ListIsAPOfLength and ListIsAPOfLengthWith copy the formal-conjectures definitions verbatim, so the goal and the reduction milestone use the same objects as Erdos195.erdos_195. Progressions may be listed forwards or backwards, which covers increasing and decreasing ones. A zero common difference never arises because f is injective. Digits are two's-complement digits x / 2^k % 2 with floor division, and ν₂ is padicValInt 2. Safe quantifies over all integers a and all nonzero r of either sign. Everything lives in the namespace Erdos195.

The development needs only Mathlib's integers, lists and $p$-adic valuations. The $\varepsilon$-order lemmas and the completion lemmas are reusable for related arrangement problems, including Problem 196 and doubly infinite variants. Contributions are welcome on the literature milestones (in particular a port of Ho's Lean proof), on new orders with no endpoints, and on the goal in either direction.

Selected references

• J. A. Davis, R. C. Entringer, R. L. Graham, G. J. Simmons, On permutations containing no long arithmetic progressions, Acta Arith. 34 (1977), 81–90. https://doi.org/10.4064/aa-34-1-81-90
• J. Geneson, Forbidden arithmetic progressions in permutations of subsets of the integers, Discrete Math. 342 (2019), 1489–1491. https://doi.org/10.1016/j.disc.2019.02.004
• S. Adenwalla, Avoiding monotone arithmetic progressions in permutations of integers, Discrete Math. 347 (2024), 114183. https://arxiv.org/abs/2211.04451
• B. S. Ho, A 4AP-free permutation of the positive integers, arXiv:2609.12780 (2026). https://arxiv.org/abs/2609.12780 ; Lean proof https://github.com/boonsuan/4ap
• J. Geneson, Density bounds for permutations avoiding monotone arithmetic progressions, arXiv:2608.12604 (2026). https://arxiv.org/abs/2608.12604
• Erdős Problem 195, https://www.erdosproblems.com/195 ; formal-conjectures ErdosProblems/195.lean.