A verified factorization algorithm for integer polynomials with polynomial complexity

  1. Jose Divasón
  2. Sebastiaan Joosten
  3. René Thiemann
  4. Akihisa Yamada
Revista:
Archive of Formal Proofs

ISSN: 2150-914x

Año de publicación: 2018

Páginas: 1-80

Tipo: Artículo

GOOGLE SCHOLAR lock_openAcceso abierto editor
Repositorio institucional: lock_openAcceso abierto Editor

Proyectos relacionados

Álgebra computacional: formalización y aplicaciones a la fiabilidad de redes y al prcesamiento de imágenes biomédicas.

2018/00009/001

Resumen

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.