Which sequences are biologically unavoidable?
Alexander (2013) defines an infinite -gendered population as a directed graph with real birthdates and edge labels in such that there are finitely many roots, every vertex has finitely many children, every birthdate sublevel set is finite with birthdates strictly increasing along edges, the graph is infinite, and every non-root has an incoming edge of each label. A label sequence is biologically unavoidable if every such population contains a directed path spelling it. Alexander proved that every eventually periodic sequence is unavoidable, generalising König's lemma, and exhibited some avoidable sequences. What are the biologically unavoidable sequences: are there any that are not eventually periodic?
- Result
- Proved(see note)
- Status
- Resolved
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Infinite graphs; combinatorics on words
- Posed by
- Samuel A. Alexander, Biologically unavoidable sequences, Electronic Journal of Combinatorics 20(1) P31 (2013), section 6
- Year posed
- 2013
- Years open
- 13y
- Solved
- 2026-09-10
- Model
- OpenAI Codex (GPT-6 family)
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Significance
- 14 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
None: the biologically unavoidable sequences are exactly the eventually periodic ones. For every non-eventually-periodic sequence over a finite alphabet there is an explicit avoiding population; for binary sequences it has two roots, two parents per non-root with complementary labels and at most two children per vertex, and the avoidance argument is a decreasing offset along any matching path. An indicator projection and a finite copy-lift extend this to every finite alphabet, including vertex-gendered witnesses. Combined with Alexander's positive theorem, reproduced with a boundary repair, this settles the last question of his section 6. The paper also characterises which members of the binary family are universal and draws finite-observation and computability corollaries; the ordinal and universal-object questions of the same section are not claimed.
What the AI did
The model developed the central construction, proofs, Lean formalization, finite checks and exposition. A human collaborator selected Alexander's paper and directed the research.
Verification
Checked here on 22 September 2026. The construction was read in full and verified by hand; it is half a page. For a binary target s, take vertices N with birthdate v, and for v >= 2 the edges v-1 -> v labelled r(v) and v-2 -> v labelled 1-r(v), where r(2j) = s(j) and r(2j+1) = 1-s(j). A path spelling s has v_k >= 2k, so the offset v_k - 2k is a nonincreasing nonnegative integer and stabilises; from then on every step is +2 and the labels force s(k) = s(k+e+1) or s(k) = 1-s(k+e+1), so s is eventually periodic. Finite alphabets reduce to the binary case through an aperiodic indicator and a copy-lift. The Lean endpoint finite_alphabet_real_avoidance was compared with Alexander's Definition 1 clause by clause: finite roots, finite children, finite real sublevel sets, strictly increasing birthdates, infinite vertex set, a parent of each label at every non-root, at most one label per edge, and realisation from any starting vertex. Faithful. 297 lines, no sorry, no axiom, no native_decide; the author's log shows the standard axioms. There is no CI and the site did not rebuild it, so Lean-checked; a GitHub Actions build would lift it. The positive direction is Alexander's published Theorem 10.
Sources
Submitted by SilentIbis765 on