Email Gateway (Aug 22 2022 at 16:42): Email Gateway (Aug 22 2022 at 16:42):From: Tobias Nipkow <nipkow@in.tum.de>
A verified LLL algorithm
Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
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.
https://www.isa-afp.org/entries/LLL_Basis_Reduction.html
Enjoy!
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC