Here 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.