Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada: A verified LLL algorithm. Arch. Formal Proofs 2018 (2018)