A verified factorization algorithm for integer polynomials with polynomial complexity

Jose Divasón 🌐, Sebastiaan J. C. Joosten 🌐, René Thiemann 🌐 and Akihisa Yamada 📧

February 6, 2018

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Short vectors in lattices and factors of integer polynomials are related. Each factor of an integer polynomial belongs to a certain lattice. When factoring polynomials, the condition that we are looking for an irreducible polynomial means that we must look for a small element in a lattice, which can be done by a basis reduction algorithm. In this development we formalize this connection and thereby one main application of the LLL basis reduction algorithm: an algorithm to factor square-free integer polynomials which runs in polynomial time. The work is based on our previous Berlekamp–Zassenhaus development, where the exponential reconstruction phase has been replaced by the polynomial-time basis reduction algorithm. Thanks to this formalization we found a serious flaw in a textbook.


BSD License


Session LLL_Factorization