ErdosProblems · research solved · AMS 11
hardknown result, no worker yet
Erdős Problem 646
Theorem 646 · Erdős
Let be distinct primes. Are there infinitely many such that is divisible by an even power of each of the ?
The answer is yes, proved by Berend [Be97], who further proved that the sequence of such 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
sorryProof. sorry
Nobody has tried yet.