A published paper or arXiv preprint answers the main question of Erdős Problem #424 (theorem erdos_424 in formal-conjectures) in full (proof, disproof, or the exact value asked for) with no hypotheses beyond the problem's own.

The problem, as stated in formal-conjectures (Apache 2.0):

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`.