Erdős Problem 342

References:

• erdosproblems.com/342
• Ben Green's Open Problem 7
• OEIS A002858
• [Gu04] Guy, Richard K., Unsolved problems in number theory (2004), xviii+437.

def Erdos342.UniqueUlamSum (a : ℕ → ℕ) (n m : ℕ) : Prop

UniqueUlamSum a n m means that $m$ has a unique representation as $a(i) + a(j)$ with $i < j < n$.

Equations

• Erdos342.UniqueUlamSum a n m = ∃! p : ℕ × ℕ, p.1 < p.2 ∧ p.2 < n ∧ m = a p.1 + a p.2

def Erdos342.IsUlamSequence (a : ℕ → ℕ) : Prop

IsUlamSequence a means that $a$ is the Ulam sequence (OEIS A002858): $a(0) = 1$, $a(1) = 2$, and for each $n \geq 2$, $a(n)$ is the least integer greater than $a(n-1)$ that has a unique representation as $a(i) + a(j)$ with $i < j < n$.

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos342.erdos_342.test.a0 (a : ℕ → ℕ) : IsUlamSequence a → a 0 = 1

$a(0) = 1$ by definition.

theorem Erdos342.erdos_342.test.a1 (a : ℕ → ℕ) : IsUlamSequence a → a 1 = 2

$a(1) = 2$ by definition.

theorem Erdos342.erdos_342.test.a2 (a : ℕ → ℕ) : IsUlamSequence a → a 2 = 3

$a(2) = 3$: the only pair $(i,j)$ with $i < j < 2$ is $(0,1)$, giving $1 + 2 = 3$.

theorem Erdos342.erdos_342.test.a3 (a : ℕ → ℕ) : IsUlamSequence a → a 3 = 4

$a(3) = 4$: among sums $> 3$ with a unique representation from $\{1,2,3\}$, the smallest is $4 = 1 + 3$. The candidate $5 = 2 + 3$ is ruled out by minimality since $4$ has a unique representation.

theorem Erdos342.erdos_342.parts.i : True ↔ ∀ (a : ℕ → ℕ), IsUlamSequence a → {n : ℕ | ∃ (m : ℕ), a m = a n + 2}.Infinite

Do infinitely many pairs $(a, a+2)$ occur in Ulam's sequence?

theorem Erdos342.erdos_342.parts.ii : True ↔ ∀ (a : ℕ → ℕ), IsUlamSequence a → have d := fun (n : ℕ) => ↑(a (n + 1)) - ↑(a n); ∃ p > 0, ∀ᶠ (m : ℕ) in Filter.atTop, d (m + p) = d m

Does Ulam's sequence eventually have periodic differences? That is, is $a(n+1) - a(n)$ eventually periodic?

theorem Erdos342.erdos_342.parts.iii : True ↔ ∀ (a : ℕ → ℕ), IsUlamSequence a → (Set.range a).upperDensity = 0

Part (iii), is the density of the sequence 0?