6 ms·
Carmichael numbers are quickly findable (Lean-verified) [pdf]
- jdb1729 9d agoHere it is proved that for all epsilon > 0 and sufficiently large n there exists a Carmichael number in the interval (n, n^(1+epsilon)] and furthermore it can be found along with its full factorization in time exp(O(log(log(n)) * log(log(log(n)))) on Mathlib's multi-stack Turing machine model. Formally verified in Lean.