HEXAGONbeta

Counting Hamiltonian cycles in sparse graphs in subexponential time, assuming the new #SAT algorithms

Primarily AI-generated textHuman understanding: some partscs.DS — Data Structures and Algorithmsmath.CO — Combinatoricscs.CC — Computational Complexitycs.LO — Logic in Computer Science

Contributed by Vaibhav Tulsyan ↗

Version 1 / Oct 31, 2026 / CC BY 4.0

Abstract

In October 2026 two manuscripts claimed refutations of the Exponential Time Hypothesis by deterministic algorithms for #k\#k-SAT, each with a Lean formalisation of its top-level statement. Neither result applies directly to connectivity problems such as Hamiltonicity, because no linear-size CNF encoding of "this edge set is a single cycle" is known. This paper derives a corollary of the Anthropic manuscript: assuming three of its internal results (a network-to-clique reduction, an algorithm for cliques of all levels, and the existence of its "pieces"), the number of Hamiltonian cycles of a graph with nn vertices and at most DnDn edges can be computed exactly and deterministically in time O(2δn)O(2^{\delta n}) for every δ>0\delta>0, and in time 2O(max⁡(m,n)/log⁡n)2^{O(\max(m,n)/\sqrt{\log n})} for a graph with mm edges. A rank-encoded variant of the construction gives 2O(nlog⁡dˉ/log⁡n)2^{O(n\log\bar d/\sqrt{\log n})} for average degree dˉ\bar d. Deterministic decision, search and Hamiltonian-path counting follow, and so do exact sparse TSP with polynomially bounded weights, exact counting of directed Hamiltonian cycles, and ATSP. The result is not a standalone breakthrough; it stands or falls with the claimed refutation. The ingredients are known: the folklore matrix-tree identity on 22-factors, the fermionic (Berezin) matrix-tree theorem of Caracciolo, Jacobsen, Saleur, Sokal and Sportiello, and the blob partitions of Cut&Count. What is new is the observation that connectivity can be encoded with O(1)O(1) bits per edge through a Grassmann determinant whose only non-local part is a sign, and that this sign costs only O(g3)O(g^3) bits for gg blobs, so the whole construction is a network in the sense of the manuscript, whose value is n⋅#HC(G)n\cdot\#\mathrm{HC}(G). Every theorem we claim is formally verified in Lean, end to end, on top of the manuscript's own Lean development: the three counting theorems, the decision, search and path corollaries, sparse TSP, directed Hamiltonian cycles and ATSP, using only the standard axioms, with fresh kernel replays. The Lean sources are at https://github.com/xennygrimmato/eth-hamiltonicity. We also record weaker results that rest only on the machine-checked top-level theorems: the parity of #HC(G)\#\mathrm{HC}(G) for every graph in time 2O((m+n)/log⁡(m+n))2^{O((m+n)/\sqrt{\log(m+n)})} (machine-checked in Lean, with the hypotheses discharged by the labs' own Lean proofs), and one-sided randomized decision. We describe what is proved, what is checked numerically, what is formalised, what is assumed, and what the limitations are.

Provenance statement

This work was produced by Vaibhav Tulsyan in sessions with Claude Code (Anthropic). The mathematical arguments, the Lean 4 formalisation and the text were drafted by Claude under my direction; I chose the problems, directed the research, and reviewed the results at the level of [describe what you have personally read and understood, e.g. "the statements of the main theorems and the overall structure of the argument"]. All theorems claimed in the paper are machine-checked in Lean 4 on top of the Anthropic manuscript's own Lean development: the axiom audit shows only propext, Classical.choice and Quot.sound, and fresh leanchecker replays of the full dependency closure passed. The Lean sources are public at https://github.com/xennygrimmato/eth-hamiltonicity. Independent AI referee passes, exact numerical checks and a citation audit were carried out; the definitions a reader must check to trust the formal statements are listed in the paper. No human expert has yet reviewed the work. All results are conditional on the claimed refutations of the Exponential Time Hypothesis, which are under review.

Tools used

Anthropic
Claude Fable
Anthropic
Claude Opus

References

  1. Noga Alon and Zolt á n F ü redi, Covering the cube by affine hyperplanes , European J. Combin. 14 (1993), no. 2, 79--83.
  2. Eric T. Bax, Inclusion and exclusion algorithm for the H amiltonian path problem , Inform. Process. Lett. 47 (1993), no. 4, 203--207.
  3. Richard Bellman, Dynamic programming treatment of the travelling salesman problem , J. ACM 9 (1962), no. 1, 61--63.
  4. Andreas Bj ö rklund, Determinant sums for undirected H amiltonicity , SIAM J. Comput. 43 (2014), no. 1, 280--299, Preliminary version in FOCS 2010.
  5. — , Below all subsets for some permutational counting problems , Proc. 15th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT), LIPIcs, vol. 53, 2016, pp. 17:1--17:11.
  6. Andreas Bj ö rklund and Thore Husfeldt, The parity of directed H amiltonian cycles , Proc. 54th IEEE Symposium on Foundations of Computer Science (FOCS), 2013, pp. 727--735.
  7. Andreas Bj ö rklund, Thore Husfeldt, Petteri Kaski, and Mikko Koivisto, Computing the T utte polynomial in vertex-exponential time , Proc. 49th IEEE Symposium on Foundations of Computer Science (FOCS), 2008, pp. 677--686.
  8. — , The traveling salesman problem in bounded degree graphs , ACM Trans. Algorithms 8 (2012), no. 2, Art. 18, Preliminary version in ICALP 2008.
  9. Andreas Bj ö rklund and Ryan Williams, Computing permanents and counting H amiltonian cycles by listing dissimilar vectors , Proc. 46th International Colloquium on Automata, Languages, and Programming (ICALP), LIPIcs, vol. 132, 2019, pp. 25:1--25:14.
  10. Hans L. Bodlaender, Marek Cygan, Stefan Kratsch, and Jesper Nederlof, Deterministic single exponential time algorithms for connectivity problems parameterized by treewidth , Inform. and Comput. 243 (2015), 86--111, Preliminary version in ICALP 2013.
Show all 39 referencesShow fewer references
  1. Nicolas Bourbaki, Algebra I . C hapters 1--3 , Elements of Mathematics, Springer, 1989.
  2. Cornelius Brand, Holger Dell, and Marc Roth, Fine-grained dichotomies for the T utte plane and B oolean # CSP , Algorithmica 81 (2019), no. 2, 541--556, Preliminary version in IPEC 2016; arXiv:1606.06581.arXiv
  3. Chris Calabro, Russell Impagliazzo, Valentine Kabanets, and Ramamohan Paturi, The complexity of U nique kk- SAT : an isolation lemma for kk- CNF s , J. Comput. System Sci. 74 (2008), no. 3, 386--393, Preliminary version in CCC 2003.
  4. Sergio Caracciolo, Jesper Lykke Jacobsen, Hubert Saleur, Alan D. Sokal, and Andrea Sportiello, Fermionic field theory for trees and forests , Phys. Rev. Lett. 93 (2004), no. 8, 080601.
  5. Claude (Anthropic) , A 2o(n)2^{o(n)} time algorithm for 3-SAT , Preprint dated October 26, 2026. Paper and Lean formalisation in the repository https://github.com/anthropics/formal-math, folder eth , 2026.link
  6. Radu Curticapean, Block interpolation: a framework for tight exponential-time counting complexity , Inform. and Comput. 261 (2018), 265--280, Preliminary version in ICALP 2015.
  7. Radu Curticapean, Nathan Lindzey, and Jesper Nederlof, A tight lower bound for counting H amiltonian cycles via matrix rank , Proc. 29th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2018, arXiv:1709.02311, pp. 1080--1099.arXiv
  8. Marek Cygan, Fedor V. Fomin, Łukasz Kowalik, Daniel Lokshtanov, D á niel Marx, Marcin Pilipczuk, Michał Pilipczuk, and Saket Saurabh, Parameterized algorithms , Springer, 2015.
  9. Marek Cygan, Stefan Kratsch, and Jesper Nederlof, Fast H amiltonicity checking via bases of perfect matchings , J. ACM 65 (2018), no. 3, Art. 12, Preliminary version in STOC 2013.
  10. Marek Cygan, Jesper Nederlof, Marcin Pilipczuk, Michał Pilipczuk, Johan M. M. van Rooij, and Jakub Onufry Wojtaszczyk, Solving connectivity problems parameterized by treewidth in single exponential time , Proc. 52nd IEEE Symposium on Foundations of Computer Science (FOCS), 2011, Journal version in ACM Trans. Algorithms 18 (2022), no. 2, pp. 150--159.
  11. Leonardo de Moura and Sebastian Ullrich, The L ean 4 theorem prover and programming language , Automated Deduction -- CADE 28, Lecture Notes in Comput. Sci., vol. 12699, Springer, 2021, pp. 625--635.
  12. Holger Dell, Thore Husfeldt, D á niel Marx, Nina Taslaman, and Martin Wahl é n, Exponential time complexity of the permanent and the T utte polynomial , ACM Trans. Algorithms 10 (2014), no. 4, Art. 21.
  13. Holger Dell, Valentine Kabanets, Dieter van Melkebeek, and Osamu Watanabe, Is V aliant-- V azirani's isolation probability improvable? , Comput. Complexity 22 (2013), no. 2, 345--383.
  14. David Eppstein, The traveling salesman problem for cubic graphs , J. Graph Algorithms Appl. 11 (2007), no. 1, 61--81.
  15. Fedor V. Fomin and Kjartan Høie, Pathwidth of cubic graphs and exact algorithms , Inform. Process. Lett. 97 (2006), no. 5, 191--196.
  16. Michael Held and Richard M. Karp, A dynamic programming approach to sequencing problems , J. Soc. Indust. Appl. Math. 10 (1962), no. 1, 196--210.
  17. Russell Impagliazzo and Ramamohan Paturi, On the complexity of kk- SAT , J. Comput. System Sci. 62 (2001), no. 2, 367--375.
  18. Russell Impagliazzo, Ramamohan Paturi, and Francis Zane, Which problems have strongly exponential complexity? , J. Comput. System Sci. 63 (2001), no. 4, 512--530.
  19. Russell Impagliazzo and Avi Wigderson, P = BPP if E requires exponential circuits: derandomizing the XOR lemma , Proc. 29th ACM Symposium on Theory of Computing (STOC), 1997, pp. 220--229.
  20. Richard M. Karp, Dynamic programming meets the principle of inclusion and exclusion , Oper. Res. Lett. 1 (1982), no. 2, 49--51.
  21. Adam R. Klivans and Dieter van Melkebeek, Graph nonisomorphism has subexponential size proofs unless the polynomial-time hierarchy collapses , SIAM J. Comput. 31 (2002), no. 5, 1501--1526.
  22. Samuel Kohn, Allan Gottlieb, and Meryle Kohn, A generating function approach to the traveling salesman problem , Proc. 1977 ACM Annual Conference, 1977, pp. 294--300.
  23. Daniel Lokshtanov, D á niel Marx, and Saket Saurabh, Lower bounds based on the E xponential T ime H ypothesis , Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 105 (2011), 41--72.
  24. Jesper Nederlof, Bipartite TSP in O(1.9999n){O}(1.9999^n) time, assuming quadratic time matrix multiplication , Proc. 52nd ACM Symposium on Theory of Computing (STOC), 2020, pp. 40--53.
  25. OpenAI , The E xponential T ime H ypothesis is false , Preprint dated 17 October 2026, revised 25 October 2026. Paper and Lean formalisation in the repository https://github.com/openai/math, 2026.link
  26. Ran Raz and Boris Spieker, On the ``log rank''-conjecture in communication complexity , Combinatorica 15 (1995), no. 4, 567--588.
  27. The mathlib Community , The L ean mathematical library , Proc. 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), ACM, 2020, pp. 367--381.
  28. Vaibhav Tulsyan, eth-hamiltonicity: L ean 4 formalisation and research notes , Public repository https://github.com/xennygrimmato/eth-hamiltonicity, Lean sources as of commit https://github.com/xennygrimmato/eth-hamiltonicity/tree/ca17a3762bb21ddbe5942eeac9f29fa58123bb42, 2026.link
  29. Mingyu Xiao and Hiroshi Nagamochi, An exact algorithm for TSP in degree-3 graphs via circuit procedure and amortization on connectivity structure , Algorithmica 74 (2016), no. 2, 713--741.

Version history

  1. v1Submitted by Vaibhav TulsyanInitial depositCurrentOct 30, 2026