Adenwalla: a permutation of $\mathbb{Z}$ with no monotone $5$ -term AP

Proved

Erdos195.adenwalla_fiveAP_free

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

arithmetic-progressionscombinatoricserdos-problems

There is a bijection $f:\mathbb{N}\to\mathbb{Z}$ with no monotone $5$ -term arithmetic progression.

\exists f:\mathbb{N}\simeq\mathbb{Z}\ \text{ with no } i_1<\dots<i_5 \text{ such that } f(i_1),\dots,f(i_5) \text{ is an increasing or decreasing AP.}

This is the upper bound $K\le4$ in Erdős Problem 195.

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 adenwalla_fiveAP_free : ∃ f : ℕ ≃ ℤ, ¬ HasMonotoneAP f 5 := by sorry

end Erdos195

Source

S. Adenwalla, Avoiding monotone arithmetic progressions in permutations of integers, Discrete Math. 347 (2024) 114183, arXiv:2211.04451, Theorem 1

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

Adenwalla: a permutation of Z\mathbb{Z}Z with no monotone 555-term AP

Adenwalla: a permutation of $\mathbb{Z}$ with no monotone $5$ -term AP