Erdős Problem 1112: Lacunary Sequences and k-fold Sumsets Disjointness

### What is the conjecture

Given integers $1 \leq d_1 < d_2$ and $k \geq 3$: Does there exist an integer $r$ such that for any lacunary sequence $B = \{b_1 < b_2 < \cdots\}$ of positive integers with $b_{i+1} \geq rb_i$, there exists a sequence $A = \{a_1 < a_2 < \cdots\}$ satisfying:
1. $d_1 \leq a_{i+1} - a_i \leq d_2$ for all $i \geq 1$
2. $(kA) \cap B = \emptyset$

where $kA$ denotes the $k$-fold sumset (all sums of $k$ elements from $A$ with repetition allowed)?

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://www.erdosproblems.com/1112

### Prerequisites needed

**Formalizability Rating:** 3/5 (0 is best) (as of 2026-02-01)

Building blocks (1-3; from search results):
- Finset and Set operations for representing sequences and sumsets
- Natural numbers and integer arithmetic for gaps and lacunary conditions

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition and infrastructure for $k$-fold sumsets (Mathlib has Finset.sum but not the specific $kA$ summation convention)
- Lacunary sequence characterization as a predicate on sequences of naturals

Rating justification (1-2 sentences): The basic mathematical objects (sets, integers, sequences) exist in Mathlib, but formalizing the specific notion of $k$-fold sumsets and the lacunary condition requires moderate new definitions tailored to this problem. The statement itself is clear and can be expressed using Mathlib's type theory, but some infrastructure for additive combinatorics idioms is needed.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-05
* ams-11

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)