A mex sequence that never repeats
Guy's question E27: the sequence from 1,1,1,0,1,0,1,1 is unbounded, so not ultimately periodic.
Open problem settled, formally verified in Lean 4
A mex sequence that is not ultimately periodic
Start with a few nonnegative integers and keep appending the least nonnegative integer that is not a sum a_i + a_{n-i} of two terms whose indices add up to the last index n already written. In Section E27 of Unsolved Problems in Number Theory, Guy asks whether every such mex sequence is ultimately periodic.
The answer is no. The mex sequence that starts 1,1,1,0,1,0,1,1 is unbounded (Theorem 1). Its zeros sit at the positions with remainder 0 or 3 modulo 5 (Lemma 1), and each zero copies an earlier value into the set whose least missing element is taken, so from the third block of five on, each block brings a value no earlier block had (Lemma 2). Appendix A gives every term: from n = 15 on, moving 15 positions ahead adds 4 at the positions with remainder 1 or 2 modulo 5 and 0 elsewhere. The answer concerns Guy’s question with ordinary addition; the variant with addition without carries (OEIS A067018), closest to the games that motivate it, is untouched.
Preprint v1, 8 October 2026, not peer reviewed. Lemmas 1 to 3 and Theorems 1 and 2 are formally verified in Lean 4 (lean/, standard axioms only); the exposition has not yet been independently reviewed. The author used AI tools (Claude, Anthropic; Codex, OpenAI) in this work, as described in the paper’s acknowledgement, and is responsible for its content.