Deterministic Factoring in Time N^O(1)

A formalized result claims that the smallest prime factor of any integer can be computed deterministically in subpolynomial time in the integer’s value: on an n-bit input, the running time is at most Cₖ·2^(n/k) for every fixed k ≥ 1. This would sharply improve on the stated best previous deterministic factoring bound, N^(1/5+o(1)). The approach turns factoring into counting divisors whose leading bits match prescribed values, then applies a counting method associated with recent proofs refuting the Exponential Time Hypothesis.

The central contribution is a Lean certificate, not a human-readable exposition: its theorem statement is 13 lines and uses only Mathlib, while the complete proof is about 35,000 lines. The authors say Claude Opus 5.5 generated the ideas and proof; they set and simplified the formal statement and checked it, but did not read the proof, which Lean verifies. The work re-proves the portion of the counting method it needs rather than importing the much larger ETH-refutation developments. It was prepared less than a day after those refutations appeared, and no readable explanation of the underlying argument is yet available; a follow-up is promised. The result is presented both as a striking factoring claim and as a more accessible formalization for researchers seeking to understand the new counting machinery.