HEXAGONbeta

Deterministic Factoring in Time No(1)N^{o(1)}

A mix of human-written and AI-generated textHuman understanding: some partscs.CC — Computational Complexitymath.NT — Number Theorycs.AI — Artificial Intelligencecs.DS — Data Structures and Algorithmscs.LO — Logic in Computer Science

Contributed by Isaac Rudich ↗, Louis-Martin Rousseau ↗

Version 1 / Oct 29, 2026 / CC BY 4.0

Abstract

The current best upper bound for deterministic factoring is N1/5+o(1)N^{1/5+o(1)}. We provide a Lean certificate that there exists a deterministic Turing machine that computes the smallest prime factor of every NN in No(1)N^{o(1)} steps: for every k≥1k\ge 1 it runs within Ck 2n/kC_k\,2^{n/k} steps on nn-bit inputs. The algorithm reduces factoring to counting divisors with prescribed leading bits, and counts them by leveraging the counting engine used to refute the Exponential Time Hypothesis (ETH). The Lean statement that a reader must check to verify the proof is only 13 lines and only uses Mathlib. The full proof is about 35,000 lines. This note was written less than 24 hours after the ETH refutations were posted. No human-readable explanation of these results exists yet, and their Lean proofs are long: Anthropic's alone runs to about 152,000 lines. Our proof re-proves only the part of the counting engine it needs and imports nothing from those developments. We hope this application, with its short statement, serves as a stepping stone for those working to understand the engine; a follow-up paper will explain this proof in detail.

Provenance statement

The paper states plainly that the ideas and the Lean proof were generated by AI (Claude Opus 5.5, Anthropic). The authors specified the formal statement, revised it until it was as simple to audit as we could make it, and audited it; we did not read the proof, which is checked by Lean. Claude Opus 5.5 also drafted the paper's explanation of the proof and checked its citations, and the authors edited the text. The intent of this work is to share an application of the counting engine behind the ETH refutations, as a more approachable entry point than the full refutation proofs.

Formalizations

Tools used

Lean
LeanVersion 4.35.0
Anthropic
Claude OpusVersion 5.5

References

  1. H. Albuquerque and S. Majid. Quasialgebra structure of the octonions. Journal of Algebra , 220(1):188--224, 1999. Numbering cited from arXiv:math/9802116.arXiv
  2. J. C. Baez. The octonions. Bulletin of the American Mathematical Society , 39(2):145--205, 2002.
  3. D. H. Bailey. FFT s in external or hierarchical memory. The Journal of Supercomputing , 4(1):23--35, 1990.
  4. A. Bostan, P. Gaudry, and É . Schost. Linear recurrences with polynomial coefficients and application to integer factorization and C artier-- M anin operator. SIAM Journal on Computing , 36(6):1777--1806, 2007.
  5. Claude (Anthropic) . A 2o(n)2^{o(n)} time algorithm for 3- SAT . Preprint, unrefereed; Lean development in the repository anthropics/formal-math, folder eth, 2026. Dated 26 October 2026.
  6. J. H. Conway and D. A. Smith. On Quaternions and Octonions: Their Geometry, Arithmetic, and Symmetry . A K Peters, Natick, MA, 2003.
  7. S. A. Cook and R. A. Reckhow. Time bounded random access machines. Journal of Computer and System Sciences , 7(4):354--375, 1973.
  8. J. W. Cooley and J. W. Tukey. An algorithm for the machine calculation of complex F ourier series. Mathematics of Computation , 19(90):297--301, 1965.
  9. D. Coppersmith. Small solutions to polynomial equations, and low exponent RSA vulnerabilities. Journal of Cryptology , 10(4):233--260, 1997.
  10. E. Costa and D. Harvey. Faster deterministic integer factorization. Mathematics of Computation , 83(285):339--345, 2014.
Show all 41 referencesShow fewer references
  1. R. Crandall and C. Pomerance. Prime Numbers: A Computational Perspective . Springer, New York, second edition, 2005.
  2. R. Curticapean and M. Xia. Parameterizing the permanent: genus, apices, minors, evaluation mod 2k2^k. In Proceedings of the 56th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2015) , pages 994--1009, 2015.
  3. L. de Moura and S. Ullrich. The L ean 4 theorem prover and programming language. In Automated Deduction -- CADE 28 , volume 12699 of Lecture Notes in Computer Science , pages 625--635. Springer, 2021.
  4. J. D. Dixon. Asymptotically fast factorization of integers. Mathematics of Computation , 36(153):255--260, 1981.
  5. P. Erd ő s. Beweis eines S atzes von T schebyschef. Acta Litterarum ac Scientiarum Regiae Universitatis Hungaricae Francisco-Josephinae, Sectio Scientiarum Mathematicarum (Szeged) , 5:194--198, 1932.
  6. A. Galluccio and M. Loebl. On the theory of P faffian orientations. I . P erfect matchings and permanents. Electronic Journal of Combinatorics , 6:R6, 1999.
  7. Y. Gao, Y. Feng, H. Hu, and Y. Pan. On factoring and power divisor problems via rank-3 lattices and the second vector. Mathematics of Computation , 2026. Published online 18 March 2026; arXiv:2512.19076.arXiv
  8. D. Harvey. An exponent one-fifth algorithm for deterministic integer factorisation. Mathematics of Computation , 90(332):2937--2950, 2021.
  9. D. Harvey and M. Hittmeir. A log-log speedup for exponent one-fifth deterministic integer factorisation. Mathematics of Computation , 91(335):1367--1379, 2022.
  10. X. He and A. Sahai. Refuting a conjecture of U mans and W ang on arithmetic-progression divisor covers. arXiv:2608.06681, 2026.arXiv
  11. M. Hittmeir. A babystep-giantstep method for faster deterministic integer factorization. Mathematics of Computation , 87(314):2915--2935, 2018.
  12. M. Hittmeir. A time-space tradeoff for L ehman's deterministic integer factorization method. Mathematics of Computation , 90(330):1999--2010, 2021.
  13. P. Hrube š , A. Wigderson, and A. Yehudayoff. Non-commutative circuits and the sum-of-squares problem. Journal of the American Mathematical Society , 24(3):871--898, 2011. Numbering cited from ECCC TR10-021.
  14. R. Impagliazzo and R. Paturi. On the complexity of kk- SAT . Journal of Computer and System Sciences , 62(2):367--375, 2001.
  15. R. S. Lehman. Factoring large integers. Mathematics of Computation , 28(126):637--646, 1974.
  16. A. K. Lenstra and H. W. Lenstra, Jr., editors. The Development of the Number Field Sieve , volume 1554 of Lecture Notes in Mathematics . Springer, 1993.
  17. H. W. Lenstra, Jr. Factoring integers with elliptic curves. Annals of Mathematics , 126(3):649--673, 1987.
  18. H. W. Lenstra, Jr. and C. Pomerance. A rigorous time bound for factoring integers. Journal of the American Mathematical Society , 5(3):483--516, 1992.
  19. M. A. Morrison and J. Brillhart. A method of factoring and the factorization of F7F_7 . Mathematics of Computation , 29(129):183--205, 1975.
  20. J. Ne š et ř il and S. Poljak. On the complexity of the subgraph problem. Commentationes Mathematicae Universitatis Carolinae , 26(2):415--419, 1985.
  21. OpenAI . The E xponential T ime H ypothesis is false. Preprint, unrefereed, 2026. Dated 17 October 2026, revised 25 October 2026. https://github.com/openai/math/blob/main/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf.link
  22. J. M. Pollard. Theorems on factorization and primality testing. Proceedings of the Cambridge Philosophical Society , 76(3):521--528, 1974.
  23. C. Pomerance. Analysis and comparison of some integer factoring algorithms. In H. W. Lenstra, Jr. and R. Tijdeman, editors, Computational Methods in Number Theory, Part I , volume 154 of Mathematical Centre Tracts , pages 89--139. Mathematisch Centrum, Amsterdam, 1982.
  24. A. Sch ö nhage and V. Strassen. Schnelle M ultiplikation großer Z ahlen. Computing , 7(3--4):281--292, 1971.
  25. D. Shanks. Class number, a theory of factorization, and genera. In 1969 Number Theory Institute (Proc. Sympos. Pure Math., Vol. XX, Stony Brook, N.Y., 1969) , pages 415--440. Amer. Math. Soc., 1971.
  26. P. W. Shor. Algorithms for quantum computation: discrete logarithms and factoring. In Proceedings of the 35th Annual Symposium on Foundations of Computer Science , pages 124--134. IEEE Computer Society Press, 1994.
  27. V. Strassen. Einige R esultate ü ber B erechnungskomplexit ä t. Jahresbericht der Deutschen Mathematiker-Vereinigung , 78(1):1--8, 1976/77.
  28. The mathlib Community . The L ean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020) , pages 367--381, 2020.
  29. C. Umans and S. Wang. A number-theoretic conjecture implying faster algorithms for polynomial factorization and integer factorization. arXiv:2511.10851, 2025.arXiv
  30. P. van Emde Boas. Machine models and simulations. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume A: Algorithms and Complexity , pages 1--66. Elsevier, Amsterdam, 1990.
  31. R. Williams. A new algorithm for optimal 2-constraint satisfaction and its implications. Theoretical Computer Science , 348(2--3):357--365, 2005.

Version history

  1. v1Submitted by Isaac RudichInitial depositCurrentOct 28, 2026