Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. Fix a modulus . If is a Sidon set with , then every residue class modulo contains elements of as . Lindström [Li98] proves this for itself by a combinatorial argument, and under the extra assumptions and bounds the error by ; these hypotheses are as Kolountzakis reports them (arXiv:math/9808061, p. 1), recorded on the card of Kolountzakis's strengthening, which notes that Lindström states his bound for and and that Kolountzakis removes both restrictions.
The question of Problem 154 concerns , and it follows from the statement for : in a Sidon set distinct unordered pairs have distinct sums, so the elements of in a residue class modulo are in bijection with the unordered pairs whose residues add to , and equidistribution of among the classes puts of the pairs in each class. In particular about half the elements of are even and half odd. The site's remark records the same deduction in its own words.
Depends on. No page of this wiki; the result is the paper's.
Acceptance. Refereed: B. Lindström, Well distribution of Sidon sets in
residue classes, J. Number Theory 69 (1998), no. 2, 197–200; the issue is dated
April 1998, and the page name uses the first day of that month. Reviewed: the
site's curator, T. F. Bloom, labels Problem 154 proved at erdosproblems.com on
this result and Kolountzakis's strengthening, which is the site's acceptance.
Two outside Lean files formalize the argument: the first, posted by Wouter van
Doorn to the site's thread on 2026-02-06 and pinned at its commit of 2026-03-02,
proves the statement for (sidon_density_limit) and formalizes, by
Harmonic's Aristotle, a write-up of Lindström's proof produced with ChatGPT; the
second, first posted on 2026-06-27 and pinned at its commit of 2026-08-22,
derives the sumset statement (erdos_154_sumset) from it, and
formal-conjectures links both. Neither file has been built or audited in this
corpus, so formalized is not listed and the Lean qualification of the site's
label is the site's.