Deterministic factoring in time N^{o(1)}
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-28-000015
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-28-000015/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-28-000015/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'