Erdős problem 646 · problems.science

Let $p_1,\ldots,p_k$ be distinct primes. Are there infinitely many $n$ such that $n!$ is divisible by an even power of each of the $p_i$ ?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

646.lean

Retained formal statement1 of 1

Let $p_1,\ldots,p_k$ be distinct primes. Are there infinitely many $n$ such that $n!$ is divisible by an even power of each of the $p_i$ ?

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

FormalConjectures/ErdosProblems/646.leanErdos646.erdos_6461 lineExact file

1True ↔ ∀ (S : Finset ℕ), (∀ p ∈ S, Nat.Prime p) → {n | ∀ p ∈ S, Even (padicValNat p n.factorial)}.Infinite

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science