Erdős Problem 406

Reference: erdosproblems.com/406

theorem erdos_406 : {n : ℕ | n.isPowerOfTwo ∧ Nat.digits 3 n ⊆ [0, 1]}.Finite ↔ sorry

Is it true that there are only finitely many powers of $2$ which have only the digits $0$ and $1$ when written in base $3$?

theorem erdos_406.variants.one_two : IsGreatest {n : ℕ | n.isPowerOfTwo ∧ Nat.digits 3 n ⊆ [1, 2]} (2 ^ 15)

If we only allow the digits $1$ and $2$ then $2^{15}$ seems to be the largest such power of $2$.