Erdős Problem 18

Theorem 18 · Erdős

$h(n!)$ is well-defined since $n!$ is practical for $n ≥ 1$ .

Formal statement · Lean 4.lean

theorem factorial_isPractical (n : ℕ) : Nat.IsPractical n.factorial := by
  sorry

Proof. sorry

Nobody has tried yet.