A formalization of the LLL basis reduction algorithm

DOI10.1007/978-3-319-94821-8_10zbMath1468.68287OpenAlexW2811256589MaRDI QIDQ1791154

René Thiemann, Jose Divasón, Akihisa Yamada, Sebastiaan J. C. Joosten

Publication date: 4 October 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-94821-8_10

Mathematics Subject Classification ID

Number-theoretic algorithms; complexity (11Y16) Lattices and convex bodies (number-theoretic aspects) (11H06) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL ⋮ A verified implementation of the Berlekamp-Zassenhaus factorization algorithm

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• HOL Light
• fpLLL
• Berlekamp Zassenhaus
• LLL Factorization
• Verified LLL
• Vector Spaces

This page was built for publication: A formalization of the LLL basis reduction algorithm