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
If the degree k of f is larger than or equal to 9, then the set of n such that f n is (k - 2)-th power free has infinitely many elements. This result is proved in [Br11].
∀ {f : Polynomial ℤ}, Irreducible f → 9 ≤ f.natDegree → (∀ (p : ℕ), Nat.Prime p → ∃ n, ¬↑p ^ (f.natDegree - 1) ∣ Polynomial.eval (↑n) f) → {n | Powerfree (f.natDegree - 2) (Polynomial.eval (↑n) f)}.InfiniteSolvedStatement only, no proof