Decidability of the Powers of Two Problem
Christoph Haase, Sep 22 2022

Dear Neil,

I saw with interest the Numberphile video featuring the Powers of Two problem.

Paraphrasing from the video (and apologies for any misrepresentation),
you say that for any n, there is no known bound on the integers to
consider in order to compute a(n). It actually turns out that there is
one for any fixed n.

The reason for this is that the problem can be rephrased as a problem in
the existential theory of Büchi arithmetic. This is the decidable
first-order theory of the structure <Z,0,1,+,V_p>, for a fixed p>1,
where V_p(x,y) holds iff x is the largest power of p dividing y without
remainder. Asserting that x is a power of p can then just be expressed
as V_p(x,x). It should then be obvious that the problem of deciding
whether a(n)>=k reduces to deciding an existential sentence in this
theory (I'm happy to give details if you wish).

This theory is decidable using methods from automata theory, there is
also tool support available, e.g., Jeffrey Shallit's "Walnut" tool:

https://cs.uwaterloo.ca/~shallit/walnut.html

I don't have the time to consider n=10, but I'm cautiously optimistic
that this should still be feasible for Walnut.

 From the decidability proof, you also get a bound on the bit-length of
the integers to consider, which is roughly 2^O(F), where F is the length
of the formula encoding the problem (which should be, if I'm not
mistaken, quadratic in n for this problem), see e.g. Eq. (1) in:

Guépin, F., Haase, C. and Worrell, J., 2019, June. On the existential
theories of Büchi arithmetic and linear p-adic fields. In 34th Annual
ACM/IEEE Symposium on Logic in Computer Science (LICS) (pp. 1-10). IEEE.
URL:
http://www.cs.ox.ac.uk/people/christoph.haase/home/publication/ghw-19/ghw-19.pdf

One can even parametrize the problem by the base, and ask for the value
of a(n) for powers of 3,4,5,.. You may find it interesting that all
those bases for which a(n)>=k for a fixed k form an ultimately periodic
set (i.e. a generalized arithmetic progression) as we show here:

Haase, C. and Mansutti, A., 2021, On Deciding Linear Arithmetic
Constraints Over p-adic Integers for All Primes. In Mathematical
Foundations of Computer Science (MFCS) (pp. 55:1-55:20). LiPICS.
URL:
http://www.cs.ox.ac.uk/people/christoph.haase/home/publication/hm-21/hm-21.pdf

I hope this is of use to you. I'm happy to discuss this further should
you have any questions.

Best wishes,
   Christoph