Number theory

Erdős 672

Can the product of an arithmetic progression of positive integers

n, n + d, ..., n + (k - 1)d

of length ≥ 4, with

(n, d) = 1

, be a perfect power?

References

erdosproblems.com/672

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ (k l : ℕ), l > 1 → k ≥ 4 → Erdos672.Erdos672With k l

What you must prove

import FormalConjectures.ErdosProblems.«672»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos672.erdos_672" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/672.lean

Source type SHA-256: sha256:c445617cb40577954b07647947103591146b81f79e29b214a02745fc58e09a1a
Task id: fc-379fc029-erdos672-erdos-672-7c2abd1d65-formalized-v1
Task commitment: sha256:e0d3c801ab19a12e49a75b9ba94051802978977794a52b20dcf5ffc4b89f1b65

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.