This file provides a
norm_num extension to prove that natural numbers are prime and compute
its minimal factor. Todo: compute the list of all factors.
Implementation Notes #
For numbers larger than 25 bits, the primality proof produced by
norm_num is an expression
that is thousands of levels deep, and the Lean kernel seems to raise a stack overflow when
type-checking that proof. If we want an implementation that works for larger primes, we should
generate a proof that has a smaller depth.
evalMinFac.aux does not raise a stack overflow, which can be checked by replacing the
prf' in the recursive call by something like