The board / number theory / #26
Erdős Problem #26
DISPROVED LEANdatabase updated 2025-12-28
The statement as posed is false. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
A sequence of naturals \((a_i)\) is _thick_ if their sum of reciprocals diverges: \[ \sum_i \frac{1}{a_i} = \infty \]
The set of multiples of a sequence \((a_i)\) is \(\{na_i | n \in \mathbb{N}, i\}\).
A sequence of naturals \((a_i)\) is _Behrend_ if almost all integers are a multiple of some \(a_i\). In other words, if the set of multiples has natural density \(1\).
Let \(A\subset\mathbb{N}\) be infinite such that \(\sum_{a \in A} \frac{1}{a} = \infty\). Must there exist some \(k\geq 1\) such that almost all integers have a divisor of the form \(a+k\) for some \(a\in A\)? This was formalized in Lean by Alexeev using Aristotle.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/26.Prizenone
Topicsnumber theory, divisors
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/26
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.