Conjectures.io

Number theory

Erdős 978 - part iii

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

References

  • [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.

No one has attempted this yet.

Formal statement

Lean type

True ↔ {n | Squarefree (n ^ 4 + 2)}.Infinite

What you must prove

import FormalConjectures.ErdosProblems.«978»
import TaskSupport

namespace Bounty

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

end Bounty

Pinned source: FormalConjectures/ErdosProblems/978.lean

Source type SHA-256
sha256:80a9df89a29578a51de4dd06033d43a7d46931b1a956c65cd5f5fa6e860d631b
Task id
fc-379fc029-parts-iii-bc83630eb3-formalized-v1
Task commitment
sha256:d8af7f84cb5e964cfca33156e024215f4dbe5a04693f783959d4fdee03299775

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.