Rich wrote,

...

My favorite effort in this direction is "2^86 is the last power of 2 without a 0 digit".

David Gale replied:

Really? In my Automatic Ant book (page 43) I speculate that statements like "there are only a finite number of 7-less powers of 2" may be undecidable, in the Godel sense that there exists no proof of the statement nor of its negation from the standard axioms.

Rich, you apparently have a proof with 7 replaced by 0. Could you elaborate?

I'm just guessing, and surely Rich will fill us in soon. But for any k, the last k digits of 2^n are eventually periodic. So if you find a k where every member of the attrating cycle of "n -> 2n mod 10^k" contains a 0, you're done. I'd have to think more about whether we expect such a scheme to succeed or fail in general. As k increases, you have more digits to work with, but also probably more terms in the cycle, and if someone else wants to work out how the probabilities balance against each other, I'm as happy to read it as to do it myself... --Michael Kleber -- It is very dark and after 2000. If you continue you are likely to be eaten by a bleen.