Erdős #195: a permutation of $\mathbb{Z}$ with no monotone $4$ -term AP

Open

Erdos195.erdos_195_exists_fourAP_free

by Ethan Cheung Wang · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

arithmetic-progressionscombinatoricserdos-problems

There is an arrangement $a_0,a_1,a_2,\dots$ of all the integers, each appearing exactly once, with no monotone $4$ -term arithmetic progression:

\exists f:\mathbb{N}\simeq\mathbb{Z}\ \text{ such that there are no } i_1<i_2<i_3<i_4 \text{ with } f(i_1),f(i_2),f(i_3),f(i_4) \text{ an increasing or decreasing AP.}

Since every permutation of $\mathbb{Z}$ contains a monotone $3$ -term progression (Davis–Entringer–Graham–Simmons 1977), this statement says that the answer to Erdős Problem 195 is $3$ . Its negation says that the answer is $4$ (Adenwalla 2024 gives the upper bound $4$ ).

Formalization Note Permutations are f : ℕ ≃ ℤ; HasMonotoneAP is copied verbatim from formal-conjectures (FormalConjecturesForMathlib/Combinatorics/AP/Basic.lean): a list of indices l with l.Pairwise (· < ·) whose image is an arithmetic progression of length $k$ , listed forwards or backwards.

Preamble

import Mathlib
import Definitions.Def_Erdos195_defs

Formal statement

namespace Erdos195

theorem erdos_195_exists_fourAP_free : ∃ f : ℕ ≃ ℤ, ¬ HasMonotoneAP f 4 := by sorry

end Erdos195

Source

Erdős Problem 195, https://www.erdosproblems.com/195 ; google-deepmind/formal-conjectures FormalConjectures/ErdosProblems/195.lean (erdos_195). Open.

Human review

Endorsed by Shuze Chen · Oct 23, 2026
Confirmed by the moderator at approval.
Endorsed by Ethan Cheung Wang · Oct 23, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Erdős #195: a permutation of Z\mathbb{Z}Z with no monotone 444-term AP

Erdős #195: a permutation of $\mathbb{Z}$ with no monotone $4$ -term AP