Erdős problem 406 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

406.lean

Retained formal statement1 of 2

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

FormalConjectures/ErdosProblems/406.leanErdos406.erdos_4061 lineExact file

1True ↔ {n | n.isPowerOfTwo ∧ Nat.digits 3 n ⊆ [0, 1]}.Finite

OpenStatement only, no proof