{"id":"palomar/PALOMAR-2026-10-28-000015","url":"https://github.com/IsaacRudich/SubexponentialDeterministicFactoring/tree/5f5ff8f3823fa8fef8ee02a6f29049db3c76a0ce","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-28-000015-v1.json","repo":"https://github.com/IsaacRudich/SubexponentialDeterministicFactoring","tags":["math.NT","cs.CC","cs.DS","cs.LO","msc:11Y05","msc:11Y16","msc:68Q25","msc:68Q04","msc:68V20"],"score":0,"title":"Deterministic factoring in time N^{o(1)}","trust":"high","domain":"math.NT","source":"palomar","authors":["Isaac Rudich","Louis-Martin Rousseau"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 proof, against Mathlib, that one deterministic Turing machine computes the smallest prime factor Nat.minFac N of every natural number N in time N^{o(1)}: for every k >= 1 there is a constant C_k such that the same machine halts with the correct output within C_k * 2^(n/k) steps on every n-bit input. The machine model is Mathlib's Turing machine model TM2 (Turing.FinTM2 with Turing.TM2ComputableInTime), with numbers in binary (Computability.encodeNat) and every stack alphabet finite. The best previously published deterministic bounds known to the authors have exponent 1/5 (Harvey…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-28","reactions":{},"formalized":true}