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
The primes show that is possible.
(fun n => ↑n / Real.log ↑n) =O[Filter.atTop] fun n => ↑(Nat.findGreatest (Erdos888.p n) n)SolvedStatement only, no proof