HEXAGONbeta

What the ETH refutations do not give: barriers for the counting engines, with machine-checked lemmas

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

Contributed by Vaibhav Tulsyan ↗

Version 1 / Nov 06, 2026 / CC BY 4.0

Abstract

In October 2026 OpenAI and Anthropic each claimed a deterministic subexponential algorithm for counting the solutions of a kk-CNF; both counting engines sum products of local tables. For SAT itself, Majdoddin bounds the rate of Anthropic's grid recursions with product terms, and Dias and Lima bound OpenAI's clause-product scheme. However, Majdoddin notes that no barrier is known for decompositions whose terms are not products, and neither paper treats the counting problems beyond SAT. We introduce the engine barrier problem: bound from below the shared bits UU of every network of a stated class that computes a given count, and the rate of every recursion of a stated class. Our approach puts a rank on every cut of a local network, and on one contraction inside both flattenings of a term. Machine-checked in Lean are: correlated (non-product) decompositions of two rectangles, of the 3×23\times2 grid and of the full 3×33\times3 grid level have flattening-rank sums at least N2N^2, N3N^3 and N8N^8, while N9N^9 is open; the row cut of the permanent has rank (nk)\binom nk, which on paper gives U≥nlog⁡2(n/s)U\ge n\log_2(n/s) for row-local networks; algebras in which the permanent is a functional of a product have dimension at least (nn/2)\binom n{n/2}; pieces have saving ρ≥1/2\rho\ge1/2 (rank form; Anthropic's observation); and exact colouring filters for Hamiltonicity need q≥n−4q\ge n-4 colours. On paper we prove U≥(1−o(1))nlog⁡2nU\ge(1-o(1))n\log_2n for vertex-local networks for the Tutte polynomial off the integer hyperbolas, and ρ≥3/8\rho\ge3/8 for correlated decompositions of full grid levels. We cite 4545 Lean theorems, with standard axioms only. Every barrier is about a named model: in Anthropic's general model no unconditional bound on UU exists without separating P\mathrm P from P#P\mathrm P^{\#\mathrm P}, and an unconditional cap on oblivious algebraic algorithms would separate VP\mathrm{VP} from VNP\mathrm{VNP}.

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 machine-checked, what is proved on paper, what is assumed and what is checked numerically. The paper cites 45 Lean 4 theorems in 16 modules of the directory lean/EthFollowup/Barriers of the public repository https://github.com/xennygrimmato/eth-hamiltonicity (commit 946c49993b78aa163fcac3f8cb78ce351dd5dcc6; the Lean files are committed and unchanged there): RankBounds.lean, RowCut.lean, AlgebraRank.lean, PermModP.lean, SpreadLemma.lean, DecorrelatedRank.lean, DecorrelatedGrid32.lean, DecorrelatedGrid33.lean, TriangularRank.lean, ColouringBarrier.lean, ColouringBarrierGraph.lean, KstarBasic.lean, KstarLower.lean, Derand.lean, IterProdTree.lean, IterProdCutRank.lean. The 45 theorems are: Decorrelated.exists_expensive, Decorrelated.rankSum_ge, EthFollowup.Barriers.AlgebraRank.algebra_rank_half, EthFollowup.Barriers.AlgebraRank.algebra_rank_sum, EthFollowup.Barriers.Colouring.colouring_barrier, EthFollowup.Barriers.Colouring.colouring_threshold_upper, EthFollowup.Barriers.ColouringGraph.colouring_barrier_graph, EthFollowup.Barriers.Derand.support_query_eq_zero, EthFollowup.Barriers.Derand.tp_le_log_of_nonempty, EthFollowup.Barriers.Derand.tq_deleted_eq_contains, EthFollowup.Barriers.PermModP.permanent_eq_zero_of_low_rank, EthFollowup.Barriers.Rank.exists_logb_rank_ge, EthFollowup.Barriers.Rank.modelR_bound, EthFollowup.Barriers.Rank.modelR_bound_nlogn, EthFollowup.Barriers.Rank.pieces_exists_large_piece, EthFollowup.Barriers.Rank.pieces_trivial_lower_bound, EthFollowup.Barriers.Rank.rank_eq_card_of_linearIndependent, EthFollowup.Barriers.Rank.rank_le_card_of_eq_sum_mul, EthFollowup.Barriers.Rank.rank_le_two_pow_of_eq_sum_mul, EthFollowup.Barriers.Rank.rank_sum_le, EthFollowup.Barriers.Rank.sum_choose_mul_choose, EthFollowup.Barriers.Rank.sum_crossing_le_total, EthFollowup.Barriers.Rank.treeSkeleton_bound, EthFollowup.Barriers.RowCut.permanent_joinMat, EthFollowup.Barriers.RowCut.rowCut_rank, EthFollowup.Barriers.RowCut.rowCut_rank_oneHot, EthFollowup.Barriers.Spread.spread_lemma, EthFollowup.Barriers.Spread.spread_slice, EthFollowup.Barriers.Spread.spread_slice_zero, EthFollowup.Barriers.Triangular.independent_sets_rank_bound, EthFollowup.Barriers.Triangular.triangular_rank_bound_hamming, EthFollowup.IterProd.BTree.cost_ge_entropy, EthFollowup.IterProd.BTree.cost_ge_equal, EthFollowup.IterProd.rank_prodMatFixed_le, EthFollowup.IterProd.rank_prodMat_pow, Grid32.H_eq_rowTwist_T0, Grid32.exists_expensive, Grid32.rankSum_ge, Grid32.rank_colFlat_T0, Grid33.exists_expensive, Grid33.rankSum_ge, Kstar.theoremL, Kstar.theoremL_log, Lossy.rank_contr_graph, Lossy.rank_contr_le. They are written on Mathlib only and do not use the Anthropic or OpenAI developments; the axiom audit of 5 November 2026 (#print axioms for all 251 theorem declarations of the directory, all 16 modules imported in one file) shows only propext, Classical.choice and Quot.sound, and no module contains sorry or native_decide. The step from a network to a factorised matrix, the cost-to-rank step, the Tutte barrier, the full-level bound 3/8, the grouping and covering caps, the template corollaries and the meta-barrier are proved on paper only and are labelled as such. The research notes at that commit include the corrections made for this version: the repaired covering proof in research/engine2-probabilistic.md section 7, the corrected conditional cap in research/engine2-algebraic.md M6.2, and the re-run check research/scripts/engine2p_covering.py. Independent AI referee passes, an overlap comparison with Majdoddin (arXiv:2610.41622) and Dias-Lima (arXiv:2611.00517), and a citation audit were carried out. No human expert has yet reviewed the work. The barriers are statements about named models of computation; they do not depend on the claimed refutations of the Exponential Time Hypothesis being correct.

Tools used

Anthropic
Claude Fable
Lean
Lean

References

  1. Sanjeev Arora, Satish Rao, and Umesh Vazirani, Expander flows, geometric embeddings and graph partitioning , J. ACM 56 (2009), no. 2, Art. 5, doi:10.1145/1502793.1502794.DOI
  2. Per Austrin, Petteri Kaski, and Kaie Kubjas, Tensor network complexity of multilinear maps , Theory Comput. 18 (2022), Art. 16, doi:10.4086/toc.2022.v018a016.DOI
  3. Roger C. Baker, Glyn Harman, and J á nos Pintz, The difference between consecutive primes, II , Proc. London Math. Soc. (3) 83 (2001), no. 3, 532--562, doi:10.1112/plms/83.3.532.DOI
  4. Alexander I. Barvinok, Two algorithmic results for the traveling salesman problem , Math. Oper. Res. 21 (1996), no. 1, 65--84, doi:10.1287/moor.21.1.65.DOI
  5. Richard Bellman, Dynamic programming treatment of the travelling salesman problem , J. ACM 9 (1962), no. 1, 61--63.
  6. Vishwas Bhargava and Anamay Tengse, Explicit commutative ROABP s from partial derivatives , Proc. 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), LIPIcs, vol. 323, 2024, arXiv:2407.10143, pp. 10:1--10:15.arXiv
  7. Deep Bhattacharjee, Subexponential weighted counting and exact optimisation , Hexagon preprint hexagon:2610.00594v1, 29 October 2026, https://hexagonmath.org/abs/2610.00594, 2026.hexagon
  8. Andreas Bj ö rklund, Determinant sums for undirected H amiltonicity , SIAM J. Comput. 43 (2014), no. 1, 280--299, Preliminary version in FOCS 2010.
  9. — , 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.
  10. Andreas Bj ö rklund, Radu Curticapean, Thore Husfeldt, Petteri Kaski, and Kevin Pratt, Fast deterministic chromatic number under the asymptotic rank conjecture , Proc. 36th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2025, arXiv:2404.04987; doi:10.1137/1.9781611978322.91, pp. 2804--2818.arXivDOI
Show all 68 referencesShow fewer references
  1. 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.
  2. 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.
  3. Andreas Bj ö rklund, Thore Husfeldt, and Mikko Koivisto, Set partitioning via inclusion-exclusion , SIAM J. Comput. 39 (2009), no. 2, 546--563, doi:10.1137/070683933.DOI
  4. Andreas Bj ö rklund, Thore Husfeldt, and Isak Lyckberg, Computing the permanent modulo a prime power , Inform. Process. Lett. 125 (2017), 20--25, doi:10.1016/j.ipl.2017.04.015.DOI
  5. 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.
  6. 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
  7. Peter B ü rgisser, Completeness and reduction in algebraic complexity theory , Algorithms and Computation in Mathematics, vol. 7, Springer, 2000, doi:10.1007/978-3-662-04179-6.DOI
  8. Matthias Christandl, P é ter Vrana, and Jeroen Zuiddam, Asymptotic tensor rank of graph tensors: beyond matrix multiplication , Comput. Complexity 28 (2019), no. 1, 57--111, doi:10.1007/s00037-018-0172-8.DOI
  9. — , Universal points in the asymptotic spectrum of tensors , J. Amer. Math. Soc. 36 (2023), no. 1, 31--79, Preliminary version in STOC 2018; doi:10.1090/jams/996.DOI
  10. Julia Chuzhoy and Rachit Nimavat, Large minors in expanders , arXiv:1901.09349, 2019.arXiv
  11. 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 , 2026.link
  12. 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
  13. 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.
  14. 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.
  15. Carlos Stein Naves de Brito, The partition exponent in the graded pieces of the C laude 3-SAT algorithm is optimal for pieces of that shape , Hexagon preprint hexagon:2610.00692v1, 31 October 2026, https://hexagonmath.org/abs/2610.00692, 2026.hexagon
  16. 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.
  17. Marc Del é glise and Jo ë l Rivat, Computing π(x)\pi(x): the M eissel, L ehmer, L agarias, M iller, O dlyzko method , Math. Comp. 65 (1996), no. 213, 235--245, doi:10.1090/S0025-5718-96-00674-6.DOI
  18. 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.
  19. Fabio Dias and Yvens Lima, Limits and constants of O pen AI 's claimed ETH refutation , arXiv:2611.00517v1, 31 October 2026.arXiv
  20. Michael Freedman, L á szl ó Lov á sz, and Alexander Schrijver, Reflection positivity, rank connectivity, and homomorphism of graphs , J. Amer. Math. Soc. 20 (2007), no. 1, 37--51, doi:10.1090/S0894-0347-06-00529-7.DOI
  21. Carla Groenland, Isja Mannens, Jesper Nederlof, and Krisztina Szil á gyi, Tight bounds for counting colorings and connected edge sets parameterized by cutwidth , Proc. 39th International Symposium on Theoretical Aspects of Computer Science (STACS), LIPIcs, vol. 219, 2022, arXiv:2110.02730, pp. 36:1--36:20.arXiv
  22. Michael Held and Richard M. Karp, A dynamic programming approach to sequencing problems , J. Soc. Indust. Appl. Math. 10 (1962), no. 1, 196--210.
  23. Ellis Horowitz and Sartaj Sahni, Computing partitions with applications to the knapsack problem , J. ACM 21 (1974), no. 2, 277--292, doi:10.1145/321812.321823.DOI
  24. Pavel Hrube š , Avi Wigderson, and Amir Yehudayoff, Non-commutative circuits and the sum-of-squares problem , J. Amer. Math. Soc. 24 (2011), no. 3, 871--898, doi:10.1090/S0894-0347-2011-00694-2.DOI
  25. Fran ç ois Jaeger, Dirk L. Vertigan, and Dominic J. A. Welsh, On the computational complexity of the J ones and T utte polynomials , Math. Proc. Cambridge Philos. Soc. 108 (1990), no. 1, 35--53.
  26. Tam á s K ő v á ri, Vera T. S ó s, and P á l Tur á n, On a problem of K . Z arankiewicz , Colloq. Math. 3 (1954), 50--57, doi:10.4064/cm-3-1-50-57.DOI
  27. Jeffrey C. Lagarias and Andrew M. Odlyzko, Computing π(x)\pi(x): an analytic method , J. Algorithms 8 (1987), no. 2, 173--191, doi:10.1016/0196-6774(87)90037-X.DOI
  28. Radu Curticapean, Get permanent results faster by counting stars , arXiv:2611.03636, 2 November 2026.arXiv
  29. Baitian Li, Counting perfect matchings and H amiltonian cycles faster , Proc. 53rd International Colloquium on Automata, Languages, and Programming (ICALP), LIPIcs, vol. 374, 2026, arXiv:2309.15422v2, pp. 138:1--138:16.arXiv
  30. Nutan Limaye, Srikanth Srinivasan, and S é bastien Tavenas, Superpolynomial lower bounds against low-depth algebraic circuits , Proc. 62nd IEEE Symposium on Foundations of Computer Science (FOCS), 2021, doi:10.1109/FOCS52979.2021.00083, pp. 804--814.DOI
  31. Bernt Lindstr ö m, Determinants on semilattices , Proc. Amer. Math. Soc. 20 (1969), no. 1, 207--208, doi:10.1090/S0002-9939-1969-0238738-4.DOI
  32. L á szl ó Lov á sz, Large networks and graph limits , Amer. Math. Soc. Colloquium Publications, vol. 60, Amer. Math. Soc., 2012, doi:10.1090/coll/060.DOI
  33. Ruhollah Majdoddin, Lowered crossover points of A nthropic's subexponential 3-SAT algorithm , arXiv:2610.41622v1, 30 October 2026.arXiv
  34. Jesper Nederlof and Karol W ę grzycki, Improving S chroeppel and S hamir's algorithm for subset sum via orthogonal vectors , Proc. 53rd Annual ACM Symposium on Theory of Computing (STOC), 2021, doi:10.1145/3406325.3451024, pp. 1670--1683.DOI
  35. Troy Tri Nguyen, A sublinear treewidth exponent for binary constraint satisfaction , Hexagon preprint hexagon:2611.00004v1, 2 November 2026, https://hexagonmath.org/abs/2611.00004, 2026.hexagon
  36. Noam Nisan, Lower bounds for non-commutative computation , Proc. 23rd Annual ACM Symposium on Theory of Computing (STOC), 1991, doi:10.1145/103418.103462, pp. 410--418.DOI
  37. 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; we use commit 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a , 2026.link
  38. Kevin Pratt, Breaking the 2n2^n barrier for graph kk-coloring , arXiv:2607.27159, 2026.arXiv
  39. Ran Raz, Multi-linear formulas for permanent and determinant are of super-polynomial size , J. ACM 56 (2009), no. 2, Art. 8, doi:10.1145/1502793.1502797.DOI
  40. Isaac Rudich and Louis-Martin Rousseau, Deterministic factoring in time No(1){N}^{o(1)} , Hexagon preprint hexagon:2610.00600v1, 29 October 2026, https://hexagonmath.org/2610.00600v1, 2026.hexagon
  41. Herbert J. Ryser, Combinatorial mathematics , Carus Mathematical Monographs, vol. 14, Math. Assoc. America, 1963.
  42. Richard Schroeppel and Adi Shamir, A T=O(2n/2){T}={O}(2^{n/2}), S=O(2n/4){S}={O}(2^{n/4}) algorithm for certain NP -complete problems , SIAM J. Comput. 10 (1981), no. 3, 456--464, doi:10.1137/0210033.DOI
  43. Joseph Shunia, An improved subexponential bound for deterministic integer factorization , Hexagon preprint hexagon:2610.00711v1, 2 November 2026, https://hexagonmath.org/2610.00711v1, 2026.hexagon
  44. Mihail Stoian, TSP escapes the O(2nn2){O}(2^n n^2) curse , arXiv:2405.03018, 2024.arXiv
  45. Terence Tao, Ernest Croot, III, and Harald Helfgott, Deterministic methods to find primes , Math. Comp. 81 (2012), no. 278, 1233--1246, arXiv:1009.3956; doi:10.1090/S0025-5718-2011-02542-1.arXivDOI
  46. 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.
  47. Vaibhav Tulsyan, Class numbers, square roots and quadratic non-residues in time 2O(n/log⁡n)2^{O(n/\sqrt{\log n})}, assuming the new #\# SAT algorithms , Hexagon preprint hexagon:2611.00115v1, 5 November 2026, https://hexagonmath.org/abs/2611.00115, 2026.hexagon
  48. — , Counting E ulerian circuits in subexponential time, assuming the new #\# SAT algorithms , Hexagon preprint hexagon:2611.00088v1, 4 November 2026, https://hexagonmath.org/abs/2611.00088, 2026.hexagon
  49. — , Counting H amiltonian cycles in sparse graphs in subexponential time, assuming the new #\# SAT algorithms , Hexagon preprint hexagon:2610.00672v1, 31 October 2026, https://hexagonmath.org/abs/2610.00672, 2026.hexagon
  50. — , eth-hamiltonicity: L ean 4 formalisation and research notes , Public repository https://github.com/xennygrimmato/eth-hamiltonicity, commit 946c49993b78aa163fcac3f8cb78ce351dd5dcc6 ; Lean sources of this paper in lean/EthFollowup/Barriers , research notes in research/ , 2026.link
  51. — , Exact amplitudes of sparse quantum circuits in subexponential time, assuming the new #\# SAT algorithms , Hexagon preprint hexagon:2611.00090v1, 4 November 2026, https://hexagonmath.org/abs/2611.00090, 2026.hexagon
  52. — , An independent machine-checked proof of deterministic factoring in time 2O(n/log⁡n)2^{O(n/\sqrt{\log n})}, via the new #\# SAT algorithms , Preprint, November 2026; source in the directory factoring-note/ of TulsyanRepo26 , 2026.
  53. — , The parity of the prime-counting function in time xo(1)x^{o(1)} , Hexagon preprint hexagon:2611.00116v1, 5 November 2026, https://hexagonmath.org/abs/2611.00116, 2026.hexagon
  54. Leslie G. Valiant, Completeness classes in algebra , Proc. 11th Annual ACM Symposium on Theory of Computing (STOC), 1979, doi:10.1145/800135.804419, pp. 249--261.DOI
  55. — , The complexity of computing the permanent , Theoret. Comput. Sci. 8 (1979), no. 2, 189--201, doi:10.1016/0304-3975(79)90044-6.DOI
  56. Herbert S. Wilf, Hadamard determinants, M ö bius functions, and the chromatic number of a graph , Bull. Amer. Math. Soc. 74 (1968), no. 5, 960--964, doi:10.1090/S0002-9904-1968-12104-4.DOI
  57. Ryan Williams, A new algorithm for optimal 2-constraint satisfaction and its implications , Theoret. Comput. Sci. 348 (2005), no. 2--3, 357--365, doi:10.1016/j.tcs.2005.09.023.DOI
  58. Or Zamir, kk-coloring is faster than computing the chromatic number , arXiv:2607.25973v2, 2026.arXiv

Version history

  1. v1 · 24 pagesSubmitted by Vaibhav TulsyanInitial depositCurrentNov 06, 2026