Skip to content

Erdős problem 978

Start work

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

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

978.lean

Retained formal statement4 of 6

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

This was disproved by the DeepMind prover agent.

FormalConjectures/ErdosProblems/978.leanErdos978.erdos_978.variants.allow_fixed_divisors8 linesExact file
False ↔  ∀ {f : Polynomial ℤ},    Irreducible f →      f.natDegree > 3 →        (¬∃ l, f.natDegree = 2 ^ l) →          0 < f.leadingCoeff →            (¬∃ p, Nat.Prime p ∧ ∀ (n : ℕ), ↑p ^ (f.natDegree - 1) ∣ Polynomial.eval (↑n) f) →              {n | Powerfree (f.natDegree - 2) (Polynomial.eval (↑n) f)}.Infinite
SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.