Erdős Problem 424: Sequence generated by $a_i a_j - 1$

References:

• erdosproblems.com/424
• A005244
• [Ben Green's Open Problem 63](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#section.8 Problem 63)

def Erdos424.nextGeneration (A : Set ℕ) : Set ℕ

Defines the set of new numbers generated from a set A by the operation $x y - 1$ for $x \neq y$.

Equations

• Erdos424.nextGeneration A = {z : ℕ | ∃ (x : ℕ) (y : ℕ), x ∈ A ∧ y ∈ A ∧ x ≠ y ∧ z = x * y - 1}

def Erdos424.sequenceSet : ℕ → Set ℕ

The sequence of sets $A_n$ where $A_0 = \{2, 3\}$ and $A_{n+1}$ is $A_n$ union all newly generated elements.

Equations

• Erdos424.sequenceSet 0 = {2, 3}
• Erdos424.sequenceSet n.succ = Erdos424.sequenceSet n ∪ Erdos424.nextGeneration (Erdos424.sequenceSet n)

def Erdos424.generatedSet : Set ℕ

The set of integers which eventually appear in the sequence, which is the union of all $A_n$.

Equations

• Erdos424.generatedSet = ⋃ (n : ℕ), Erdos424.sequenceSet n

theorem Erdos424.erdos_424 : generatedSet.HasPosDensity ↔ sorry

Let $a_1 = 2$ and $a_2 = 3$ and continue the sequence by appending to $a_1, \ldots, a_n$ all possible values of $a_i a_j - 1$ with $i \neq j$. Is it true that the set of integers which eventually appear has positive density?