Paper Info
Title
A verified factorization algorithm for integer polynomials with polynomial complexity.
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.
Year
Venue
Field
2018
Archive of Formal Proofs
Integer,Exponential function,Lattice (order),Polynomial,Algorithm,Factorization,Irreducible polynomial,Time complexity,Factorization of polynomials,Mathematics
DocType
Volume
Citations 
Journal
2018
0
PageRank 
References 
Authors
0.34
0
4
Name
Order
Citations
PageRank
Jose Divasón1289.96
Sebastiaan J. C. Joosten2176.87
René Thiemann398469.38
Akihisa Yamada 000244010.86