← All papers
First page of Solutions to several problems on infinite sumset configurations

Solutions to several problems on infinite sumset configurations

Shisheng Li, Yong Su

math.CO Oct 29, 2026 · v1 math.DS math.NT
The main theorem and most other results are formalized in Lean 4 with Mathlib; some published theorems enter as explicit hypotheses. No sorry or axioms are used.
We resolve a number of the problems collected by Kra, Moreira, Richter and Robertson in their survey "Problems on infinite sumset configurations in the integers and beyond". Our main result is that in every countably infinite abelian group, every set of positive upper Banach density contains a sumset $B_1+\dots+B_k$ of $k$ infinite sets, for every $k$; the proof uses the Kronecker factor, but no higher-order Host-Kra structure theory, nilsystems of step greater than one, or nilspaces. We also answer, positively or negatively, questions on monochromatic sets $B+mB$, on sumsets in sets of logarithmic density, on polynomial sumset configurations, on sums of the form $B_{i_1}+\dots+B_{i_m}$ with $B_i$ drawn from a density family, on random sets, on ordered sumsets in shifted primes, on sums and products in $\mathbb{N}$ and $\mathbb{Q}$, and on sumsets in abelian groups. Several of these answers concern the questions as literally stated, and two follow directly from known examples; in each case we say so and discuss the natural corrected question. Finally, answering a question of Kousek and Radić, we show that the supremum of the lower Banach densities of sets $A\subset\mathbb{N}$ such that $B+B+t\not\subset A$ for every infinite $B\subset\mathbb{N}$ and every $t\ge0$ (respectively $B+B\not\subset A$ for every infinite $B$) is $1/2$ (respectively $3/4$). The main theorem and most of the other results are formalized in Lean 4, with some published theorems entering as explicit hypotheses.

Kra, Moreira, Richter and Robertson's survey poses many open questions on infinite sumset configurations in sets of positive density in the integers, in abelian groups and in other settings. A central question asks whether every positive upper Banach density set in a countable abelian group contains a sumset of k infinite sets.

The main theorem is proved with the Kronecker factor and standard ergodic and spectral theory. It extends the short proof of the k=2 case and builds the configuration one level at a time. Other questions are answered with explicit constructions and counterexamples, some relying on recent results of other authors. Most results are formalized in Lean 4 with Mathlib; certain published theorems are taken as explicit hypotheses.

Every positive upper Banach density set in a countably infinite abelian group contains B_1+...+B_k with all B_i infinite. Twenty survey questions are answered, plus a Kousek–Radić question showing the lower Banach density thresholds are 1/2 (with a shift) and 3/4 (without). Lean files contain no sorry or added axioms; several results are formalized unconditionally, others conditionally on cited theorems.

QuestionFileStatus
5.14ThmK* (14 files)conditional on four classical theorems
5.16, §5.3(a)Q516conditional on [8, Cor. 1.13]
5.10Q510complete
§3.2(a)S32acomplete
3.20Q320complete
Lean formalization status (excerpt)