Paired states and Hamiltonian cycles in cubic bipartite planar graphs

Comments and discussion

• Mohamed Sabba (@ma_sabba), post on X (2026-10-08). Replying to the physics-flavoured description of the proof, points to "a deep connection between a quantum control problem involving sums of complex exponentials (composite pulse design) and Hamiltonian cycles"; a follow-up post says Astra claims this analogy for the proof's key insight and that the author can attest only to the composite-pulse side.
• jboggan, Hacker News (2026-10-07). A commenter who reports working on the conjecture since 2002 notes that the paper is problem 180, that it resembles an approach they had abandoned, and that they are reading it.
• Jake Boggan (jboggan), Hacker News (2026-10-07). The same commenter describes the proof as explicitly selecting the edges not in the Hamiltonian cycle, with a key step that "involves a complex valued exponential sum on the edges," while saying they are still digesting it.
• jboggan, Hacker News (2026-10-07). Calls the paper "a fairly short paper and quite tractable," names the disk lemma and the cancellation calculations as the main parts, and says their earlier test suite agrees with the new algorithm.
• jboggan, Hacker News (2026-10-07). Reports having an AI implement the paper's constructive procedure and run it against the commenter's existing test suite of graphs, with results that looked good.
• Jake Boggan (@jakeboggan), post on X (2026-10-07). In a thread of posts (also 1, 2, 3), the same long-time hobbyist says the complex-valued terms led an LLM to cite a "fugacity-zero loop gas in an infinitesimal magnetic field", that the key insight is "more at home in a theoretical physics paper than most graph theory papers", and that the result clears them to work on a strengthening of the conjecture.
• Jake Boggan (@jakeboggan), post on X (2026-10-09). Says the OpenAI proof "was quite different than most approaches" taken by them and others, which "typically focused on induction proofs and lifting Hamiltonian cycles".

Formalization

• OpenAI, Lean scope note for family 180 (openai/math release, 2026-10-06). States that the release's Lean formalization proves the existence of a Hamiltonian cycle for every finite simple cubic bipartite planar 3-vertex-connected graph, with challenge statement BarnetteHamiltonian.lean and proof modules under lean/OAI/Combinatorics/Hamiltonian; as of 2026-10-20 the family is not listed in lean/formalization.yaml.
• Yash Thakker, OpenAI Math Results: 8 Claims, Lean Status, Expert Views (explainx.ai, 2026-10-07, updated to 2026-10-15). Reports that the solution folder has 31 files with no sorry or axiom found by text search, that the challenge statement requires a single spanning cycle rather than a possibly disconnected 2-factor, and that lean/formalization.yaml has no entry for this family; the author did not build the code. [family-level]
• anxkhn, Add Barnette's Hamiltonian-cycle conjecture and manuscript result (google-deepmind/formal-conjectures issue #7144 and PR #7149, opened 2026-10-11, open). Proposes an independent Lean statement of the theorem with a reusable PlaneEmbedding structure, without a formal_proof link because the external proof was not run through Comparator; a commenter asked on 2026-10-12 whether a conjecture that is "already closed" should be included.

Related prior literature mentioned by others

• thomasahle, Hacker News (2026-10-07). Relays an LLM literature search suggesting the cancellation trick has precedents in fully packed O(n) loop models, where complex phases on loop orientations are used and the n→0 limit gives Hamiltonian walks. [AI-generated per source]
• jboggan, Hacker News (2026-10-07). Points to Penrose's work on counting Tait colourings of planar cubic graphs and to Kasteleyn-sign and matrix-tree analogies as possible precedents; a reply mentions Arf invariants as the mathematical counterpart of Kasteleyn signs.

Possibly relevant literature (found by the agent, not checked)

• M. T. Batchelor, J. Suzuki, C. M. Yung, Exact Results for Hamiltonian Walks from the Solution of the Fully Packed Loop Model on the Honeycomb Lattice (Phys. Rev. Lett. 73, 2646 (1994); arXiv:cond-mat/9408083). Fully packed O(n) loop model on the honeycomb (a cubic planar lattice) at n=0, the physics setting named as a precedent for the paper's signed exponential-sum cancellation.
• Peter Zograf, The enumeration of edge colorings and Hamiltonian cycles by means of symmetric tensors (arXiv:math/0403339, 2004). Extends Penrose's tensor contractions to enumerate edge colourings and Hamiltonian cycles, a possible algebraic antecedent of the weighted sum over pairs of states.
• Gunnar Brinkmann, Jan Goedgebeur, Brendan D. McKay, The Minimality of the Georges-Kelmans Graph (Math. Comp., 2022, doi:10.1090/mcom/3701; arXiv:2101.00943). Reports that Barnette's conjecture holds up to at least 90 vertices, computational evidence for Theorem 1.1 not cited in the paper's account of prior partial results.
• Jan Florek, A sufficient condition for cubic 3-connected plane bipartite graphs to be hamiltonian (arXiv:2309.09578, 2023, rev. 2024). Partial result extending Goodey's face-size condition, relevant to the paper's survey of face-structure cases (Goodey, Feder–Subi, Schnieders).

Digests and expositions

• Azmat, Barnette's Conjecture: Inside OpenAI's Surprising Proof and Why It Matters (Binary Verse AI, 2026-10-08). Non-technical walkthrough of the dual induced-tree formulation, paired states, disk identity, and cancellation-then-nonvanishing structure, noting that it gives no polynomial-time algorithm; several of its "Lean" links point to unrelated articles on the same site.