Erdős Problem a Daythe open tracker
The board / number theory / #240

Erdős Problem #240

PROVEDdatabase updated 2025-08-31

The statement as posed is true, and a proof exists.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

`a P i` is the `i`-th smallest element of `Erdos675.composedOf P`, the positive integers all of whose prime factors lie in `P`, counting from index `0`. So `a P 0 = 1` (the site writes \(a_1<a_2<\cdots\)). For a nonempty set `P` of primes, `composedOf P` is infinite, `a P` is strictly increasing and the natural-number subtractions below are exact. If `P` contains no prime, then `composedOf P = {1}` and `a P i = 0` for `i ≥ 1` (the junk value of `Nat.nth`); the statements below exclude this.

Is there an infinite set of primes \(P\) such that if \(\{a_1<a_2<\cdots\}\) is the set of integers divisible only by primes in \(P\) then \(\lim a_{i+1}-a_i=\infty\)? The answer is yes, proved by Tijdeman [Ti73, Theorem 7]. The question was asked to Erdős by Wintner [Er65b, p. 218]. See also Erdős Problem 368.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 3 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/240.
Prizenone
Topicsnumber theory, primes
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/240

Attempts

submit one →
NOBODY HAS SENT US AN ATTEMPT YET

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.

← #239the board#241 →