Graph theorist Zhentao Li publishes a digested, partly re-proved version of OpenAI’s proof
Result confirmed
Importance: major (4 of 5)The takeaway
OpenAI’s 6 Oct release claimed Barnette’s conjecture (every cubic 3-connected bipartite planar graph is Hamiltonian), with a Lean proof. A combinatorialist has now written the argument out by hand, replacing its exponential-sum step with explicit sign-reversing involutions.
Status
- Claim
Result confirmed
- Our reporting
- Medium confidence
- Verification
- Lean proof, not yet reviewed
- Importance
- Major (4 of 5)
- Last verified
- 23 October 2026
Your AI and this story
- GPT-6 Astra174 days after its cutoff
- Claude Opus 5.5113 days after its cutoff
- Gemini 4 Argon204 days after its cutoff
- Grok 4.7143 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 113 days before it.
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.304901, 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.
Sources
3 sources from 2 sites. Numbers match the chips in the text.
3 sources: 3 primary
Primary
Changes
- Filed (PDF read)