Erdős Problem 366

Exercise 366 · Erdős

Note that $8$ is $3$ -full and $9$ is 2-full.

Formal statement · Lean 4.lean

theorem exists_three_full_then_two_full : ∃ n > 0, (3).Full n ∧ (2).Full (n + 1) := by
  sorry

Proof. sorry

Nobody has tried yet.