---

Claim. Let $t_n$ be the least $t$ such that some subset of $\{n+1,\ldots,n+t\}$ has product with $n$ a perfect square ($t_n=0$ for square $n$), and let $P(n)$ be the largest prime factor of $n$. Bui, Pratt and Zaharescu prove (Theorem 1.1) that for every fixed $c\in(0,1]$ the proportion of $n\le x$ with $t_n\le n^c$ tends to the same limit as the proportion with $P(n)\le n^c$, namely the Dickman–de Bruijn value $\rho(1/c)$; so for every fixed $c>0$ a positive proportion of integers have $t_n\le n^c$. They also prove (Theorem 1.2) that at least $x^{1-o(1)}$ integers $n\le x$ have $t_n\le\exp(O(\sqrt{\log n\log\log n}))$, and (Theorem 1.4) that every sufficiently large non-square $n$ has

$$t_n\gg(\log\log n)^{6/5}(\log\log\log n)^{-1/5},$$

with an effective constant. These results answer the estimate that Problem 841 asks for, in the reading the site gives it, and refute Granville's expectation that $t_n>n^c$ should hold for some fixed $c>0$. The paper's abstract and introduction are written in these terms; the library card is Bui, Pratt and Zaharescu 2024.

Earlier results. If a prime $p$ divides $n$ to an odd power, every subset of $\{n+1,\ldots,n+t\}$ whose product with $n$ is a square must contain a multiple $n+j$ of $p$, so $p\mid j$ and $t_n\ge p$; in particular $t_n\ge P(n)$ whenever $P(n)$ divides $n$ exactly once, for example whenever $P(n)>\sqrt n$. Without that condition the bound fails: for $n=242=2\cdot11^2$ the product $242\cdot245\cdot250=3850^2$ gives $t_{242}=8<11$ (the site's commentary states $t_n\ge P(n)$ for every $n$, which is too strong). Granville and Selfridge (Electron. J. Combin. 8 (2001), Corollary 1, cited by the paper) proved that $t_n=P(n)$ whenever $P(n)>\sqrt{2n}+1$, and Guy's B30 (Guy 2004, pp. 128–129) reports Selfridge's bound $t_n\le\max(P(n),3\sqrt n)$. The site's commentary records that Erdős first asked whether the integers with $t_n\ge n^{1-o(1)}$ have density zero. These are the background to the claim, not part of it.

Acceptance. The site's curator, Thomas Bloom, labels the problem solved and credits the result to Bui, Pratt and Zaharescu in the page's commentary, which is the reviewed evidence. The paper appeared in Math. Proc. Cambridge Philos. Soc. 176 (2024), no. 2, 309–323, which is the refereed evidence.

Formalization. Boris Alexeev's lean-proofs repository holds, at the pinned commit linked above, a Lean development of the paper's results whose header names OpenAI Codex as its author (Lean 4.33.0, Mathlib v4.33.0): its Core.lean states that it proves the Granville–Selfridge large-prime estimate, the finite square-subset and smooth-interval lemmas of Bui, Pratt and Zaharescu, and their moving-threshold distributional comparison, and its LowerBound.lean closes with a single theorem combining $t_n=P(n)$ for $P(n)>\sqrt{2n}+1$, $t_n\le40\sqrt n$ otherwise, the distribution theorem in the form that the two counting functions differ by $o(x)$, the $x^{1-o(1)}$ family of small values with explicit constant $20$, and the lower bound. The formal-conjectures statement file for the problem, added 2026-09-21, tags its erdos_841 declaration and four variants as research solved, points each at this development and says the formalization is by Codex; the community database (teorth/erdosproblems) records the problem as formalized, while the site's label stays SOLVED without a Lean marker. Since the development names the paper's results as what it formalizes, it is recorded as the claimants' formalization link. This corpus has not built or audited it, so it is not formalized evidence.

Scope. The statement asks for an estimate of $t_n$, an open-ended request. The claim is recorded as settling it because the site reads the distribution theorem, the bound $t_n\le\exp(O(\sqrt{\log n\log\log n}))$ for at least $x^{1-o(1)}$ integers $n\le x$, and the lower bound as the answer; the order of $t_n$ for an individual non-square $n$ between the two bounds is not determined by the paper.