Formal target: Corpus.Erdos137.erdos_137.variants.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.

Exact formal statement

∀ (k : Nat),
  Filter.Eventually.{0}
    (fun n =>
      ∀ (m : Nat),
        LT.lt.{0} 0 m →
          Exists.{1} fun P =>
            And (Eq.{1} (Finset.card.{0} P) k)
              (∀ (p : Nat),
                Membership.mem.{0, 0} P p →
                  And (Nat.Prime p)
                    (And (Dvd.dvd.{0} p (Finset.prod.{0, 0} (Finset.Ioc.{0} m (HAdd.hAdd.{0, 0, 0} m n)) fun x => x))
                      (Not
                        (Dvd.dvd.{0} (HPow.hPow.{0, 0, 0} p 2)
                          (Finset.prod.{0, 0} (Finset.Ioc.{0} m (HAdd.hAdd.{0, 0, 0} m n)) fun x => x))))))
    Filter.atTop.{0}

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record