A
Bounded gaps
A walk along the number line whose steps all lie between d₁ and d₂. The even numbers, any arithmetic progression, or the wobbling (2,4)-walk below.
Erdős problems · No. 1112 · July 2026
The Lacunary Dichotomy
A sparse sequence can dodge a bounded-gap k-fold sumset if and only if the gap window clears a single integer threshold. That settles the question Erdős and Graham recorded in 1980.
Theorem · Johan Land · Lean 4 · sorry-free
Let k ≥ 3 and 1 ≤ d1 < d2 be integers. Write kA for the k-fold sumset of a sequence A of positive integers — all sums of k terms, repetitions allowed. Call B lacunary of ratio r if bi+1 ≥ r bi. Erdős asked: does there exist an integer r such that every such B admits a sequence A whose consecutive gaps all lie in [d1, d2] and (kA) ∩ B = ∅? Write rk(d1, d2) for the least such r, if any.
Theorem (Land, 2026)
The ratio exists if and only if d2 ≥ k + 1. When it exists, rk ≤ 192 d2.
Below the cut the obstruction is strong: for every prescribed sequence of pointwise lower bounds on the successive ratios of B, however rapidly growing, a single B meets the k-fold sumset of every admissible A. The case k = 2 was already settled — the ratio exists and is at most 2 (Chen, 2000; Bollobás–Hegyvári–Jin, 1997 for (2,3)).
The two characters
A bounded-gap walk, and a sparse set it must miss
kA
k-fold sumset
Every sum of k members of A, the same member reusable. Much denser than A. Not the set of k-multiples.
B
Lacunary
Successive terms grow at least by a factor r. Powers of ten, or anything thinner. The holes are the room the construction uses.
A (2,4)-walk and its 3-fold sumset
A
3A
The dichotomy, as a machine
Does rk(d1, d2) exist?
Set the fold k and the gap window. The whole question collapses to one comparison: the largest allowed gap against k + 1.
Exists
r_3(2,4) exists and is at most 768.
Explicit ratio: any B with successive ratio at least 768 admits such an A. The constant 192 is not optimized.
Threshold: existence iff d2 ≥ k + 1. Here k + 1 = 4, so the window clears it.
The threshold for k = 5
2
3
4
5
6
7
8
9
10
11
12
13
no ratio worksr ≤ 192 d₂ worksd₂ →
The cut, in numbers
Existence begins at d₂ = k + 1. The listed bound is 192·d₂ at that first working window.
| k | first d₂ | r ≤ |
|---|---|---|
| 3 | 4 | 768 |
| 4 | 5 | 960 |
| 5 | 6 | 1152 |
| 6 | 7 | 1344 |
| 8 | 9 | 1728 |
| 10 | 11 | 2112 |
A walk with bounded gaps
Steer A so that 3A misses B
Tap a gap to take the next step. The lower row is the 3-fold sumset of the finite walk so far. Seal marks are a toy lacunary B (ratio 3). This is the problem in miniature: keep the dense row off the sparse one.
A
3A
Collisions with B: 3. Window vs threshold: d₂ ≥ k+1 = 4, so the infinite theorem says a large enough ratio exists.
A digest of the argument
Four stages, one cut
Land's paper runs long on purpose: three backgrounds meet, and a finite certificate layer has to be checkable by a human who is not already fluent in all of them. What follows is the spine. The Lean files that check each stage sit at github.com/beetree/math_erdos_1112.
- I
Existence — Beatty through the holes
When d2 ≥ k + 1 the gap window is wide enough that a walk A can be steered around the k-fold constraints imposed by any sufficiently lacunary B. A lacunary sequence with large ratio leaves enormous empty intervals. Nested-interval / Beatty bookkeeping places the next term of A inside [ai + d1, ai + d2] so that no k-sum lands on a point of B.
The construction yields the explicit (unoptimized) bound rk(d1, d2) ≤ 192 d2. Lean: Existence/.
- II
Non-existence — words, then a slot
When d2 ≤ k, no growth condition on B is enough. The gap sequence of any admissible A is an infinite word on the alphabet {d1, …, d2}. Combinatorics on words (balanced words, Morse–Hedlund, Sturmian ladders) plus an amortized slot argument produce, from A, a finite set of generators G to which a covering lemma applies. One carefully chosen lacunary B then hits kA for every such A at once.
This is the strong form: the ratio sequence of B may be prescribed in advance, arbitrarily rapidly growing. Lean: NonEx/.
- III
(SHARP) — a bounded subset-sum theorem
The reduction lands on a finite additive-combinatorics lemma of possible independent interest.
|G| ≥ 3, gcd(G) = 1, max(G) = M
⇒ a multiset of ≤ M − 1 elements of G whose subset sums cover M consecutive integers.The proof is a six-branch decision tree (cases D, P, L, E, T, B). Its finite certificate layer — hundreds of small integer rows — is checked three ways: two independent Python harnesses, and the Lean kernel, with no native_decide. Lean: Sharp/.
- IV
Assembly
Existence supplies one side of the iff, with the ratio 192·d2. Strong non-existence supplies the other. Both directions are inhabited, so the biconditional is not vacuous. The three theorems are stated against a frozen definition file and proved in Erdos1112Proof/Final.lean.
Sources
Proved, machine-checked, awaiting the ledger
Community "closed" on erdosproblems.com/1112 means Thomas Bloom accepts a solution. The mathematics is complete: a sorry-free Lean 4 development, axioms only propext, Classical.choice, Quot.sound, and a human paper written from first principles. Bloom has confirmed that the Lean statement matches the recorded question. What remains is editorial digestion — which this page is for.
Credit is not ambiguous. The theorem is Johan Land's (July 2026). The core reasoning was carried by Claude, with GPT and Gemini in an adversarial role; Land directed, audited, and takes responsibility. This digest does not claim authorship of the proof. It is a public instrument for reading the dichotomy.
Citation
Land, J. (2026). A dichotomy for k-fold sumsets of bounded-gap sequences (Erdős problem 1112). https://github.com/beetree/math_erdos_1112 doi:10.5281/zenodo.21568276