A prescribed Hamiltonian cycle that a book-embedding algorithm cannot produce
A 16-vertex graph carries a Hamiltonian cycle that the Alam et al. book-embedding algorithm cannot return for any choice of dual spanning tree, answering a question of Bekos, Kaufmann and Pfister in the negative.
- Lab
- Independent
- Model
- OpenAI Codex, with Claude for adversarial review
- Field
- Computer science
- Date
- 2026-08-11
- Human collaborators
- Lennart Rudolph
What was found
Bekos, Kaufmann and Pfister asked whether every prescribed Hamiltonian cycle of a Barnette graph can be recovered from the book-embedding algorithm of Alam and co-authors by choosing the dual spanning tree appropriately. The answer is no. The paper exhibits an explicit 16-vertex Barnette graph whose Hamiltonian cycle has a complementary perfect matching meeting all three edge-colour classes of the simultaneous edge and face colouring the algorithm uses. Every output of the algorithm contains each edge designated green, whatever spanning tree is chosen, and the prescribed cycle omits a green edge under every global colour labelling, so no run can produce it. Note what is not being claimed: the graph satisfies Barnette's conjecture and is Hamiltonian. What fails is the algorithm's ability to reach a particular cycle, not the conjecture.
Novelty check
The question is stated by Bekos, Kaufmann and Pfister about the earlier book-embedding algorithm of Alam and co-authors, and the paper answers it directly rather than a nearby question. Searched for a prior counterexample to prescribed-cycle recovery and none appears; the surrounding literature treats the recovery question as open. The construction is a new explicit instance, not a retrieval. Barnette's conjecture itself is untouched and remains open, so nothing in the novelty claim depends on it.
Caveats and known objections
The formalization is partial by its own account: the Lean covers the finite combinatorial core, and the topological realization of the incidence data as a sphere embedding, together with the published algorithm's Property 1, remain external inputs. So the machine checking establishes that the displayed graph has the stated combinatorial properties and that the obstruction fires, not the whole argument end to end. Not peer-reviewed. Autonomy graded ai-assisted on the paper's own disclosure, which is the authoritative one: Codex assisted with literature and novelty searches, certificate verification, code testing, proof development, and manuscript drafting and editing, while Claude was used for independent adversarial review, and the author states that neither system qualifies as an author and takes full responsibility. Worth recording a discrepancy: the Palomar record lists the authors as the human plus two model names, which the paper explicitly declines to do. The paper's statement is the one graded here.
Machine-checked elsewhere
PalomarPALOMAR-2026-08-21-000002
lennrt/palomar-formalizations at 090b3b300ba8 · checked 2026-08-21
ProvedBarnettePalomar.concrete_graph_certificateBarnettePalomar.face_coloring_certificateBarnettePalomar.property_one_excludes_prescribed_cycle
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
Covers the finite core only. The sphere embedding and the algorithm's Property 1 are external inputs, which the record states.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and AI-assisted.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and ai-assisted for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). A prescribed Hamiltonian cycle that a book-embedding algorithm cannot produce. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-08-11-prescribed-cycle-recoveryBibTeX
@misc{whataifound-independent-2026-recovery,
title = {A prescribed Hamiltonian cycle that a book-embedding algorithm cannot produce},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Formally verified. Autonomy: AI-assisted.},
url = {https://whataifound.org/finding/2026-08-11-prescribed-cycle-recovery}
}