HEXAGONbeta

The parity of the prime-counting function in time xo(1)x^{o(1)}

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

Computing the prime-counting function π(x)\pi(x) exactly takes x1/2+o(1)x^{1/2+o(1)} steps by the analytic method of Lagarias and Odlyzko, and to our knowledge its parity is known faster only on short intervals: Tao, Croot and Helfgott decide whether an interval of length at most x1/2+cx^{1/2+c} near xx contains an odd number of primes in time x1/2−c+o(1)x^{1/2-c+o(1)}. However, their identity needs the Mobius function μ(d)\mu(d) for all d≤xd\le\sqrt x, and we know of no bound of the form xo(1)x^{o(1)} for the parity, even conditionally. We present deterministic algorithms that output π(x) mod 2\pi(x) \bmod 2 and the parity of the number of primes in any interval [A,B][A,B] in time 2O(n/log⁡n)=xo(1)2^{O(n/\sqrt{\log n})}=x^{o(1)}, where nn is the input bit length. Our approach replaces μ(d)\mu(d) by its residue modulo 2, which is the squarefree indicator again: the number of chains d12∣md_1^2\mid m, d22∣d1,…d_2^2\mid d_1,\dots of depth LL is odd exactly when mm is squarefree, for m<22Lm<2^{2^L}. The parity of π\pi on [A,B][A,B] is then the parity of one count of tuples satisfying O(log⁡n)O(\log n) multiplications, which Anthropic's counting engine evaluates through a network whose variables have geometrically shrinking widths. We prove both theorems in Lean 4 (piParity_TM_rate, piIntervalParity_TM_rate; axioms propext, Classical.choice, Quot.sound). The result does not give deterministic prime finding or the exact value of π(x)\pi(x): the parity can be even on every interval one queries, and exact counts seem to need iterated products, for whose product-tree verifiers we prove a lower bound in Lean. The constants are astronomical, and the 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. M. Agrawal, N. Kayal, and N. Saxena, PRIMES is in P , Ann. of Math. (2) 160 (2004), no. 2, 781--793.
  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. R. C. Baker, G. Harman, and J. Pintz, The difference between consecutive primes, II , Proc. London Math. Soc. (3) 83 (2001), no. 3, 532--562.
  4. M. Deléglise and J. 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.
  5. 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
  6. J. C. Lagarias, V. S. Miller, and A. M. Odlyzko, Computing π(x)\pi(x): the M eissel-- L ehmer method , Math. Comp. 44 (1985), no. 170, 537--560.
  7. J. C. Lagarias and A. M. Odlyzko, Computing π(x)\pi(x): an analytic method , J. Algorithms 8 (1987), no. 2, 173--191.
  8. 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.
  9. A. V. Lelechenko, Parity of the number of primes in a given interval and algorithms of the sublinear summation , Visn. Odes. Nats. Univ., Mat. Mekh. 18 (2013), no. 1(17), 104--114; arXiv:1305.1639.arXiv
  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 20 referencesShow fewer references
  1. 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
  2. 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
  3. 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
  4. R. Sladkey, A successive approximation algorithm for computing the divisor summatory function , arXiv:1206.3369, June 2012.arXiv
  5. T. Tao, Deterministic way to find primes -- discussion thread , The polymath blog, 28 July 2009, https://polymathprojects.org/2009/07/28/deterministic-way-to-find-primes-discussion-thread/.link
  6. T. Tao, E. Croot III, and H. Helfgott, Deterministic methods to find primes , Math. Comp. 81 (2012), no. 278, 1233--1246; arXiv:1009.3956 (as D. H. J. Polymath).arXiv
  7. 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
  8. V. 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 , preprint, November 2026; source in the directory classnumber-note/ of TulsyanRepo26 .
  9. 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 .
  10. 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 f5aad1a .link

Version history

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