Erdős Problem #424

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? As explained on [erdosproblems.com/424](https://www.erdosproblems.com/424), "positive density" here means positive *lower* density: is there \(c > 0\) such that for all large \(x\) at least \(cx\) of the integers in \([1, x]\) appear? See `erdos_424.variants.exact_density` for the literal reading. The answer is yes: Korsky [Ko26] (with ChatGPT 5.6 Pro) proved that the set has positive lower density. The linked formal proof (Alexeev and Codex) shows that there is `c > 0` with `c * x ≤ #{n ∈ [1, x] | n ∈ generatedSet}` for all large `x`, which gives `c / 2 ≤ generatedSet.lowerDensity`.