---

Claim. For integers $k\ge3$ and $1\le d_1<d_2$, the question of Problem 1112 has the answer yes exactly when $d_2\ge k+1$. The dichotomy answers the Statement (precise) of the problem for every triple $(k,d_1,d_2)$. Above the threshold a ratio linear in $d_2$ works: every sequence $B=\{b_1<b_2<\cdots\}$ of positive integers with $b_{i+1}\ge rb_i$ admits a sequence $A=\{a_1<a_2<\cdots\}$ with $d_1\le a_{i+1}-a_i\le d_2$ for all $i$ and $kA\cap B=\emptyset$, for $r=192d_2$ in the original development and for $r=d_2+2$ in the September revision of the paper. When $d_2\le k$ no ratio works, and more: for every sequence $R_1,R_2,\ldots$ of positive integers there is one $B$ with $b_{i+1}\ge R_ib_i$ that meets $kA$ for every such $A$. In the notation of the site's commentary (page last edited 28 December 2025), $r_k(d_1,d_2)$ exists if and only if $d_2\ge k+1$, and then $r_k(d_1,d_2)\le192d_2$, independently of $d_1$, with the revision claiming $r_k(d_1,d_2)\le d_2+2$; this agrees with the nonexistence of $r_3(2,3)$ that Bollobás, Hegyvári and Jin proved ([BHJ97], on its claim page). The write-up is J. Land, A sharp dichotomy for bounded-gap sumsets, Theorem 1 (eight pages, dated September 2026), at the pinned commit of 2026-09-13. Its existence half places, by a nested-interval argument, a real $\theta$ with $\{b_n\theta\}$ in a short fixed interval for all large $n$, and takes $A$ to be the integer parts of $\alpha(m+i)$ with $\alpha=1/\theta$ in $(d_2-1,d_2]$: the gaps are $d_2-1$ or $d_2$, and no $k$-fold sum of members of $A$ is a remaining term of $B$. Its nonexistence half shows that, for $d_2\le k$, the $k$-fold sumset of every admissible $A$ contains a full congruence class from some point on, through a density consequence of Kneser's theorem and a finite subset-sum lemma (a set $G$ of at least three positive integers with greatest common divisor $1$ and maximum $M$ has a multiset of at most $M-1$ members of $G$ whose subset sums contain $M$ consecutive integers), and then builds one $B$ meeting every such tail. The $k$-fold sumset allows repeated summands, as the site's $kA$ does. The result was first posted on the problem's discussion thread on 2026-07-06, with the original development (existence bound $192d_2$, archived on Zenodo on 2026-07-25 as the record linked above), and submitted as a proof claim on 2026-07-17; on 2026-09-13 the paper and the Lean proof were replaced by the shortened argument described here, which the paper says is based on a manuscript supplied by Stijn Cambie and which improves the bound to $d_2+2$. The revision's proof is not checked in this corpus.

Submission note. Posted to erdosproblems.com as a proof claim by Johan Land (account JohanLand) on 17 July 2026, giving "Fable 5, Opus 4.8, GPT 5.5 Pro" as the AI used:

Note: Proof previously discussed in the comment section before this "proof claim" functionality was added to the site. Briefly: For $k \ge 3$, $r_k(d_1,d_2)$ exists iff $d_2 \ge k+1$, with $r_k \le 192,d_2$ - independently of $d_1$. Existence: a Beatty sequence with slope $\gamma \in (k, d_2)$ confines $kA$ to width-$k$ windows, and a nested-interval argument steers $\gamma$ past every element of a lacunary $B$. Non-existence: a single diagonal $B$ works once every admissible $kA$ contains a full congruence class eventually; this reduces, via word combinatorics for two-letter gap alphabets (Sturmian case included) and a subset-sum lemma for larger ones - every finite $G$ with $\gcd(G)=1$, $|G|\ge 3$ admits a multiset of at most $\max G - 1$ elements whose subset sums contain $\max G$ consecutive integers. Context: Everything is verified in Lean (see link below). More info: I've structured a repo to ease consumption of the proof: https://github.com/beetree/math_erdos_1112

Formalization. The repository's lean/Erdos1112.lean defines RatioWorks k d₁ d₂ r (every $B$ with $b_1\ge1$, strictly increasing and $r\,b_i\le b_{i+1}$ admits an $A$ with $a_1\ge1$, gaps in $[d_1,d_2]$ phrased additively, and kFoldSumset k a disjoint from the range of $B$) and Question k d₁ d₂ as the existence of such a natural ratio; a bridge question_iff_questionInt proves the equivalence with the problem's integer ratio. lean/Erdos1112Proof/Final.lean proves erdos_1112: Question k d₁ d₂ ↔ k + 1 ≤ d₂ under 3 ≤ k, 1 ≤ d₁ and d₁ < d₂, with erdos_1112_int for the integer form, erdos_1112_existence_bound for the ratio $d_2+2$ and erdos_1112_strong_nonexistence for the varying-ratio form. The toolchain is Lean v4.27.0; the repository's readme says its audit file AxiomsCheck.lean permits only propext, Classical.choice and Quot.sound. These files show no sorry at the pinned commit of 2026-09-13; this corpus has not built, replayed or audited that revision. Boris Alexeev's lean-proofs repository added on 2026-08-26 a port of the original development (existence bound $192d_2$) to Lean 4.33, under Land's name as informal and formal author and citing the thread post and the original repository (src/latest/ErdosProblems/Erdos1112.lean, linked above at a pinned commit); this corpus built that port, as the Acceptance paragraph records.

Depends on. Nothing in this wiki; the argument is the paper's own.

Claimant and postings. The claimant is Johan Land, who directs and audits the work; the proof claim names Fable 5, Opus 4.8 and GPT 5.5 Pro as the systems used, and the paper's declaration says that in the original development Claude (Fable 5 and Opus 4.8) contributed to the mathematical arguments with GPT-5.5 and Gemini 3.1 consulted for advice and review, that GPT-6-Astra and Claude Sonnet 5 assisted with the revision and its formalization, and that the author takes responsibility for the claims. The comments on the proof claim carry a report of 2026-07-17 by a pseudonymous forum user who rebuilt the original Lean development from scratch, found that the kernel accepts the final theorems with only the three standard axioms and with no sorry and no native_decide, and ran the certificate harnesses; a remark of 2026-08-19 by Stijn Cambie that the hundred-page proof should be far shorter; and Land's notice of 2026-09-13 of the revised paper. The rebuild is by an unnamed user, not a named reviewer, so it adds no evidence kind.

Acceptance. Formalized. This corpus's verification built Boris Alexeev's lean-proofs repository at the pinned commit 8822f7dd of 2026-09-15, linked above (its src/latest project, Lean v4.33.0, Mathlib v4.33.0), whose module ErdosProblems/Erdos1112.lean and development ErdosProblems/Erdos1112/ are the port of Land's original development of July 2026, existence ratio $192d_2$, credited by the port's header to Land as informal and formal author; the September revision in Land's repository was not built, so the ratio $d_2+2$ is not formalized here. The verification checked the axioms of the four final theorems Erdos1112.erdos_1112, Erdos1112.erdos_1112_int, Erdos1112.erdos_1112_strong_nonexistence and Erdos1112.erdos_1112_existence_bound, which are exactly propext, Classical.choice and Quot.sound. The comparator challenge ComparatorChallenges/ErdosProblems/Erdos1112.lean of the same project pins the four declarations with the definitions their types reach (IsLacunaryWith, IsLacunaryWithInt, IsVarLacunaryWith, HasGapsIn and kFoldSumset), and the fingerprint of each declaration was found identical to the challenge's. The statements were audited clause by clause against the problem's Statement: erdos_1112 proves that for all $k\ge3$ and $1\le d_1<d_2$ some natural ratio $r$ works if and only if $k+1\le d_2$, and erdos_1112_int proves the same for an integer $r$, the site's wording; $B$ is infinite, strictly increasing and positive with $b_{i+1}\ge rb_i$, $A$ is infinite and positive with gaps in $[d_1,d_2]$ stated additively, $kA$ allows repeated summands, and $kA\cap B=\emptyset$ is taken literally. A finite $A$ would make the question trivial, and allowing a finite $B$ changes nothing. The build certifies the full answer this page claims, with the varying-ratio nonexistence for $d_2\le k$ (erdos_1112_strong_nonexistence) and the ratio $192d_2$ above the threshold (erdos_1112_existence_bound); it does not certify the ratio $d_2+2$. Not reviewed: on the discussion thread the site's curator, Thomas F. Bloom, wrote on 2026-07-13 that the main theorem erdos_1112 of the original development is a correct formalization of the claim and that the code compiles with no sorry, and that the curator had not yet tried to understand the proof; the site's label is OPEN (LEAN), its commentary (page last edited 28 December 2025) does not mention the claim, and the community database's formalization pointer names Land's repository as the solution; the curator has not marked the problem settled, so no reviewed evidence is listed. Not refereed: the write-up is posted in Land's repository and archived on Zenodo, with no journal publication.