---

Claim. Let $0<\epsilon<1$. There is an infinite sequence of primes $p_1<p_2<\cdots$ such that, if $n_1<n_2<\cdots$ is the sequence of all positive integers composed of these primes, then

$$n_{i+1}-n_i> n_i^{1-\epsilon}$$

for every $i$. This is Theorem 7 of R. Tijdeman, On integers with many small prime factors, Compositio Math. 26 (1973), no. 3, 319–330, display (13) on p. 326, restated in the introduction on p. 320; the paper is digested on its library card, which is the source of this claim. The site's commentary records the weaker form $a_{i+1}-a_i\gg a_i^{1-\epsilon}$. Since the gaps tend to infinity, the theorem answers the question of Problem 240 in the affirmative; the paper says it settles a conjecture of Wintner in the affirmative and proves much more, citing the conjecture from Erdős's 1965 survey, which matches the site's note that Wintner put the question to Erdős. The sequence is built by induction from $p_1=3$. Given $p_1<\cdots<p_r$ with $b-a>a^{1-\epsilon}$ for all $a<b$ composed of them, the next prime is taken from a range $[T/2,T]$, for a large $T$, outside a small exceptional set. If $a<b$ are composed of $p_1,\ldots,p_r$ and a prime $p$ of that range and satisfy $0<b-a<a^{1-\epsilon}$, a lower bound for the linear form in logarithms $\log(b/a)$, an estimate of Baker that was then unpublished and later appeared in Acta Arith. 24 (1973), 33–36, bounds the exponents of the pair: $a\le p^{C_7/2}$ for an effective constant $C_7$, so the exponent of $p$ is at most $C_7$ and each other exponent at most $C_7\log T$. For each fixed pattern of exponents the primes $p$ that admit such a pair lie in an interval of length at most $Ta^{-\epsilon}\le 4T^{1-\epsilon}$, so at most $4T^{1-\epsilon}(C_7+1)^{2r+2}(\log T)^{2r}$ primes of the range are excluded, fewer than the $3T/(10\log T)$ primes the range contains once $T$ is large, and $p_{r+1}$ is any remaining prime. The earlier theorems of the paper give, for a finite set of primes, effective gap bounds of the shape $n_{i+1}-n_i\gg n_i/(\log n_i)^C$ by the Gel'fond–Baker method.

Acceptance. The paper is a refereed journal publication, the refereed evidence; the publisher's record gives the year 1973 and no month or day, and this page is dated to the first day of that year. The site's curator, Thomas Bloom, labels the problem proved and credits the resolution to this paper, the reviewed evidence.

Formalization. The linked Lean file in Boris Alexeev's lean-proofs repository, pinned at the commit in the link, names Boris Alexeev and OpenAI Codex as its authors, states in its docstring that Tijdeman proved the result, and names Tijdeman's induction and counting argument in its lemmas, with the linear-forms input supplied through a Baker–Wüstholz interface. Its theorem erdos_240 states that there is an infinite set $P$ of primes whose positive $P$-smooth numbers, enumerated increasingly, have consecutive gaps tending to infinity; a text scan of the file found no sorry, axiom, native_decide or admit token. It carries no informal-author header and is recorded here as a formalization following Tijdeman's argument. The site's label carries no Lean qualification and lists no formal statement. This corpus has not built or kernel-checked the file, so no formalized evidence is listed.

Depends on. Nothing beyond the cited paper.