# An AI Research Program Tried to Crack Barnette’s Conjecture. It Failed Usefully. > Entirely AI-generated research log, August 2026. > > Generated entirely by AI agents using OpenAI Codex. Research initiated and periodically steered by Tyler Klose. Barnette remains open. The goal-directed investigation left a preserved trail of dead proof strategies, internally replayable finite witnesses against tempting proof claims, and candidate results that survived only internal AI review. ## AI authorship and research disclosure **This article was written entirely by AI.** The underlying research program was also conducted primarily by goal-directed AI agents. Tyler Klose supplied the initial objective, decided whether the work should continue, and periodically redirected or constrained it. Many intermediate questions, proof strategies, experiments, and research directions were selected autonomously by the agents. The agents generated all of this article’s prose and substantially all of the mathematical reasoning, proofs, code, computational analysis, and reviews. Tyler is not a graph theorist. He did not write or independently verify this work, does not claim it as his own mathematics, and considers it far beyond his expertise. **Barnette’s conjecture remains open.** The symbolic arguments described here have not been certified by qualified human reviewers. Computational claims apply only to their explicitly stated inputs and search boundaries. Internal AI reviews and separate verifier programs are not peer review. This is a transparent record of an AI research experiment awaiting external scrutiny—not established mathematics. ## Status - Barnette: **open** - Proof of the conjecture: **none** - Counterexample to the conjecture: **none** - Human expert review: **none** ## The honest result No proof. No counterexample. No almost. The program did not solve Barnette’s conjecture, and its latest checkpoint is not one lemma away from doing so. It explored a large tree of ideas, killed many of its own proposed arguments, narrowed one proof architecture to a precise local frontier, and kept a separate counterexample search alive. Then it paused at a named unresolved step. That sounds like failure because it is failure—if the only acceptable output is a resolution of the conjecture. Yet the private workspace also contains explicit small graphs that refute attractive proof strategies, candidate arbitrary-size constructions explaining why restricted strategies fail, a conditional route from one kind of forced edge to a genuine counterexample, and several symbolic claims that may deserve expert attention. A journal-style negative-results paper, a longer program report, and a replay supplement also exist there. None has been peer reviewed or made publicly replayable. The distinction matters. An AI can produce enough notation, tests, and internal criticism to make a body of work look institutional. That visual density is not certification. In this account, each mathematical claim is therefore treated as one of six things: published background, a deterministically checked finite object, an AI-derived symbolic result, a candidate result whose novelty is unknown, an open question, or a retired route. ## The problem in one minute **Established background.** Barnette’s conjecture says that every finite, simple, planar, bipartite, cubic, 3-connected graph contains a Hamiltonian cycle: one closed route that visits every vertex exactly once. The statement dates to 1969. It has been proved for meaningful subclasses, and [a cited exhaustive computation verified every Barnette graph through 90 vertices](https://arxiv.org/abs/2101.00943), but it remains open in general. The research program used a matching-based view. In a cubic graph every vertex has three incident edges. Remove a perfect matching—one selected edge touching every vertex—and exactly two edges remain at each vertex. Those remaining edges must form one or more disjoint cycles. Barnette can therefore be asked this way: does every Barnette graph have some perfect matching whose complement is exactly one cycle? The cube is a Barnette graph. One of its perfect matchings leaves two four-cycles; a different matching leaves one eight-cycle, so the cube is Hamiltonian. ## The seductive idea Start with any perfect matching. If its complement has several cycles, find a nearby face whose boundary alternates between matching and nonmatching edges. Flip those choices around the face. The result is another perfect matching, and sometimes two complementary cycles merge into one. The first imagined proof was a descent argument: choose a flip that reduces the cycle count, repeat, and eventually reach a Hamiltonian cycle. When immediate descent failed, the agents allowed a small temporary increase—a mathematical mountain pass—on the hope that some fixed amount of backtracking would always be enough. **Retired route.** Exact witnesses killed each version in turn: ```text 16 vertices 2 → 3 → 1 24 vertices 2 → 4 → 3 → 1 32 vertices 2 → 5 → 3 → 2 → 1 ladder family 2 → k → … → 1 ``` The 16-, 24-, and 32-vertex rows are exact finite witnesses, deterministically checked. The ladder row is an AI-derived symbolic family, unreviewed. The numbers count cycles after each face flip. The family refutes a fixed-height bound for this restricted mechanism; it does not refute Barnette or every possible local method. The checked finite witnesses are Hamiltonian, not counterexamples to Barnette; they show that this natural route can be forced to look worse before it gets better. The unreviewed ladder family claims arbitrary peak height only within its explicit local four-bridge, single-gap mechanism. It does not establish a global lower bound for face-flip proofs. ## The useful failure A hurts. B does nothing. Together they work. A 36-vertex planar cubic brace—a highly connected bipartite graph in matching theory—supplied the pivotal witness. For one selected matching, the complement had two cycles. The program enumerated 116 individual alternating contours. None reduced the count. Yet one coordinated pair did. ```text base 2 cycles contour A 3 cycles (worse) contour B 2 cycles (no improvement) A and B 1 cycle (Hamiltonian) ``` **Exact finite witness · deterministically checked.** The interaction succeeds even though neither move succeeds alone. That failure forced a better question: not “which single contour improves the state?” but “what can several contours accomplish together?” The workspace contains an unreviewed derivation claiming an exact three-pairing formula for this surgery and a planar-bipartite parity restriction on how the contours interact. **AI-derived symbolic result · unreviewed.** The formula is an arbitrary-size argument, not merely a computation on the 36-vertex graph. It may be a useful lemma. It is not a proof of Barnette, and it has not been certified by a human graph theorist. ## The proof lane The program eventually abandoned a global “energy always goes down” story. It moved to a more structural formulation called `P4-BRACE`: in the relevant cubic planar braces, can a Hamiltonian cycle be required to contain any prescribed path of three edges? The workspace treats this as an equivalent route to Barnette, drawing on [published matching theory](https://arxiv.org/abs/2202.11641), while tight three-edge cuts provide a way to compose local prescriptions. The remaining work then became a boundary-response problem. Replace a small collar of faces, record how possible Hamiltonian traversals interact with the exposed boundary, and prove that at least one replacement-compatible boundary state also works in the original graph. Finite computation can enumerate a collar’s menus; symbolic reasoning still has to justify why a local menu transfers in every host. **In plain English:** within the 15 one-collision residual collars, 13 were discharged; the remaining two contribute 28 rooted placements. A sixteenth alternating collar and other branches remain. The agents selected one root to attack. Fully discharging it would handle one placement, not the conjecture. The active reduction currently reads: ```text 101 dense-collar patterns └─ 85 discharged └─ 16 residual patterns └─ 15 with one-collision replacement candidates └─ 13 P4-admitted └─ 2 hard collars / 28 rooted placements total (14 per collar) └─ 1 selected root; current subproblem: GAP RE-SPLICE IMAGE ``` **Open question · internal AI proof bookkeeping.** A full discharge of this rooted placement would close only one of 28. `GAP RE-SPLICE IMAGE` itself would eliminate at most the short-circuit horn; `RUN` and `CYCLE` would remain. A separate alternating length-10 collar and the `LOW-SQUARE` branch also remain. None of this reduction has been externally validated. The exact next lemma is named `GAP RE-SPLICE IMAGE`. Seven “Type I” boundary caps have been reduced to a run/cycle/short-circuit trichotomy; the missing step asks which caps the re-splice can produce—in particular, whether it can produce a forbidden short-circuit arc at all. The hoped-for result is that planarity rules those arcs out. Even then, the run and cycle horns would need separate arbitrary-size separator arguments. Three “Type II” caps remain a separate two-face move problem. That is meaningful progress only at the scale of this reduction. It would be misleading to say the conjecture is down to one lemma. There are 28 hard rooted placements in this piece of the induction, plus other branches outside it. ## The disproof lane A separate lane searched for counterexamples and was deliberately kept independent from the proof story. Its cleanest symbolic result is conditional: if a Hamiltonian Barnette graph contains an edge that belongs to every Hamiltonian cycle, then a cube-based amplifier constructs an explicit non-Hamiltonian Barnette graph on `3n + 2` vertices. **AI-derived symbolic result · conditional and unreviewed.** The internal argument claims the construction preserves every required graph property. But no forced edge was found, so no counterexample was built. Three copies of the component behind a forced edge would make all three edges incident to one cubic root mandatory. A cycle can use only two of them. This is an unreviewed candidate conditional theorem; the missing input is the forced edge. The computational search also stayed negative. An internal exact enumeration found no counterexample through 46 vertices, below the published exhaustive frontier of 90. A separate adversarial order-68 search completed 28 batches covering 874 graphs, 1.88 million ordered two-edge constraint checks, and 89,148 single-edge checks without an obstruction. Those batches were complete; the order-68 census was not. The search also recovered the known 26-vertex Asano–Saito–Exoo–Harary non-Hamiltonian cubic bipartite planar graph after weakening 3-connectivity to 2-connectivity. It is a useful near-miss, not a Barnette counterexample. The attempted local repairs either preserved the separating cut or restored Hamiltonicity. ## What fell out of it The following claims survived the agents’ own attempts to falsify them. That is internal process evidence only; their proofs and novelty status still need qualified external review. - **Coordinated contour surgery — AI-derived symbolic result.** The workspace contains an unreviewed three-pairing formula claiming to explain why several alternating moves can succeed when every move fails alone. - **P4 menus and interfaces — AI-derived symbolic result.** The workspace claims prescribed traversal menus compose across tight three-edge cuts; an exact cube witness defeats a stronger three-menu version. - **Prescribed coherent decycling — candidate, novelty unknown.** A workspace proof claims an arbitrary-size theorem for cyclically 4-edge-connected cubic graphs of order divisible by four, without planarity. It needs a proof audit and literature check. - **Negative-results package — private research artifact.** A theorem-centered paper, full program report, witness atlas, and standalone replay supplement preserve which stronger statements the workspace reports as failed. The package is not yet public. - **Communication complexity — AI-derived side branch, unreviewed.** Graph face-flip response tables became finite communication matrices. The workspace reports exact bit costs and formulas for explicit promised graph families—not claims about P versus NP. ## Research interpretation The most convincing output is the graveyard. The agents repeatedly generated plausible proof narratives. The valuable behavior was not generating them; language models are exceptionally good at that. The valuable behavior was turning each narrative into a falsifiable obligation, building an exact witness when it failed, and retiring the route instead of laundering it into a confident conclusion. This experiment suggests that goal-driven AI can sustain a long mathematical falsification program. It can preserve a detailed chain of “this stronger statement is false, here is the smallest witness we found, here is exactly what remains.” It can also create an intimidating quantity of unchecked symbolic work. Those two facts belong together. More autonomous research increases the need for provenance, independent reproduction, and human expertise; it does not reduce it. Code helped where the claims were finite. It reconstructed graphs, enumerated matchings, checked Hamiltonian cycles through separate solver paths, replayed certificates, and made numerical boundaries explicit. Code did not certify arbitrary-size proofs, establish novelty, or turn internal adversarial review into peer review. So the publishable result is not “AI nearly solved Barnette.” It did not. The publishable result is a transparent record of what a sustained AI research process looked like when it was forced to keep its failures—and how some of those failures became sharper mathematics. ## Process provenance The preserved workspace spans May 23 through August 16, 2026. Goal-directed AI agents operating through OpenAI Codex could inspect local files, write and execute code, choose intermediate questions, and continue from named checkpoints. Tyler supplied the initial objective, decided whether the run should continue, and sometimes redirected or constrained it; he did not supply or verify the mathematics. Research notes, programs, finite witnesses, and a replay supplement remain in the private workspace. The research workspace was not under version control, so its chronology rests on dated checkpoint files and filesystem state rather than commit history. This public account does not yet include the full prompt history or a stable artifact bundle, so its provenance is incomplete and outside reproduction is not currently possible. ## Claim ledger - **Published background:** claims sourced to external mathematical literature. - **Exact finite witness:** an explicit object checked by deterministic code in the private workspace; only the stated object or bounded class is covered. - **AI-derived symbolic result:** an arbitrary-size argument written in the workspace; not certified by a qualified human reviewer. - **Candidate side result:** both correctness and novelty require expert review before any standalone mathematical claim. - **Open question:** unresolved. A named next step is a navigation aid, not evidence that the conjecture is close. - **Retired route:** a proposed proof mechanism refuted within its stated scope. It says nothing broader without another argument. ## External context - [Bekos, Kaufmann, and Pfister, “Approximating Barnette’s Conjecture” (2025)](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.GD.2025.6)—a recent approximation result and concise statement of the problem. - [Gorsky, Steiner, and Wiederrecht, “Matching Theory and Barnette’s Conjecture” (2022)](https://arxiv.org/abs/2202.11641)—the brace and matching-theoretic perspective used by the proof program. - [Schnieders, “Barnette Graphs with Faces up to Size 8 are Hamiltonian” (2025)](https://arxiv.org/abs/2508.03531)—a version-one preprint claiming a computationally assisted bounded-face theorem. The workspace treated the claim as provisional and did not use it as a premise. - [Brinkmann, Goedgebeur, and McKay, “The Minimality of the Georges-Kelmans Graph” (2022)](https://arxiv.org/abs/2101.00943)—including the published exhaustive verification of Barnette’s conjecture through 90 vertices. **Workspace artifacts.** The AI-generated journal manuscript, full report, code, witness files, and replay supplement are preserved locally but are not yet linked here; the supplement replays finite evidence, not arbitrary-size proofs. Before a mathematical submission, the package needs stable public provenance and expert review. --- Status as of August 29, 2026: Barnette’s conjecture is still open. This article is entirely AI-produced. Tyler Klose chose the destination and sometimes touched the wheel; the agents chose much of the route, did the mathematical work, and wrote this account of where they ended up. This is a plain-text mirror of for LLMs and agents.