---

Claim. There is a set of positive integers of density one whose increasing enumeration has distinct products on distinct consecutive blocks; the answer to the question is yes.

Submission note. Posted to erdosproblems.com as a proof claim by Animish Sharm (account AnimishSharma) on 26 July 2026, giving "Claude" as the AI used:

So the proof starts with taking a Greedy Scan (accept n unless a collision appears) then aften overlap cancellation P = nS then Localize left block and terminal suffix after this we can split this into 3 cases, case 1: far exponent branch: monotonicity lemma and direct endpoint count case 2: Dickman near-diagonal smooth factors case 3: Auxillary curves: shifted congruences and CCDN point counting. all rejection families are o(N) therefore the density one argument is settled Notes: The lean proof is dependent upon 3 axioms - matomakiTeravainenE2 - dickman_smooth_density - ccdn_slab_count all 3 are not present in mathlib, except these 3 the whole proof is formalized

The result. A proof claim submitted to the site on 26 July 2026 by the author of the GitHub repository Animish-Sharma/Erdos, whose folder 421 first appeared on 28 June 2026 in a commit titled "Solved 421"; the proof-claim entry says it was made using Claude. The summary: build the set by a greedy scan, accepting $n$ unless a collision appears; after cancelling the overlap of two equal block products, localize the earlier block and the terminal suffix; and dispose of the collision families in three cases, a far-exponent branch by a monotonicity lemma and a direct endpoint count, a near-diagonal case of smooth factors by Dickman-type estimates, and auxiliary curves by shifted congruences and the point counting of Castryck, Cluckers, Dittmann and Nguyen; every rejection family is $o(N)$, so the set has density one. The Lean file Erdos421.lean formalizes the argument except for three axioms, stated in the entry as results not in Mathlib: a theorem of Matomäki and Teräväinen on products of two primes in almost all very short intervals, a smooth-number density estimate, and a slab count from the dimension-growth theorem. The folder's commit history shows the first commit of 28 June 2026, the Lean file added on 2 July, a revision titled "421 complete" on 25 July and the branch D04-closed of 26 July 2026, which the proof claim submits. This page is named by the first posting; the site's proof claim of 26 July 2026 is the version linked above.

Standing. On 13 July 2026 the site's curator linked this attempt in the thread among claimed solutions that had not passed moderation, saying they had not read them in detail and made no claim about their correctness; the proof claim was accepted onto the proof-claim tab on 26 July. Pratt's digested proof of 1 September 2026 describes it as a different proof sharing some features with those of Chojecki and Sneiderman, formalized in Lean with the three literature results assumed as axioms; Pratt's note does not follow it. The problem's solved standing rests on Chojecki's claim and Sneiderman's claim, not on this one. Nobody is known to have reviewed the argument; the Lean development was neither built nor audited in this corpus, and a proof from axioms is not a kernel-checked proof of the statement. The repository's files are not held in this corpus; this page draws on the proof-claim entry and the commit listing.

Depends on. No page of this wiki.