---

Claim. Let $A$ be the smallest set of positive integers that contains $2$ and $3$ and contains $ab-1$ whenever $a,b\in A$ are distinct. Then $A$ has positive lower density: there is a constant $c>0$ with $|A\cap[1,x]|\ge cx$ for all large $x$. This answers the precise Statement of Problem 424 yes. The claim says nothing about whether the natural density of $A$ exists, the natural-density variant recorded on the problem page.

Submission note. Posted to erdosproblems.com as a proof claim by Samuel Korsky (account SamKorsky) on 20 July 2026, giving "GPT 5.6-Pro" as the AI used:

Identical to the partial proof claim summary: the idea is to produce many distinct affine maps with a common slope (using initial elements of the sequence $2, 3, 5, 9, 14$) and use a finite interval partition with transition probabilities to distinguish the resulting maps. Notes: Comments are welcome, particularly on exposition and readability which I'm working on improving.

Posted to erdosproblems.com as a proof claim by Samuel Korsky (account SamKorsky) on 18 July 2026, giving "GPT 5.6-Pro" as the AI used:

I believe I am able to prove (with help from GPT-5.6 Pro) the positive lower density claim for a more favorable sequence (namely, removing the $i \ne j$ restriction). The general idea is to produce many distinct affine maps with a common slope (using initial elements of the sequence $2, 3, 5, 8, 9$) and use a finite interval partition with transition probabilities to distinguish the resulting maps. Comments are welcome! Notes: Some remarks with regards to the literature: [Er77c] states the problem exactly as written here, while the wording in Green's open problem list allows for a1 = a2 (the case studied here). However, given that Green cites this page and Erdos directly, I assume this difference was unintentional. Additionally, I spent some time prompting GPT 5.6-Pro about developing a similar argument for the exact problem here, but was only able to GPT to claim (not human-verified) a proof that if $A$ is the set corresponding to the sequence in the problem, then $|A \cap [1,x]| \gg \frac{x}{\sqrt{\log x}}$. If there's interest I can try to verify its correctness and write it up.

Argument, as the claimant describes it. The write-up fixes the multipliers $2,3,5,9,14$, all early members of the sequence, and evaluates compositions of the affine maps $x\mapsto mx-1$ at $17$, so that the distinct-factor condition is met. Many compositions share one slope, a product of the multipliers; a finite partition of an interval into states, with transition probabilities between the states, is used to show that distinct compositions with a common slope land on distinct integers often enough to give the linear lower bound. The author credits an AI system, GPT 5.6-Pro as the proof-claim tab names it, with much of the calculation. This corpus has not reviewed the argument.

Postings. A partial claim of 18 July 2026 claimed a proof of the positive-lower-density statement for the variant sequence in which the factors may coincide, that is, $a_i^2-1$ is adjoined too, using the multipliers $2,3,5,8,9$; the author notes that this variant is the wording of Green's open problem list, while Erdős's own statement and the site require distinct factors. Korsky's comment of 19 July 2026 announced that the same interval-coding argument extends to the problem as stated, and the full claim of 20 July 2026 carries that extension; this page is dated by the full claim, the first posting of the result it records. The preprint "Positive Lower Density for Hofstadter's $ab-1$ Problem" (arXiv:2608.07910, version 1 of 8 August 2026, CC BY 4.0) is the same result.

Formalization. On 22 July 2026 Boris Alexeev reported in the claim's thread that an AI system (Codex) had formalized the proof in Lean 4, and confirmed that the formal statement is correct, with "positive density" read as positive lower density. The file in Boris Alexeev's public repository plby/lean-proofs (linked above at the pinned commit of 15 September 2026; toolchain comment Lean 4.33.0, Mathlib v4.33.0; informal authors the AI system and Korsky, formal authors Codex and Alexeev) declares itself a formalization of Korsky's result and states Erdos424.erdos_424: some $c>0$ has $c\,x\le|\{n\in[1,x]:n\in\texttt{generatedSet}\}|$ for all large $x$, where generatedSet is the staged-set definition of formal-conjectures. It is linked here as a formalization of this claim, not as a result of its own. On 21 September 2026 formal-conjectures retagged its statement erdos_424 (answer yes, $0<$ lower density) research solved, citing the preprint and linking that file as the formal proof, while its own theorem keeps a sorry and its variant exact_density, the existence of a positive natural density, stays research open; the statement file is linked above as a record of that tag, since a statement with a sorry body is not a formalization. This corpus's verification built the src/latest folder of plby/lean-proofs at the pinned commit (2026-09-15; Lean v4.33.0, Mathlib v4.33.0) and checked the axioms of Erdos424.erdos_424, which are exactly propext, Classical.choice and Quot.sound; the solution contains no sorry, admit, added axiom or native_decide. The repository's comparator challenge for the problem pins that declaration, and the fingerprint of its type and of the definitions nextGeneration, sequenceSet and generatedSet it reaches was found identical in the challenge and in the solution. The file also proves that the staged set equals the smallest set containing $2$ and $3$ and closed under $ab-1$ for distinct $a$ and $b$, and every element is at least $2$, so subtraction on the natural numbers never truncates. The statement was audited clause by clause against the Claim: it states positive lower density of the distinct-factor set, with $x$ running over the natural numbers, which changes nothing since the bound passes to real $x$ with $c/2$, and it says nothing about whether the natural density exists. What was built is the file at the pinned commit; the repository's copy for Lean and Mathlib v4.32.0 was not built.

Depends on. No page of this wiki. The write-up is self-contained apart from elementary properties of the sequence's early terms.

Acceptance. Accepted on formalized evidence, on the precise Statement; the natural-density variant stays open. The acceptance rests on the build and statement audit recorded under Formalization; the kernel-checked proof does not rely on the informal write-up. The site's label is OPEN (page last edited 31 March 2026, proof-claims thread accessed 2026-10-06); the site's curator commented in the thread only on the write-up's style. The thread holds Alexeev's confirmation of the formal statement and a pseudonymous check of 22 July 2026, run with GPT-5.6 Pro, that found the proof correct but flagged three steps as not fully justified: the convex-hull assertion of Section 2, the claim that the interval-state path determines the multiplier sequence (Section 4), and the supermartingale property of the stopped process on which the hitting-time estimate rests; the author replied that an earlier draft contained these details and agreed to restore them. These are gaps in the informal write-up only. The thread also holds one critical reading, a comment of 22 July 2026 by the site user Woett that the write-up is unintelligible after the theorem statement, with a guessed outline of the idea: the set containing $17$ and closed under $b\mapsto ab-1$ for $a\in\{2,3,5,9,14\}$ sits inside $A$, so it suffices to show that this set has positive lower density; the author confirmed that this is the central idea. Not reviewed: there is no acceptance by the site, and Alexeev co-authored the formalization, so Alexeev's confirmation of the statement is the formalizers' own and not an independent acceptance. Not refereed: there is no refereed version.