What was already known
The authors compare with the deterministic exponent-one-fifth factoring algorithms of Harvey (2021) and Harvey–Hittmeir (2022). The construction re-proves the part of Claude’s new 3-SAT counting engine needed to search for divisors through a multiplication network.
AI involvement
The pinned source explicitly attributes the mathematical ideas and Lean code to Claude. Rudich and Rousseau posed the questions and designed and audited the formal statement. Their direction is retained separately from the model-generated counting construction.
Importance
Would replace a fixed positive exponent of N in general deterministic factoring by N^{o(1)}. This is a distinct application of the counting engine, with its own exact machine theorem.
Limitations
The theorem outputs the smallest prime factor; iteration to produce the full factorization is explained but not formalized. The stronger exp(O(log N/√log log N)) bound is only a conjecture, with no proof asserted. Constants are not computed and the algorithm is described as galactic, so no practical cryptographic break is established. The authors audited the statement and explicitly did not read the proof.
Technical verification
The authors report a completed fresh Lean build, its measured duration and the axiom output for Factoring.subexponentialRate. Challenge and Solution use Mathlib TM2 with binary input/output and finite alphabets; the only reported axioms are propext, Classical.choice and Quot.sound. Registry admission alone is not the checking basis. No local replay was performed.
Formal checking
The authors report a completed fresh Lean build, its measured duration and the axiom output for Factoring.subexponentialRate. Challenge and Solution use Mathlib TM2 with binary input/output and finite alphabets; the only reported axioms are propext, Classical.choice and Quot.sound. Registry admission alone is not the checking basis. No local replay was performed. The source reports completion, but gives no exact check date.
- Checker
- Rudich and Rousseau: reported Lean 4.35.0 kernel build
- Scope
- A single deterministic Turing machine outputs the smallest prime factor Nat.minFac N of every natural number N in binary. For each integer k≥1 there is a constant C_k such that its running time on every n-bit input is at most C_k·2^{⌊n/k⌋}; all stack alphabets are finite. Thus the stated deterministic running time is N^{o(1)}.
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Few is the default when evidence for a higher level is insufficient. The authors explicitly say they did not read the proof. The repository gives a mechanism summary, but it does not document a completed human explanation of the central new argument.
Correction and publication history
Clarifies that the source reports completed checking but does not supply its exact completion date. Research claims and rating levels are unchanged.
Read this published revisionNewly reviewed source-backed algorithm with contribution-specific AI attribution and checking limits.
Read this published revision