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