Skip to content

Erdős problem 646

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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/646.lean

Formal Conjectures

FormalConjectures/ErdosProblems/646.leanErdos646.erdos_6461 lineExact file
True ↔ ∀ (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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:646
  • PLBY Lean proofsErdosProblems.Erdos646

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page