Erdős Problem #841

Let \(t_n\) be minimal such that \(\{n+1,\ldots,n+t_n\}\) contains a subset whose product with \(n\) is a square number (and let \(t_n=0\) if \(n\) is itself square). Estimate \(t_n\). A problem of Erdős, Graham, and Selfridge. For example, \(t_6=6\) since \(6\cdot 8\cdot 12=24^2\). It is trivial that \(t_n\geq P(n)\), where \(P(n)\) is the largest prime divisor of \(n\). Bui, Pratt, and Zaharescu [BPZ24] proved that the distribution of \(t_n\) continues to follow \(P(n)\), in that for any fixed \(c\in (0,1]\) \[\lim_{x\to \infty}\frac{\lvert \{ n\leq x : t_n\leq n^c\}\rvert}{x} = \lim_{x\to \infty}\frac{\lvert \{ n\leq x : P(n)\leq n^c\}\rvert}{x}.\] The statement below is that the difference of the two counting functions is \(o(x)\). This was formalized in Lean by Codex.