Number theory

Withdrawn

Erdős problem 978 - part ii

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)

(k-2)

-power-free?

Withdrawn 6 Oct 2026

OWNER_ACCEPTED_PUBLICATION_CLOSURE (closed on the release owner's instruction of 2026-10-06T23:17:23Z to accept the public resolution claim in OpenAI math corpus family 020, commit adc7f1241b42e322a6451854ab7e4b4c146bf78a, first public 2026-10-06T21:58:50Z. Owner-directed acceptance: no independent proof replay or certification was performed. See OWNER-ACCEPTED-CLOSURES-2026-10-06.md.)

nobody has started

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«978»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos978.erdos_978.parts.ii" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔
  ∀ {f : Polynomial ℤ},
    Irreducible f →
      f.natDegree > 3 →
        (¬∃ l, f.natDegree = 2 ^ l) →
          0 < f.leadingCoeff →
            (∀ (p : ℕ), Nat.Prime p → ∃ n, ¬↑p ^ (f.natDegree - 2) ∣ Polynomial.eval (↑n) f) →
              {n | Powerfree (f.natDegree - 2) (Polynomial.eval (↑n) f)}.Infinite

Original conjecture source: FormalConjectures/ErdosProblems/978.lean

Task id: fc-6a786f99-parts-ii-0993545a2c-formalized-v1
Task commitment: sha256:d94f66daebb9504fb9a3a391d21c855ba3e6e07f9f389bead42c394b911ca8f9

References

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.

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord

Contribution history

Individual lemmas, special cases and supporting work, shown in their original scope.

Nothing has been published against this problem yet.

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

pool/tier-1/erdos-978-parts-ii-formalized →

conjectures-contribution

Every published piece for this problem, with its Lean source and its signed record.

contributions/erdos-978-parts-ii →