Rarefied Thue-Morse Sums Via Automata Theory and Logic

Let $t(n)$ denote the number of $1$-bits in the base-$2$ representation of $n$, taken modulo $2$. We show how to prove the classic conjecture of Leo Moser, on the rarefied sum $\sum_{0\leq i<n} (-1)^{t(3i)}$, using tools from automata theory and logic. The same technique can be used to prove results about analogous sums.