Erdős problem 406

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$ ?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

406.lean

Retained formal statement2 of 2

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

FormalConjectures/ErdosProblems/406.leanErdos406.erdos_406.variants.one_two1 lineExact file

1IsGreatest {n | n.isPowerOfTwo ∧ Nat.digits 3 n ⊆ [1, 2]} (2 ^ 15)

OpenStatement only, no proof