The sequence $a+(2^i-1)r$ contains no 3-term arithmetic progression

Proved

Erdos195.doubling_seq_no_three_ap

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

arithmetic-progressionscombinatoricserdos-problems

Let $a,r\in\mathbb{Z}$ with $r\neq0$ and $x_i=a+(2^i-1)r$ for $i\in\mathbb{N}$ . Then no term is the average of two other terms: for all $i,j,l$ with $i\neq l$ ,

2x_j\neq x_i+x_l,

since this would force $2^{j+1}=2^i+2^l$ with $i\neq l$ . The sequence $(x_i)$ is the orbit of iterated fourth-term completions $x_{i+2}=3x_{i+1}-2x_i$ appearing in tree-witness constructions for Erdős Problem 195; it contains no nonconstant $3$ -term arithmetic progression.

Formalization note: stated for natural-number indices with 2 ^ i computed in ℤ.

Preamble

import Mathlib
import Definitions.Def_Erdos195_tree

Formal statement

namespace Erdos195

theorem doubling_seq_no_three_ap (a r : ℤ) (hr : r ≠ 0) (i j l : ℕ) (hil : i ≠ l) :
    2 * (a + (2 ^ j - 1) * r) ≠ (a + (2 ^ i - 1) * r) + (a + (2 ^ l - 1) * r) := by sorry

end Erdos195

Source

Erdős Problem 195 (https://www.erdosproblems.com/195); statements from GPT 6 Astra (Oct 23 2026 'tree' answers tree10, generalized), Lean-verified by Grok Bot for Ethan Cheung

View graph

The sequence a+(2i−1)ra+(2^i-1)ra+(2i−1)r contains no 3-term arithmetic progression

The sequence $a+(2^i-1)r$ contains no 3-term arithmetic progression