---

Claim. For every $\epsilon>0$ and $k\ge2$ and every sufficiently large $N$ there are $k$ consecutive integers in $[N/2,N]$ each member $m$ of which is $m^\epsilon$-smooth, so in particular $N^\epsilon$-smooth. This is the second strengthening of the question of Problem 369 that the site proposes, for all large $N$ rather than for infinitely many, and it implies the question as written; the formal-conjectures statement erdos_369 encodes the weaker $N^\epsilon$ reading. The construction follows Balog and Wooley 1998 with different parameters: choose pairwise coprime squarefree $r_j$ with $\varphi(r_j)/r_j<\epsilon/2$, build $a=C\,2^{Lu}3^{Lv}$ by the Chinese remainder theorem so that $a/j=b_j^{r_j}$ for $1\le j\le k-1$, so that the cyclotomic factorization of $b_j^{r_j}-1$ bounds every prime factor of $a-j$ by a constant times $N^{\epsilon/2}$, and use the irrationality of $\log2/\log3$ to place $a$ in $(3N/4,N)$ for every large $N$. The author posted the argument with a written sketch on the site's forum on 2026-03-26 under the name YueerYang; the formal files name the author Sky Yang. The claimant reports in that post that GPT (version not stated) translated the claimant's idea and wrote it in rigorous form and helped them search the literature, and in a later post the same day that they had GPT 5.4 and Claude Opus 4.6 check the argument.

Acceptance. On the forum on 2026-03-27 the site's curator, Thomas F. Bloom, wrote first that they saw no immediate problem and that the argument is close to that of Balog and Wooley with a different choice of parameters, and later the same day that the argument settles the most natural interpretation of the problem in the affirmative, reporting that Wooley confirmed that the Balog–Wooley paper addressed a slightly different problem; the site labels the problem proved (reviewed). Wouter van Doorn formalized the argument in Lean 4 with the Aristotle system and posted the file on 2026-03-27; the file declares itself a formalization of Yang's proof, so it is a link on this page rather than a claim of its own. The copy in the lean-proofs repository is what the formal-conjectures project links as the formal proof of its statement erdos_369, a run of $k$ consecutive integers in $[n/2,n]$ with every prime factor at most $n^\epsilon$, for all large $n$; van Doorn's theorem proves the member-wise bound, which implies it. The statement file is linked above as a record, since it holds no proof. This corpus has not built either file or audited its statement, so formalized is not listed, and there is no refereed publication. A stronger result, a run in $[n-n^c,n]$ for some $c<1$ and all large $n$, follows from a 2020 theorem of Bober, Fretwell, Martin and Wooley and has its own page, Bober, Fretwell, Martin and Wooley 2020.

Depends on. Nothing in this wiki.