Skip to Content

A verified factorization algorithm for integer polynomials with polynomial complexity

Posted on

Authors:

  • Divasón, Jose
  • Joosten, Sebastiaan J. C.
  • Thiemann, René
  • Yamada, Akihisa

Formal proof development

Published in: Archive of Formal Proofs

https://www.isa-afp.org/entries/LLL_Factorization.html

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 entry:

@article{Divason18c,
 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.},
 author = {Jose Divas{\'o}n and Sebastiaan Jozef Christiaan Joosten and Ren{\'e} Thiemann and Akihisa Yamada},
 bdsk-url-1 = {https://www.isa-afp.org/entries/LLL_Factorization.html},
 day = {6},
 issn = {2150-914x},
 journal = {Archive of Formal Proofs},
 language = {English},
 month = {2},
 publisher = {SourceForge},
 title = {A verified factorization algorithm for integer polynomials with polynomial complexity},
 url = {https://www.isa-afp.org/entries/LLL_Factorization.html},
 year = {2018}
}