Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 1112
claims/: The 2 claim pages of Problem 1112, one per claimant's result; the problem's standing derives from them.
Statement. Let and . Does there exist an integer such that if is a lacunary sequence of positive integers with then there exists a sequence of positive integers such that
for all and , where is the -fold sumset?
Statement (precise). For which integers and does there exist an integer such that, whenever is a sequence of positive integers with for all , there is a sequence of positive integers with for all and , where is the -fold sumset? In the site's notation: for which does exist?
Notes. The site's wording begins "Let and .
Does there exist an integer ...", which can be read two ways: as one
yes-or-no assertion quantified over every triple, or as a separate question for
each triple. Under the first reading the answer has been no since 1997:
Bollobás, Hegyvári and Jin [BHJ97] proved that for and gaps in
no ratio exists. The site's curator reads it the second way. The curator's
commentary defines as the least ratio that works for a given
triple, records that does not exist, and says that "the more general
question of existence of for remains open"; the problem
was posted as open with [BHJ97] already in its commentary, which is only
consistent with the per-triple reading. The Statement (precise) above states
that reading. The curator also notes that the question is the curator's own
generous reading of a vague remark of Erdős and Graham [ErGr80, p. 18], so the
Statement is the site's question rather than Erdős's words. Under the precise
Statement Johan Land's dichotomy (a ratio exists exactly when ,
with the ratio in the built development and in the September
2026 revision) settles every triple, so the problem is solved; [BHJ97] settles
the triple and is a partial claim. The site keeps the label OPEN
(LEAN): on 13 July 2026 the curator confirmed on the thread that erdos_1112 is
a correct formalization and compiles without sorry, and wrote of not yet
having tried to understand the proof; the acceptance here rests instead on the
port of Land's development that this corpus built and audited.
Status. OPEN (LEAN), the site's label (page last edited 28 December 2025).
The site's proof-claims tab carries a full proof claim by Johan Land (announced
on the discussion thread on 2026-07-06, submitted as a proof claim on
2026-07-17, with the AI systems used named on the claim page) that a ratio
exists exactly when , with a write-up and a Lean 4 development, the
development the Formalization field links as the solution; the site's curator
confirmed on the thread on 2026-07-13 that the main Lean theorem of the original
development formalizes the question and compiles without sorry, a development
replaced on 2026-09-13 by the shortened argument described on the claim page.
The claim is accepted on
its claim page
on a port of the original development that this corpus built and audited (see
Formalization). The curator has verified only the formalization, not the proof,
so this page's solved standing departs from the site's label. Bollobás, Hegyvári
and Jin [BHJ97] settled one instance, proving that for and gaps in
no ratio exists, in the stronger varying-ratio form, an accepted partial claim
on
its claim page.
Tang and Yang [TaYa21], credited by the commentary with further technical
nonexistence results, have no claim page: the paper is not held and its journal
copy is behind a subscription, and its zbMATH review (Zbl 1499.11038) says only
that the authors give growth conditions on under which has a subsequence
inside , without naming the instances they settle, so the paper may settle
further instances.
Source. erdosproblems.com/1112, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #1112, https://www.erdosproblems.com/1112.
References.
- [BHJ97] Bollobás, Béla and Hegyvári, Norbert and Jin, Guoping, On a problem of Erdős and Graham. Discrete Math. (1997), 253-257.
- [Ch00] Chen, Yong-Gao, On sums and intersects of sequences. Discrete Math. (2000), 351-354.
- [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980); p. 18.
- [TaYa21] Tang, Min and Yang, Quan-Hui, On a problem of Erdős and Graham. Publ. Math. Debrecen (2021), 485-493.
Formalization. Solution at
https://github.com/beetree/math_erdos_1112.
This corpus built the port of Land's original development in Boris Alexeev's
lean-proofs repository,
src/latest/ErdosProblems/Erdos1112.lean
at a pinned commit of 2026-09-15, checked the axioms of its four final theorems
and found their fingerprints identical to the repository's comparator challenge,
as the claim page records; the port proves the dichotomy with the ratio
, and the September revision in Land's repository, with the ratio
, is not built.
Current assessment
Solved by Land's dichotomy, accepted on a Lean port built here; one instance
settled in a refereed paper. Read triple by triple, as the Statement
(precise) states (see Notes), the question asks for which with
and a ratio exists. Theorem 3 of [BHJ97] settles ,
in the negative, in the varying-ratio form. It is an accepted
partial claim on
its claim page.
Johan Land's full claim, on
its claim page,
answers every triple: a ratio exists exactly when . It is accepted
on formalized evidence: this corpus built the port of Land's original
development in Boris Alexeev's lean-proofs repository at a pinned commit, found
the axioms of its four final theorems to be the three standard ones, matched
their fingerprints to the repository's comparator challenge and audited their
statements clause by clause against the Statement above, as the claim page
records. The built development proves the ratio above the threshold;
the ratio of the September revision of the paper is not built. On 13
July 2026 the curator confirmed that the main Lean statement of the original
development formalizes the question and compiles without sorry, and wrote of
not yet having tried to understand the proof. The site's label stays OPEN
(LEAN), so no reviewed evidence is listed, and there is no refereed write-up.
Tang and Yang [TaYa21] give further nonexistence results whose instances the
available review does not name (see Status). The two-summand results the site
records concern , outside the problem's range: the Erdős–Graham
construction, Theorem 1 of [BHJ97] and Chen's [Ch00]. No release item or lead
names the problem.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.