### 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.

### License

BSD License

### Topics

- Mathematics/Algebra

### Session LLL_Factorization

- Factor_Bound_2
- Missing_Dvd_Int_Poly
- LLL_Factorization_Impl
- LLL_Factorization
- Sub_Sums
- Factorization_Algorithm_16_22
- Modern_Computer_Algebra_Problem

### Depends on

- A verified LLL algorithm
- Perron-Frobenius Theorem for Spectral Radius Analysis

### Auto-related entries

- Polynomial Interpolation
- The Factorization Algorithm of Berlekamp and Zassenhaus

## Cite

×

LLL_Factorization-AFP

    @article{LLL_Factorization-AFP,
      author  = {Jose Divasón and Sebastiaan J. C. Joosten and René Thiemann and Akihisa Yamada},
      title   = {A verified factorization algorithm for integer polynomials with polynomial complexity},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/LLL_Factorization.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Feb 7, 2018 : Isabelle2017