Problem detail · source-aware
VibeMathed reports this item as candidate. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Let $a_1 = 2$ and $a_2 = 3$ and continue the sequence by appending to $a_1, \dots, a_n$ all possible values of $a_ia_j - 1$ with $i \ne j$. Is it true that the set of integers which eventually appear has positive density?
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement fidelity, correctness, priority, or novelty.
GPT-5.6 Pro developed the argument together with Samuel Korsky, in particular searching for the transition matrices the interval-partition argument needs. The Lean formalization was produced separately, with Codex, by Boris Alexeev.
Provider: OpenAI · Prompt public: unknown · Independence: unknown
Lean 4.32.0 and Mathlib v4.32.0 formalization by Boris Alexeev, produced with Codex, from the informal argument of Samuel Korsky and GPT-5.6 Pro. Rebuilt independently on 2026-08-02 against Lean 4.32.0 and Mathlib v4.32.0 (the file as published, sha256 ca4a2371918b1a7c66dccfe324305298): all 6,394 lines compile in 1,215 s with no sorry and no admit, and #print axioms reports the top theorem depending on exactly [propext, Classical.choice, Quot.sound], the three standard Lean axioms, with no sorryAx and nothing assumed. The formalized conclusion is positive lower density, stated against the same nextGeneration, sequenceSet and generatedSet definitions the Formal Conjectures statement of #424 uses. Status is candidate rather than resolved because erdosproblems.com has not accepted the claim: its proof-claims page states plainly that appearing there is no guarantee of correctness and does not mean anyone associated with the site examined any part of the proof.
Correctness: supported · statement fidelity: audited · peer review: none
Proves positive lower density. The Formal Conjectures encoding asks for Set.HasPosDensity, a density that exists and is positive; erdosproblems.com says Erdos most likely meant lower density.
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.