HEXAGONbeta

Counting Eulerian circuits 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 / Nov 04, 2026 / CC BY 4.0

Abstract

Counting the Eulerian circuits of an undirected graph is #P-complete, even for planar 4-regular graphs, while for directed graphs the BEST theorem counts them in polynomial time. However, we are unaware of any exact algorithm for undirected graphs of bounded degree that runs in time 2o(m)2^{o(m)}, where mm is the number of edges. We show that such an algorithm follows from the exact counting of Hamiltonian cycles that we proved earlier on top of Anthropic's claimed #SAT algorithm. The reduction is classical: by Kotzig's description, the Eulerian circuits of GG are in bijection with the Hamiltonian cycles of the line graph of the double subdivision of GG, which has 3m3m vertices and at most (Δ+1)m(\Delta+1)m edges. We prove in Lean 4 (theoremEuler, theoremEuler_noIso, theoremEuler_rate; axioms propext, Classical.choice, Quot.sound) that for every δ>0\delta>0 and Δ\Delta a finite-alphabet Mathlib Turing machine outputs the number of Eulerian circuits of every graph of maximum degree at most Δ\Delta within ⌊C(n+2)C2δm⌋\lfloor C(n+2)^C 2^{\delta m}\rfloor steps, and within ⌊C2δm⌋\lfloor C 2^{\delta m}\rfloor steps when there is no isolated vertex; and that one machine does so for all graphs within ⌊C(n+2)C2Cmlog⁡2(Δ+2)/log⁡2(m+2)⌋\lfloor C(n+2)^C 2^{Cm\log_2(\Delta+2)/\sqrt{\log_2(m+2)}}\rfloor steps. The factor (n+2)C(n+2)^C pays for reading the n2n^2-bit adjacency matrix and cannot be dropped. The bijection is checked by brute force on twelve small graphs, for example 132 circuits for K5K_5. The formal object is Kotzig's transition-system definition; its agreement with Mathlib's Eulerian walks is not formalised. The constants are astronomical, and the proof rests on Anthropic's Lean development of its claimed refutation of the Exponential Time Hypothesis, which is under review.

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 statements of the main theorems together with the paper's own account of what is proved, what is assumed, what is checked numerically and what is not formalised. Every theorem the paper claims is 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. Computations, written proofs and informal remarks are labelled as such in the paper and are not claimed as machine-checked. 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
Lean
Lean

References

  1. Claude (Anthropic), A 2o(n)2^{o(n)} time algorithm for 3-SAT , preprint dated 26 October 2026. Paper and Lean formalisation in the repository https://github.com/anthropics/formal-math, folder eth ; we use commit 16a5ce41304fcdaea4e0be7c132e1c361dc26da5 .link
  2. N. Balaji, S. Datta and V. Ganesan, Counting E uler tours in undirected bounded treewidth graphs , 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015), LIPIcs, vol. 45, 2015, pp. 246--260; arXiv:1510.04035.arXiv
  3. T. van Aardenne-Ehrenfest and N. G. de Bruijn, Circuits and trees in oriented linear graphs , Simon Stevin 28 (1951), 203--217.
  4. G. Brightwell and P. Winkler, Counting E ulerian circuits is #\# P -complete , Proc. 7th Workshop on Algorithm Engineering and Experiments and 2nd Workshop on Analytic Algorithmics and Combinatorics (ALENEX/ANALCO 2005), SIAM, 2005, pp. 259--262; arXiv:cs/0405067.arXiv
  5. P. Chebolu, M. Cryan and R. Martin, Exact counting of E uler tours for generalized series-parallel graphs , J. Discrete Algorithms 10 (2012), 110--122.
  6. Q. Ge and D. Štefankovič, The complexity of counting E ulerian tours in 44-regular graphs , LATIN 2010: Theoretical Informatics, Lecture Notes in Comput. Sci., vol. 6034, Springer, 2010, pp. 638--649.
  7. A. Kotzig, Eulerian lines in finite 44-valent graphs and their transformations , Theory of Graphs (Proc. Colloq., Tihany, 1966), Academic Press, New York, 1968, pp. 219--230.
  8. A. Kotzig, Moves without forbidden transitions in a graph , Mat. Časopis 18 (1968), no. 1, 76--80.
  9. L. de Moura and S. 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.
  10. The mathlib Community, The L ean mathematical library , Proc. 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), 2020, pp. 367--381.
Show all 16 referencesShow fewer references
  1. OEIS Foundation, The On-Line Encyclopedia of Integer Sequences , sequence A007082, https://oeis.org/A007082.link
  2. 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.link
  3. A. Schrijver, Bounds on the number of E ulerian orientations , Combinatorica 3 (1983), no. 3--4, 375--380.
  4. C. A. B. Smith and W. T. Tutte, On unicursal paths in a network of degree 44 , Amer. Math. Monthly 48 (1941), 233--237.
  5. V. Tulsyan, Counting H amiltonian cycles in sparse graphs in subexponential time, assuming the new #\# SAT algorithms , Hexagon preprint hexagon:2610.00672v1, October 2026; source and Lean development at https://github.com/xennygrimmato/eth-hamiltonicity.hexagon
  6. V. Tulsyan, eth-hamiltonicity: L ean 4 formalisation and research notes , public repository https://github.com/xennygrimmato/eth-hamiltonicity, 2026; Lean sources as of commit 394740c .link

Version history

  1. v1 · 8 pagesSubmitted by Vaibhav TulsyanInitial depositCurrentNov 04, 2026