cs.CC — Computational Complexity

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

Contributed by Isaac Rudich, Louis-Martin Rousseau

The current best upper bound for deterministic factoring is $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 $N$ in $N^{o(1)}$ steps: for every $k\ge 1$ it runs within $C_k\,2^{n/k}$ steps on $n$-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.