Erdős Problem 366

Reference: erdosproblems.com/366

theorem Erdos366.erdos_366 : (∃ (n : ℕ), Nat.Full 2 n ∧ Nat.Full 3 (n + 1)) ↔ sorry

Are there any $2$-full $n$ such that $n+1$ is $3$-full?

theorem Erdos366.exists_three_full_then_two_full : ∃ (n : ℕ), Nat.Full 3 n ∧ Nat.Full 2 (n + 1)

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

theorem Erdos366.erdos_366.variant.three_two : {n : ℕ | Nat.Full 3 n ∧ Nat.Full 2 (n + 1)}.Infinite ↔ sorry

Are there infinitely many 3-full $n$ such that $n+1$ is 2-full?

theorem Erdos366.erdos_366.variant.weaker : (∃ (n : ℕ), Nat.Full 3 n ∧ Nat.Full 3 (n + 1)) ↔ sorry

Are there any consecutive pairs of $3$-full integers?