1 paper
Katharina Kreuzer, Tobias Nipkow
This paper describes the formal verification of NP-hardness reduction functions of two key problems relevant in algebraic lattice theory: the closest vector problem and the shortes…