ErdosProblems · research solved · AMS 11

hardknown result, no worker yet

Erdős Problem 646

Theorem 646 · Erdős

Let p1,…,pkp_1,\ldots,p_k be distinct primes. Are there infinitely many nn such that n!n! is divisible by an even power of each of the pip_i?

The answer is yes, proved by Berend [Be97], who further proved that the sequence of such nn has bounded gaps (where the bound depends on the initial set of primes).

Formal statement · Lean 4.lean
theorem erdos_646 : answer(True) ↔
    ∀ S : Finset ℕ, (∀ p ∈ S, p.Prime) →
      {n : ℕ | ∀ p ∈ S, Even (padicValNat p (n !))}.Infinite := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗