Prove2Me

Erdős #195 reduction: the answer is 33 iff some permutation of Z\mathbb{Z} avoids monotone 44-APs

Proved
Erdos195.answer_eq_three_iff

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

arithmetic-progressionscombinatoricserdos-problems

Let K=sup⁡{k∈N:every bijection f:N→Z has a monotone k-term AP}K=\sup\{k\in\mathbb{N} : \text{every bijection } f:\mathbb{N}\to\mathbb{Z} \text{ has a monotone } k\text{-term AP}\}, the quantity in the formal-conjectures statement of Erdős Problem 195. Then

K=3  ⟺  ∃f:N≃Z with no monotone 4-term AP.K=3 \iff \exists f:\mathbb{N}\simeq\mathbb{Z} \text{ with no monotone } 4\text{-term AP}.

This connects the mission goal to the formal-conjectures answer variable; it follows from the bounds 3≤K≤43\le K\le 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 kk, listed forwards or backwards.

Preamble
import Mathlib
import Definitions.Def_Erdos195_defs
Formal statement
namespace Erdos195

theorem answer_eq_three_iff :
    sSup {k : ℕ | ∀ f : ℕ ≃ ℤ, HasMonotoneAP f k} = 3 ↔ ∃ f : ℕ ≃ ℤ, ¬ HasMonotoneAP f 4 := by sorry

end Erdos195
Source
formal-conjectures ErdosProblems/195.lean (erdos_195, erdos_195.variants.leq_4_bound); Davis et al. 1977; Adenwalla 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