HEXAGONbeta

Exact amplitudes of sparse quantum circuits in subexponential time, assuming the new #SAT algorithms

Primarily AI-generated textHuman understanding: some partsquant-ph — Quantum Physicscs.CC — Computational Complexitycs.DS — Data Structures and Algorithms

Contributed by Vaibhav Tulsyan ↗

Version 1 / Nov 04, 2026 / CC BY 4.0

Abstract

Classical simulation lower bounds for quantum circuits have been derived from the Exponential Time Hypothesis (ETH). However, in October 2026 OpenAI and Anthropic claimed deterministic subexponential algorithms for #k-SAT, refuting ETH, and neither manuscript mentions quantum circuits. We record the corollary. Assuming three internal results of the Anthropic manuscript, one deterministic Turing machine computes the amplitude ⟨y∣C∣x⟩\langle y|C|x\rangle of a Clifford+T circuit with GG two-qubit gates in arbitrary connectivity exactly, as an element of Z[ω]/2 k\mathbb{Z}[\omega]/\sqrt2^{\,k} with ω=eiπ/4\omega=e^{i\pi/4}, in time 2O(G/log⁡G)2^{O(G/\sqrt{\log G})} whenever the input length LL satisfies log⁡L≤G0.9\log L\le G^{0.9}. The proof reads the sum over paths, one bit per wire segment, as an Anthropic-type network, with a Kronecker map for Z[ω]\mathbb{Z}[\omega] and a Galois bound. We machine-check this theorem in Lean 4 (amplitude_TM_rate', amplitude_TM_rate, amplitude_TM; axioms propext, Classical.choice, Quot.sound) on top of Anthropic's Lean development (sources at https://github.com/xennygrimmato/eth-hamiltonicity). On paper only, the method gives exact marginals and exact sampling, depth-dd circuits in 2O(dn/log⁡n)2^{O(dn/\sqrt{\log n})}, and, through OpenAI's tensor-contraction theorem, polynomial space when the number of Hadamard-type gates is O(G)O(G). Conversely, constant-depth circuits with O(n)O(n) gates encode #3-SAT with O(n)O(n) clauses, so the rate matches that of the refutations. We check the fine-grained supremacy conjectures we found against their sources; a counting form of the Calabro-Impagliazzo-Paturi width reduction refutes the gap conjecture of Morimae and Tamaki's depth-scaling paper. Dense statements (cubic phases, permanents, random circuits) survive. Nothing here concerns approximate sampling, the constants are galactic, and everything is conditional on the claimed refutations, which are 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. S. Aaronson and A. Arkhipov, The computational complexity of linear optics , Theory Comput. 9 (2013), 143--252.
  2. S. Aaronson and L. Chen, Complexity-theoretic foundations of quantum supremacy experiments , Proc. 32nd Computational Complexity Conference (CCC 2017), LIPIcs, vol. 79, 2017, pp. 22:1--22:67; theorem numbers as in arXiv:1612.05903v2.arXiv
  3. 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
  4. D. Bhattacharjee, Subexponential weighted counting and exact optimisation , Hexagon preprint hexagon:2610.00594v1, 29 October 2026, https://hexagonmath.org/abs/2610.00594.hexagon
  5. A. Bj ö rklund, Below all subsets for some permutational counting problems , Proc. 15th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2016), LIPIcs, vol. 53, 2016, pp. 17:1--17:11.
  6. S. Bravyi and D. Gosset, Improved classical simulation of quantum circuits dominated by C lifford gates , Phys. Rev. Lett. 116 (2016), no. 25, 250501.
  7. S. Bravyi, D. Gosset and R. K ö nig, Quantum advantage with shallow circuits , Science 362 (2018), no. 6412, 308--311.
  8. S. Bravyi, G. Smith and J. A. Smolin, Trading classical and quantum computational resources , Phys. Rev. X 6 (2016), no. 2, 021043.
  9. M. J. Bremner, R. Jozsa and D. J. Shepherd, Classical simulation of commuting quantum computations implies collapse of the polynomial hierarchy , Proc. R. Soc. A 467 (2011), no. 2126, 459--472.
  10. H. Buhrman, S. Patro and F. Speelman, The quantum strong exponential-time hypothesis , arXiv:1911.05686 (v2), 2019. Published as A framework of quantum strong exponential-time hypotheses , Proc. 38th STACS, LIPIcs, vol. 187, 2021, pp. 19:1--19:19.arXiv
Show all 31 referencesShow fewer references
  1. C. Calabro, R. Impagliazzo and R. Paturi, A duality between clause width and clause density for SAT , Proc. 21st Annual IEEE Conference on Computational Complexity (CCC 2006), 2006, pp. 252--260.
  2. A. M. Dalzell, A. W. Harrow, D. E. Koh and R. L. La Placa, How many qubits are needed for quantum computational supremacy? , Quantum 4 (2020), 264; arXiv:1805.05224.arXiv
  3. H. Dell, T. Husfeldt, D. Marx, N. Taslaman and M. Wahl é n, Exponential time complexity of the permanent and the T utte polynomial , ACM Trans. Algorithms 10 (2014), no. 4, Art. 21.
  4. C. Huang, M. Newman and M. Szegedy, Explicit lower bounds on strong quantum simulation , arXiv:1804.10368 (v2), 2018; published in IEEE Trans. Inform. Theory 66 (2020), no. 9, 5585--5600.arXiv
  5. C. Huang, M. Newman and M. Szegedy, Explicit lower bounds on strong simulation of quantum circuits in terms of TT -gate count , arXiv:1902.04764 (v2), 2019.arXiv
  6. R. Impagliazzo and R. Paturi, On the complexity of kk- SAT , J. Comput. System Sci. 62 (2001), no. 2, 367--375.
  7. R. Impagliazzo, R. Paturi and F. Zane, Which problems have strongly exponential complexity? , J. Comput. System Sci. 63 (2001), no. 4, 512--530.
  8. I. L. Markov and Y. Shi, Simulating quantum computation by contracting tensor networks , SIAM J. Comput. 38 (2008), no. 3, 963--981.
  9. T. Morimae and S. Tamaki, Depth-scaling fine-grained quantum supremacy based on SETH and qubit-scaling fine-grained quantum supremacy based on O rthogonal V ectors and 3-SUM , arXiv:1902.08382 (v1), 2019. Version 2 (November 2019), with R. Hayakawa as additional author, is retitled Fine-grained quantum supremacy based on O rthogonal V ectors, 3-SUM and A ll- P airs S hortest P aths .arXiv
  10. T. Morimae and S. Tamaki, Fine-grained quantum computational supremacy , arXiv:1901.01637 (v4), 2019; published in Quantum Inf. Comput. 19 (2019), no. 13&14, 1089--1115.arXiv
  11. T. Morimae and S. Tamaki, Additive-error fine-grained quantum supremacy , Quantum 4 (2020), 329; arXiv:1912.06336.arXiv
  12. M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information , Cambridge University Press, 2000.
  13. 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
  14. H. Qassim, H. Pashayan and D. Gosset, Improved upper bounds on the stabilizer rank of magic states , Quantum 5 (2021), 606; arXiv:2106.07740.arXiv
  15. H. J. Ryser, Combinatorial Mathematics , Carus Mathematical Monographs, no. 14, Mathematical Association of America, 1963.
  16. R. Schuler, An algorithm for the satisfiability problem of formulas in conjunctive normal form , J. Algorithms 54 (2005), no. 1, 40--44.
  17. B. M. Terhal and D. P. DiVincenzo, Adaptive quantum computation, constant depth quantum circuits and A rthur-- M erlin games , Quantum Inf. Comput. 4 (2004), no. 2, 134--145.
  18. C. A. Tovey, A simplified NP -complete satisfiability problem , Discrete Appl. Math. 8 (1984), no. 1, 85--89.
  19. 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
  20. 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 ca17a37 .link
  21. T. B. Wahl and S. Strelchuk, Simulating quantum circuits using efficient tensor network contraction algorithms with subexponential upper bound , Phys. Rev. Lett. 131 (2023), no. 18, 180601; arXiv:2208.01498.arXiv

Version history

  1. v1Submitted by Vaibhav TulsyanInitial depositCurrentNov 04, 2026