### Abstract

The Lenstra-Lenstra-Lovász basis reduction algorithm, also known as LLL algorithm, is an algorithm to find a basis with short, nearly orthogonal vectors of an integer lattice. Thereby, it can also be seen as an approximation to solve the shortest vector problem (SVP), which is an NP-hard problem, where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm also possesses many applications in diverse fields of computer science, from cryptanalysis to number theory, but it is specially well-known since it was used to implement the first polynomial-time algorithm to factor polynomials. In this work we present the first mechanized soundness proof of the LLL algorithm to compute short vectors in lattices. The formalization follows a textbook by von zur Gathen and Gerhard.

### License

BSD License

### History

May 25, 2018
  Integrated much faster LLL implementation based on integer arithmetic (Bottesch, Haslbeck, Thiemann)
April 16, 2018
  Integrated formal complexity bounds (Haslbeck, Thiemann)

### Topics

- Computer science/Algorithms/Mathematical
- Mathematics/Algebra

### Session LLL_Basis_Reduction

- Missing_Lemmas
- More_IArray
- Norms
- Int_Rat_Operations
- Cost
- List_Representation
- Gram_Schmidt_2
- Gram_Schmidt_Int
- LLL
- LLL_Impl
- LLL_Complexity
- LLL_Number_Bounds
- LLL_Certification
- FPLLL_Solver

### Depends on

- Algebraic Numbers in Isabelle/HOL
- The Factorization Algorithm of Berlekamp and Zassenhaus

### Used by

- Hardness of Lattice Problems
- Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
- Linear Inequalities
- A verified factorization algorithm for integer polynomials with polynomial complexity

### Auto-related entries

- Hardness of Lattice Problems

## Cite

×

LLL_Basis_Reduction-AFP

    @article{LLL_Basis_Reduction-AFP,
      author  = {Ralph Bottesch and Jose Divasón and Max W. Haslbeck and Sebastiaan J. C. Joosten and René Thiemann and Akihisa Yamada},
      title   = {A verified LLL algorithm},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/LLL_Basis_Reduction.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
- Sep 7, 2018 : Isabelle2018
- Aug 16, 2018 : Isabelle2018
- Feb 3, 2018 : Isabelle2017