A verified factorization algorithm for integer polynomials with polynomial complexity

Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada

Archive of Formal Proofs 2018.


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.


  AFP entry


author = {Jose Divas\'on and Sebastiaan Joosten and Ren\'e Thiemann and Akihisa Yamada},
title = {A verified factorization algorithm for integer polynomials with polynomial complexity},
journal = {Archive of Formal Proofs},
month = feb,
year = 2018,
note = {\url{}, Formal proof development},
ISSN = {2150-914x}
Nach oben scrollen