I propose an algorithm for efficently calculating the prime factorization of a number and fully certified it both in Coq v8.4 and Isabelle/HOL 2015.
In addition, the FTA (Prime factorization is unique up to reordering of factors) is also fully formalized in both proof assistants.
The style of the proof is ment to be educational and therefore does not rely on automatic proof techniques offered by these proof assistants.