norm_num
extensions on natural numbers #
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.
Note: evalMinFac.aux
does not raise a stack overflow, which can be checked by replacing the
prf'
in the recursive call by something like (.sort .zero)
A predicate representing partial progress in a proof of minFac
.
Instances For
The norm_num
extension which identifies expressions of the form minFac n
.