
A
verified
LLL
algorithm
Title: 
A verified LLL algorithm 
Authors:

Ralph Bottesch,
Jose Divasón,
Maximilian Haslbeck,
Sebastiaan Joosten,
René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at) and
Akihisa Yamada

Submission date: 
20180202 
Abstract: 
The LenstraLenstraLová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 NPhard 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 wellknown since it was used to implement the first
polynomialtime 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. 
Change history: 
[20180416]: Integrated formal complexity bounds (Haslbeck, Thiemann)
[20180525]: Integrated much faster LLL implementation based on integer arithmetic (Bottesch, Haslbeck, Thiemann) 
BibTeX: 
@article{LLL_Basis_ReductionAFP,
author = {Ralph Bottesch and Jose Divasón and Maximilian Haslbeck and Sebastiaan Joosten and René Thiemann and Akihisa Yamada},
title = {A verified LLL algorithm},
journal = {Archive of Formal Proofs},
month = feb,
year = 2018,
note = {\url{https://isaafp.org/entries/LLL_Basis_Reduction.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Algebraic_Numbers, Berlekamp_Zassenhaus 
Used by: 
Linear_Inequalities, LLL_Factorization, Modular_arithmetic_LLL_and_HNF_algorithms 
