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
Cambie and Weisenberg have noted in the comments that the set of semiprimes also works, showing is achievable.
(fun n => ↑n * Real.log (Real.log ↑n) / Real.log ↑n) =O[Filter.atTop] fun n => ↑(Nat.findGreatest (Erdos888.p n) n)SolvedStatement only, no proof