Первые цифры степени двойки.

[Yhn112]

Это не учебная задача, просто внезапно заинтересовавший меня вопрос.
Верно ли, что для любой конечной последовательности цифр существует такое $k$, что запись числа $2^k$ начинается с этой последовательности цифр? И если да, то с помощью чего это можно бы доказать (ну и если нет тоже)? У меня пока внятных идей нет.

[DeBill]

Yhn112
Это известная задача, и решать можно примерно так (будем доказывать, что начинается с 777).
Отметим на окружности единичной длины "канаву" с началом в точке $\lg 7.77$ и концом в точке $\lg 7.78$, и запустим человечка, шагающего по окружности с шагом $\lg 2$. Надо доказать, что рано или поздно он наступит в канаву....

[Simple Fairy]

Есть замечательная статья из Кванта на эту тему:
Статья - отсюда можно вывести, что степень двойки может начинаться с любых цифр.