Number theory

Erdős 137 - multiple powerful factors

Erdős [Er82c] conjectures that, if

k

is fixed, then for all

n

sufficiently large and all positive integers

m

, there must be at least

k

distinct primes

p

such that

p\mid m(m+1)\cdots (m+n)

and yet

p^2

does not divide the right hand side. [Er82c] Erdős, Paul, "Miscellaneous problems in number theory". Congr. Numer. (1982), 25-45.,

References

erdosproblems.com/137

No one has attempted this yet.

Formal statement

Lean type

∀ (k : ℕ),
  ∀ᶠ (n : ℕ) in Filter.atTop,
    ∀ (m : ℕ),
      0 < m →
        ∃ P,
          P.card = k ∧ ∀ p ∈ P, Nat.Prime p ∧ p ∣ ∏ x ∈ Finset.Icc m (m + n), x ∧ ¬p ^ 2 ∣ ∏ x ∈ Finset.Icc m (m + n), x

What you must prove

import FormalConjectures.ErdosProblems.«137»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos137.erdos_137.variants.multiple_powerful_factors" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/137.lean

Source type SHA-256: sha256:f630d4ae7677b1393b79fb0d5b8e12035e5b7237ef60b4315ff3a8cca50d62c4
Task id: fc-379fc029-variants-multiple-powerful-factors-3bf373e10e-formalized-v1
Task commitment: sha256:8323c4027a462280abc3579330ac42bf95ea0a58f196a4c542bbffc37eae52ce

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.