Email Gateway (Aug 22 2022 at 16:43): Email Gateway (Aug 22 2022 at 16:43):From: Tobias Nipkow <nipkow@in.tum.de>
A verified factorization algorithm for integer polynomials with polynomial
complexity
Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
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.
https://www.isa-afp.org/entries/LLL_Factorization.html
Textbook authors beware!
smime.p7s
Last updated: Apr 25 2024 at 08:20 UTC