HEXAGONbeta

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

Primarily AI-generated textHuman understanding: some partsmath.NT — Number Theorycs.CC — Computational Complexitycs.DS — Data Structures and Algorithmscs.LO — Logic in Computer Science

Contributed by Vaibhav Tulsyan ↗

Version 1 / Nov 05, 2026 / CC BY 4.0

Abstract

Basic problems of computational number theory have proven deterministic bounds that are fixed powers of the input. The class number h(D)h(D) of an imaginary quadratic discriminant takes ∣D∣1/2+o(1)|D|^{1/2+o(1)} steps unconditionally and ∣D∣1/5+o(1)|D|^{1/5+o(1)} under the generalised Riemann hypothesis (GRH); the least quadratic non-residue modulo a prime pp takes p1/(4e)+o(1)p^{1/(4\sqrt e)+o(1)} by Burgess's 1957 bound, polynomial only under GRH; exact divisor sums ∑m≤xτ(m)\sum_{m\le x}\tau(m) take x1/3+o(1)x^{1/3+o(1)}. However, none of these bounds is of the form Xo(1)X^{o(1)}, even conditionally. We present deterministic algorithms in time 2O(n/log⁡n)2^{O(n/\sqrt{\log n})}, where nn is the input bit length, for six such problems: the number of reduced forms of discriminant −N-N, for fundamental discriminants h(−N)h(-N); the least square root of aa modulo any mm; the least quadratic non-residue modulo a prime; and ∑m≤xτ(m)\sum_{m\le x}\tau(m), ∑m≤xσ(m)\sum_{m\le x}\sigma(m) and the Gauss circle count. Our approach writes each answer as a count of solutions of equations with one or two products and evaluates it with Anthropic's counting engine through one network library: products by a two-dimensional Schönhage-Strassen network, sums by signed carry chains, inequalities by comparison chains, with O(n)O(n) shared bits. We prove the seven resulting theorems in Lean 4 (for example hForm_TM_rate; axioms propext, Classical.choice, Quot.sound): a finite-alphabet Mathlib Turing machine outputs the answer within ⌊C⋅2Cn/log⁡2(n+2)⌋\lfloor C\cdot2^{Cn/\sqrt{\log_2(n+2)}}\rfloor steps on every input. Lean proves the count of Gauss's reduced forms; its equality with the ideal class number of Q(−N)\mathbb{Q}(\sqrt{-N}) is classical and not formalised. The constants are astronomical, the machines use exponential space, and every result 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 Opus
Lean
Lean

References

  1. N. C. Ankeny, The least quadratic non residue , Ann. of Math. (2) 55 (1952), 65--72.
  2. 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
  3. E. Bach, Explicit bounds for primality testing and related problems , Math. Comp. 55 (1990), no. 191, 355--380.
  4. E. Bach and J. Shallit, Algorithmic Number Theory, Vol. 1: Efficient Algorithms , MIT Press, Cambridge, MA, 1996.
  5. D. A. Buell, Binary Quadratic Forms: Classical Theory and Modern Computations , Springer-Verlag, New York, 1989.
  6. D. A. Burgess, The distribution of quadratic residues and non-residues , Mathematika 4 (1957), 106--112.
  7. D. A. Burgess, On character sums and primitive roots , Proc. London Math. Soc. (3) 12 (1962), 179--192.
  8. M. Cipolla, Un metodo per la risoluzione della congruenza di secondo grado , Rend. Accad. Sci. Fis. Mat. Napoli (3) 9 (1903), 154--163.
  9. H. Cohen, A Course in Computational Algebraic Number Theory , Graduate Texts in Mathematics, vol. 138, Springer-Verlag, Berlin, 1993.
  10. D. A. Cox, Primes of the Form x2+ny2x^2+ny^2: Fermat, Class Field Theory, and Complex Multiplication , 2nd ed., John Wiley & Sons, Hoboken, NJ, 2013.
Show all 33 referencesShow fewer references
  1. D. Harvey, An exponent one-fifth algorithm for deterministic integer factorisation , Math. Comp. 90 (2021), no. 332, 2937--2950.
  2. J. L. Hafner and K. S. McCurley, A rigorous subexponential algorithm for computation of class groups , J. Amer. Math. Soc. 2 (1989), no. 4, 837--850.
  3. 1337isnot1337 (GitHub user) and contributors, integer-factoring: deterministic integer factoring bounds , public repository https://github.com/1337isnot1337/integer-factoring; Lean formalisation in formal-appendix/ (pull request #20, merged 30 October 2026).link
  4. Y. Lamzouri, X. Li, and K. Soundararajan, Conditional bounds for the least quadratic non-residue and related problems , Math. Comp. 84 (2015), no. 295, 2391--2412; corrigendum, Math. Comp. 86 (2017), 2551--2554.
  5. 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.
  6. H. W. Lenstra, Jr., On the calculation of regulators and class numbers of quadratic fields , Journées Arithmétiques 1980 (J. V. Armitage, ed.), London Math. Soc. Lecture Note Ser., vol. 56, Cambridge Univ. Press, 1982, pp. 123--150.
  7. H. W. Lenstra, Jr., Algorithms in algebraic number theory , Bull. Amer. Math. Soc. (N.S.) 26 (1992), no. 2, 211--244.
  8. D. Li, Computing the divisor summatory function in N9/28+o(1)N^{9/28+o(1)} , arXiv:2609.29949, September 2026.arXiv
  9. 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.
  10. A. S. Mosunov and M. J. Jacobson, Jr., Unconditional class group tabulation of imaginary quadratic fields to ∣Δ∣<240|\Delta|<2^{40} , Math. Comp. 85 (2016), no. 300, 1983--2009.
  11. 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
  12. M. O. Rabin, Digitalized signatures and public-key functions as intractable as factorization , Technical Report MIT/LCS/TR-212, MIT Laboratory for Computer Science, January 1979.
  13. I. Rudich and L.-M. Rousseau, Deterministic factoring in time No(1)N^{o(1)} , Hexagon preprint hexagon:2610.00600v1, published 29 October 2026, https://hexagonmath.org/2610.00600v1.hexagon
  14. R. J. Schoof, Quadratic fields and factorization , Computational Methods in Number Theory, Part II (H. W. Lenstra, Jr. and R. Tijdeman, eds.), Mathematical Centre Tracts, vol. 155, Mathematisch Centrum, Amsterdam, 1982, pp. 235--286.
  15. R. Schoof, Elliptic curves over finite fields and the computation of square roots mod pp , Math. Comp. 44 (1985), no. 170, 483--494.
  16. D. Shanks, Five number-theoretic algorithms , Proc. Second Manitoba Conference on Numerical Mathematics (Winnipeg, 1972), Congressus Numerantium VII, Utilitas Math., 1973, pp. 51--70.
  17. J. Shunia, An improved subexponential bound for deterministic integer factorization , Hexagon preprint hexagon:2610.00711v1, published 2 November 2026, https://hexagonmath.org/2610.00711v1.hexagon
  18. R. Sladkey, A successive approximation algorithm for computing the divisor summatory function , arXiv:1206.3369, June 2012.arXiv
  19. T. Tao, E. Croot III, and H. Helfgott, Deterministic methods to find primes , Math. Comp. 81 (2012), no. 278, 1233--1246.
  20. A. Tonelli, Bemerkung über die Auflösung quadratischer Congruenzen , Nachr. Königl. Ges. Wiss. Göttingen (1891), 344--346.
  21. 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
  22. V. Tulsyan, 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 .
  23. 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 b9ea3f1 .link

Version history

  1. v1 · 11 pagesSubmitted by Vaibhav TulsyanInitial depositCurrentNov 05, 2026