1. FormalConjectures
  2. ErdosProblems
  3. «978»
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Erdős Problem 978

Reference:

    erdosproblems.com/978

    [Ho67] Hooley, C., On the power free values of polynomials. Mathematika (1967), 21--26.

    [Br11] Browning, T. D., Power-free values of polynomials. Arch. Math. (Basel) (2011), 139--150.

    [Er53] Erdős, P., Arithmetical properties of polynomials. J. London Math. Soc. (1953), 416--425.

open Polynomial Set namespace Erdos978

Let f ∈ ℤ[X] be an irreducible polynomial with positive leading coefficient. Suppose that the degree k of f is larger than 2 and is not equal to a power of 2. Then the set of n such that f n is (k - 1)-th power free is infinite, and this is proved in [Er53].

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_978.variants.sub_one {f : ℤ[X]} (hi : Irreducible f) (hd : 2 < f.natDegree) (hp : ∀ (x : ℕ), f.natDegree ≠ 2 ^ x) (hlc : 0 < f.leadingCoeff) : {n : ℕ | Powerfree (f.natDegree - 1) (f.eval (n : ℤ))}.Infinite := f:ℤ[X]hi:Irreducible fhd:2 < f.natDegreehp:∀ (x : ℕ), f.natDegree ≠ 2 ^ xhlc:0 < f.leadingCoeff⊢ {n | Powerfree (f.natDegree - 1) (eval (↑n) f)}.Infinite All goals completed! 🐙

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].

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_978.parts.i {f : ℤ[X]} (hi : Irreducible f) (hd : 2 < f.natDegree) (hp2 : ∀ (x : ℕ), f.natDegree ≠ 2 ^ x) (hlc : 0 < f.leadingCoeff) (hp : ∀ (p : ℕ), p.Prime → ∃ n : ℕ, ¬ (p : ℤ) ^ (f.natDegree - 1) ∣ f.eval (n : ℤ)) : HasPosDensity {n : ℕ | Powerfree (f.natDegree - 1) (f.eval (n : ℤ))} := f:ℤ[X]hi:Irreducible fhd:2 < f.natDegreehp2:∀ (x : ℕ), f.natDegree ≠ 2 ^ xhlc:0 < f.leadingCoeffhp:∀ (p : ℕ), Nat.Prime p → ∃ n, ¬↑p ^ (f.natDegree - 1) ∣ eval (↑n) f⊢ {n | Powerfree (f.natDegree - 1) (eval (↑n) f)}.HasPosDensity All goals completed! 🐙

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].

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_978.variants.sub_two {f : ℤ[X]} (hi : Irreducible f) (hd : 9 ≤ f.natDegree) (hp : ∀ (p : ℕ), p.Prime → ∃ n : ℕ, ¬ (p : ℤ) ^ (f.natDegree - 1) ∣ f.eval (n : ℤ)) : {n : ℕ | Powerfree (f.natDegree - 2) (f.eval (n : ℤ))}.Infinite := f:ℤ[X]hi:Irreducible fhd:9 ≤ f.natDegreehp:∀ (p : ℕ), Nat.Prime p → ∃ n, ¬↑p ^ (f.natDegree - 1) ∣ eval (↑n) f⊢ {n | Powerfree (f.natDegree - 2) (eval (↑n) f)}.Infinite All goals completed! 🐙

If $k > 3$ (and $k \neq 2^l$), then are there infinitely many $n$ for which $f(n)$ is $(k-2)$-power-free?

This was disproved by the DeepMind prover agent.

@[category research solved, AMS 11, formal_proof using formal_conjectures at "https://github.com/mo271/formal-conjectures/blob/3b5d6ac2555cd63b83d418c29ff040876be9dee0/FormalConjectures/ErdosProblems/978.lean#L64"] theorem declaration uses 'sorry'erdos_978.variants.allow_fixed_divisors : answer(False) ↔ ∀ {f : ℤ[X]}, Irreducible f → f.natDegree > 3 → (¬ ∃ l : ℕ, f.natDegree = 2 ^ l) → 0 < f.leadingCoeff → (¬ ∃ p : ℕ, p.Prime ∧ ∀ n : ℕ, (p : ℤ) ^ (f.natDegree - 1) ∣ f.eval (n : ℤ)) → {n : ℕ | Powerfree (f.natDegree - 2) (f.eval (n : ℤ))}.Infinite := ⊢ False ↔ ∀ {f : ℤ[X]}, Irreducible f → f.natDegree > 3 → (¬∃ l, f.natDegree = 2 ^ l) → 0 < f.leadingCoeff → (¬∃ p, Nat.Prime p ∧ ∀ (n : ℕ), ↑p ^ (f.natDegree - 1) ∣ eval (↑n) f) → {n | Powerfree (f.natDegree - 2) (eval (↑n) f)}.Infinite All goals completed! 🐙

If $k>3$ (and $k \neq 2^l$), and for all primes $p$ there exists $n$ such that $p^{k-2}\nmid f(n)$, then are there infinitely many $n$ for which $f(n)$ is $(k-2)$-power-free?

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_978.parts.ii : answer(sorry) ↔ ∀ {f : ℤ[X]}, Irreducible f → f.natDegree > 3 → (¬ ∃ l : ℕ, f.natDegree = 2 ^ l) → 0 < f.leadingCoeff → (∀ (p : ℕ), p.Prime → ∃ n : ℕ, ¬ (p : ℤ) ^ (f.natDegree - 2) ∣ f.eval (n : ℤ)) → {n : ℕ | Powerfree (f.natDegree - 2) (f.eval (n : ℤ))}.Infinite := ⊢ True ↔ ∀ {f : ℤ[X]}, Irreducible f → f.natDegree > 3 → (¬∃ l, f.natDegree = 2 ^ l) → 0 < f.leadingCoeff → (∀ (p : ℕ), Nat.Prime p → ∃ n, ¬↑p ^ (f.natDegree - 2) ∣ eval (↑n) f) → {n | Powerfree (f.natDegree - 2) (eval (↑n) f)}.Infinite All goals completed! 🐙

Does n ^ 4 + 2 represent infinitely many squarefree numbers?

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_978.parts.iii : answer(sorry) ↔ {n : ℕ | Squarefree (n ^ 4 + 2)}.Infinite := ⊢ True ↔ {n | Squarefree (n ^ 4 + 2)}.Infinite All goals completed! 🐙 end Erdos978