No countable universal family of avoiding populations, even with exact parent counts
Alexander (2013), Section 6, asks to what extent populations avoiding a sequence can be universal among all such populations, by analogy with universal-graph theory. Interpret embedding as an injective adjacency-preserving map. In the source population class (infinite, finitely many roots, finite children, real chronological birthdates with finite earlier sublevels, and an incoming parent of each label at every nonroot), can one host, or a countable host family, contain every population avoiding a fixed avoidable word? The result also asks whether the obstruction survives exactly one incoming parent of each label. The source does not prescribe a unique embedding category; this is the explicit ordinary-embedding interpretation.
- Result
- Disproved(see note)
- Status
- Partial result
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Infinite labelled graphs; universality
- Posed by
- Samuel A. Alexander, Biologically Unavoidable Sequences (2013), Section 6, published p.12; ordinary injective-embedding interpretation.
- Year posed
- 2013
- Years open
- 13y
- Solved
- 2026-09-29
- Model
- OpenAI Codex (GPT-6 family)
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Significance
- 8 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
No. From any population avoiding s and any countable family of source-population hosts, construct an avoider with the same roots and exactly one incoming parent per label, admitting no injective map to any host with any finite global edge-stretch bound. Thus even adjacency embeddings fail. Parent selection preserves avoidance; terminal cloning preserves the selected infinite-word language exactly. The proof makes fibre sizes exceed enumerated finite host balls while preserving the actual population axioms. This strengthens the earlier complete-fibre obstruction by retaining exact parent counts. Separately, complete blow-ups preserve every corresponding least matching height, linking the obstruction to the rank question. Classical locally finite graph diagonalization is credited. Terminal vertices are permitted; fixed child caps, noninjective maps and arbitrarily unbounded stretch are outside the theorem. It answers the stated embedding interpretation, not every possible category.
What the AI did
A human collaborator selected the research directions and requested source correspondence, explanations, proof checking and submission. Codex agents developed the concrete mathematical construction or deduction, Lean proofs and exposition. Other agents in the project reviewed the arguments and source correspondence. These are internal project checks, not independent human expert review. Model-led discovery of the submitted scoped result is claimed; independent human verification and worldwide priority are not claimed.
Verification
Checked here on 30 September 2026 to the extent the artefacts allow. Lean 4.33.1 with Mathlib pinned at 0df444a3. The submitter's manifest records four new modules with 42 selected endpoints and three reused modules with 21 earlier endpoints, permitting only propext, Classical.choice and Quot.sound. The repository's Verify workflow is green on the correct repository. The site did not rebuild the development and no third party has audited the informal-to-formal correspondence, so this is Lean-checked rather than Lean-verified. The source URL was corrected: the submitted address omitted the repository's trailing dash and returned 404. Partial, as submitted: the answer is for ordinary injective embeddings, which is the interpretation the submitter states, and Alexander's Section 6 does not fix an embedding category.
Sources
- Lean proofPinned public research note, Lean source and verification receiptsExact-parent construction and obstructionEarlier generic complete-fibre obstructionExact matching-height transport
- Problem recordOriginal universal-avoider question, section 6
- OtherFrozen owner proof manifestPrimary-source and prior-work mapFull result-family publication ledgerSuccessful integrated hosted proof audit
Submitted by ZestyDingo473 on