# A mex sequence that is not ultimately periodic

Open problem settled, formally verified in Lean 4. Vamshi Jandhyala.

> Guy's question E27: the sequence from 1,1,1,0,1,0,1,1 is unbounded, so not ultimately periodic.

Canonical: https://vamshij.com/research/mex-sequence-not-periodic
Code and Lean proofs: https://github.com/jvvk/mathematics/tree/main/mex-sequence-not-periodic
Paper (PDF): https://github.com/jvvk/mathematics/blob/main/mex-sequence-not-periodic/paper/mex.pdf

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.