---

Claim. Corollary 1 of Product of integers in an interval, modulo squares (Electron. J. Combin. 8 (2001), #R5, p. 4) proves two bounds for the $t_n$ of Problem 841. If $P(n)>\sqrt{2n}+1$, where $P(n)$ is the largest prime factor of $n$, then $t_n=P(n)$. Otherwise $t_n\le3\sqrt{n/2}+1$. Write $n=ap$ with $p=P(n)$. In the first case, the bound $t_n\le p$ comes from five explicit integers in $(n,n+p]$, the largest being $n+p$, whose product with $n$ is a square. The second case follows from the paper's Theorem 2. The site credits the result to Selfridge.

Covers. The exact value of $t_n$ for every $n$ with $P(n)>\sqrt{2n}+1$, and $t_n\ll\sqrt n$ for every other $n$. It does not give the distribution of $t_n$.

The companion lower bound $t_n\ge p(n)$ holds when $p(n)$ is the largest prime dividing $n$ to an odd power, as the paper's preceding paragraph defines it. It fails for the largest prime divisor, which is how the corollary names $p(n)$: $t_{242}=8<11$.

Acceptance. The paper appeared in the Electronic Journal of Combinatorics, a refereed journal, which is the refereed evidence.

Formalization. The OpenAI Codex development linked on the Bui-Pratt-Zaharescu page states that it proves the exact large-prime estimate of Granville and Selfridge. Its final theorem has $t_n=P(n)$ for $P(n)>\sqrt{2n}+1$ and the weaker $t_n\le40\sqrt n$ otherwise. This corpus has not built it, so it is not formalized evidence.