Erdős problem 888
What is the size of the largest such that if are such that is a square then ?
Sources
FormalConjectures/ErdosProblems/
888.lean
Retained formal statement
Erdős claims that Sárközy proved that (a proof of this bound is provided by Tao in the comments).
(fun n => ↑(Nat.findGreatest (Erdos888.p n) n)) =o[Filter.atTop] Nat.castSolvedStatement only, no proof