# A verified factorization algorithm for integer polynomials with polynomial complexity

 Title: A verified factorization algorithm for integer polynomials with polynomial complexity Authors: Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada Submission date: 2018-02-06 Abstract: 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. BibTeX: @article{LLL_Factorization-AFP, author = {Jose Divasón and Sebastiaan Joosten and René 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{http://isa-afp.org/entries/LLL_Factorization.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: LLL_Basis_Reduction, Perron_Frobenius Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.