Distinct consecutive products in a density-one set via prime-gap deletions

Abstract

The preprint constructs a subset of the natural numbers of natural density one whose increasing enumeration has pairwise distinct finite consecutive products, resolving Erdős Problem 421. The proof combines a sparse deletion scheme based on prime-gap interiors and connector intervals with a structural analysis of possible product collisions, integral-point estimates for separated-variable curves, and results on primes in almost all short intervals. Version 2 adds a Lean 4 formalization of the main theorem, a supplement describing the formalization, and the report of an independent verification. The preprint and its LaTeX source are unchanged from version 1. Files Erdos421_submission_named.pdf and Erdos421_submission_named.tex: the preprint and its source, unchanged from version 1. Erdos421_lean_supplement.pdf and Erdos421_lean_supplement.tex: a 13-page supplement that states the formal theorem and its hypotheses, gives a lemma-by-lemma correspondence between the paper and the Lean declarations, lists the points at which the formal proof departs from the text, and describes the verification procedure. Erdos421-lean.zip: the Lean project. It contains 142 library modules, the root module, the axiom audit Audit.lean, the verification drivers, the pinned toolchain and dependency manifest, a plain-text correspondence table and a checksum manifest. VERIFICATION.txt: the completed independent verification report, including logs. CHANGES.md: the review findings and the changes made in this version. README.txt and SHA256SUMS: an inventory of the submission set and SHA-256 hashes of every file in it. The formal result The final theorem of the development is stated in Erdos421/SourceConclusion.lean: theorem main_of_cited_analytic_inputs (hJ : JiaShortIntervalBound) (hCCDN : CCDNPlaneBound) : MainStatement MainStatement is Theorem 1 of the paper with the sequence indexed from 0: there is a strictly increasing sequence of positive integers whose range has natural density one and whose inclusive consecutive products are pairwise distinct. The two hypotheses are the only inputs from the literature that are not formalized. CCDNPlaneBound is the plane case, at integer radii, of the affine-curve bound of Castryck, Cluckers, Dittmann and Nguyen (Theorem 19 of the paper). JiaShortIntervalBound is the prime-existence consequence of Jia's theorem on primes in almost all short intervals (Section 5 of the paper). Both are ordinary propositions passed to the theorem as arguments; neither is an axiom of the development. The hypotheses are used only for the density-one conclusion. The absence of collisions in the constructed set is proved without them (eventually_manuscript_no_block_collision in Erdos421/Paper.lean). The formalization fixes one admissible parameter value, ε = 1/1000, and in places uses documented sufficient variants of the paper's intermediate estimates. It establishes the main conclusion from the two cited inputs; it does not reproduce every displayed estimate in the paper verbatim. Verification The project pins Lean leanprover/lean4:v4.19.0 and Mathlib commit c44e0c8ee63ca166450922a373c7409c5d26b00b. The sources contain no sorry, no axiom declarations, no native_decide, and no unsafe or implemented_by declarations. An independent verification completed on 10 September 2026 checked all 143 modules with Lean's frontend and kernel at trust level 0 and confirmed that each of the 927 public theorems depends only on the standard axioms propext, Classical.choice and Quot.sound. Every proof source and Audit.lean in this version is byte-identical to the files that were checked. The changes in version 2 are limited to documentation and to the status wording of the verification drivers, as recorded in CHANGES.md. To reproduce the check, run lake exe cache get, lake build and lake env lean Audit.lean inside Erdos421-lean/, or run python3 verify.py. To verify the downloaded files, unzip Erdos421-lean.zip next to the other files and run sha256sum -c SHA256SUMS. Declaration of generative AI and AI-assisted technologies During the preparation and revision of the manuscript, the Lean development and the supplement, the author used AI assistants, including OpenAI's GPT-5.6 and Anthropic's Claude Opus 4.8, for critical review of proofs, drafting and revising Lean proofs, consistency checking, proofreading and editorial revision. Every Lean proof in the archive is checked by the Lean kernel as described in the supplement, and this check does not depend on the origin of the proof text. The author reviewed and evaluated all model-generated output, made all final mathematical and editorial decisions, and takes full responsibility for the content. No AI system is listed as an author.