An AI research program tried to crack Barnette’s conjecture. It failed usefully.

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.

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, 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?

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.

The last distinction is easy to lose. 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.

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.

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 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, 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 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.

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.

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.

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.

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.

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.

• Bekos, Kaufmann, and Pfister, “Approximating Barnette’s Conjecture” (2025)—a recent approximation result and concise statement of the problem.
• Gorsky, Steiner, and Wiederrecht, “Matching Theory and Barnette’s Conjecture” (2022)—the brace and matching-theoretic perspective used by the proof program.
• Schnieders, “Barnette Graphs with Faces up to Size 8 are Hamiltonian” (2025)—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)—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.