---
id: "2026-10-21-barnette-conjecture-openai-proof-zhentao-li-exposition"
url: "https://postcutoff.com/e/2026-10-21-barnette-conjecture-openai-proof-zhentao-li-exposition/"
as_of: "2026-10-23T13:24:00+02:00"
date: "2026-10-21"
date_precision: day
category: science
importance: 4
confidence: medium
status: [Result confirmed]
verification: "Lean proof, not yet reviewed"
sources: 3
editor: human editor
human_review: null
version: null
---

As of: 2026-10-23 13:24 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-10-21-barnette-conjecture-openai-proof-zhentao-li-exposition/

# Graph theorist Zhentao Li publishes a digested, partly re-proved version of OpenAI's proof

Full title: Barnette's 1969 Hamiltonicity conjecture: graph theorist Zhentao Li publishes a digested, partly re-proved version of OpenAI's proof

OpenAI's 6 Oct 2026 math release (family 180, manuscript "Paired states and Hamiltonian cycles in cubic bipartite planar graphs", 24 Sep) claims Barnette's conjecture, with a Lean formalization listed in its catalogue. On 21 Oct Zhentao Li posted arXiv 2610.30490, "a digested exposition of OpenAI's generated proof", which keeps the proof "essentially unchanged" but replaces the complex-valued exponential sum with two sign-reversing involutions and proves a stronger statement: G − e has a Hamiltonian cycle for every Barnette graph G and edge e. Unrefereed.

## Key facts
- Conjecture: David Barnette (1969): every cubic 3-connected bipartite planar graph has a Hamiltonian cycle; a weakening of Tait's disproved conjecture
- OpenAI claim (CONTENTS.md, family 180): 'Proves that every finite simple cubic bipartite planar 3-vertex-connected graph has a Hamiltonian cycle, resolving Barnette's conjecture. Equivalently, every three-edge path in a finite simple cubic 3-vertex-connected bipartite Pfaffian graph lies in a Hamiltonian cycle', with a Lean link
- Li's note (arXiv 2610.30490, math.CO, 21 Oct): Theorem 3, for every Barnette graph G and every edge e0, G − e0 has a Hamiltonian cycle; main case cyclically 4-edge-connected, lower connectivity in Appendix C
- Proof outline (Li): find a perfect matching of the face–black-vertex incidence graph minus N[b0] whose complement is a spanning tree; take the dual tree on white vertices; trace it into a spanning tree of G; orient towards w0 and delete e0 and the out-edges of white vertices; the remaining 2-factor is a Hamiltonian cycle. Existence of the matching is shown by counting with sign-reversing involutions
- Li: 'The proof presented here is essentially unchanged, but replaces some parts of the generated proof with combinatorial arguments. In particular, we replace the complex-valued exponential sum with direct bijections (namely, two sign-reversing involutions).'
- AI disclosure (verbatim): 'LLMs were used to read and understand the OpenAI preprint, to revise and format this note and to generate figures from their description.'

## What happened

Barnette's conjecture is one of the best-known open problems on Hamiltonian cycles in planar graphs. OpenAI's 6 Oct release listed a proof as family 180, with a Lean formalization in its catalogue.

On 21 Oct Zhentao Li posted [arXiv 2610.30490](https://arxiv.org/abs/2610.30490), a 14-page "digested exposition". He keeps OpenAI's strategy: a perfect matching in an auxiliary face–vertex graph whose complement is a spanning tree, which is traced into a spanning tree of G and turned into a Hamiltonian cycle. He replaces the generated proof's complex-valued exponential sum with two sign-reversing involutions and proves the stronger statement that G − e is Hamiltonian for every edge e. He used LLMs to read the OpenAI preprint and to format the note.

No other expert reactions were found on 23 Oct (X not searched).

## Why it matters

With Thompson's group F and Nagata's conjecture, Barnette's conjecture is now the third headline claim of OpenAI's release that an outside specialist has written out by hand. Here the claim also has a machine-checked proof from OpenAI, so the human exposition mainly adds readability and a second, partly independent argument.

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 174 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 113 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 204 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 143 days after its cutoff

## Sources

1. [arXiv 2610.30490: Zhentao Li, A note on the proof of Barnette's conjecture](https://arxiv.org/abs/2610.30490) (arxiv.org, paper)
2. [OpenAI: Paired states and Hamiltonian cycles in cubic bipartite planar graphs (24 Sep manuscript)](https://github.com/openai/math/blob/main/preprints/Paired-states-and-Hamiltonian-cycles-in-cubic-bipartite-planar-graphs-September-24-2026/paper.pdf) (github.com, paper)
3. [openai/math CONTENTS.md (family 180, Lean link)](https://github.com/openai/math/blob/main/CONTENTS.md) (github.com, code)

## Changes

- 2026-10-23 (filed): Created (PDF read)

## Related

- 2026-10-21: [Nagata's 1959 conjecture](https://postcutoff.com/e/2026-10-21-nagata-conjecture-openai-proof-tevelev-exposition/index.md)
- 2026-10-13: [Thompson's group F is nonamenable](https://postcutoff.com/e/2026-10-13-thompson-group-f-nonamenable-kim-lodha-exposition/index.md)
- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)