Erdős problem 978
Let f ∈ ℤ[X] be an irreducible polynomial with positive leading coefficient. Suppose that the degree k of f is larger than 2, is not equal to a power of 2, and f n has no fixed (k - 1)-th power divisors other than 1. Then the set of n such that f n is (k - 1)-th power free has positive density, and this is proved in [Ho67].
Sources
FormalConjectures/ErdosProblems/
978.lean
Retained formal statement
Does n ^ 4 + 2 represent infinitely many squarefree numbers?
True ↔ {n | Squarefree (n ^ 4 + 2)}.InfiniteOpenStatement only, no proof