Verification of NP-Hardness Reduction Functions for Exact Lattice Problems

DOI10.1007/978-3-031-38499-8_21MaRDI QIDQ6492756zbMATH OpenFDO

Authors Tobias Nipkow

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_21

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• Approximate CVP in time \(2^{0.802 n}\) -- now in any norm!
• Approximating CVP to within almost-polynomial factors is NP-hard
• Concrete semantics. With Isabelle/HOL
• Factoring polynomials with rational coefficients
• Hardness of approximating the shortest vector problem in lattices
• scientific article; zbMATH DE number 5485482 (Why is no real title available?)
• scientific article; zbMATH DE number 1256724 (Why is no real title available?)
• scientific article; zbMATH DE number 1775383 (Why is no real title available?)
• scientific article; zbMATH DE number 2120513 (Why is no real title available?)
• scientific article; zbMATH DE number 7699437 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Lattice-based Cryptography
• On Lovász' lattice reduction and the nearest lattice point problem
• Sphere packings, lattices and groups. With additional contributions by E. Bannai, R. E. Borcherds, J. Leech, S. P. Norton, A. M. Odlyzko, R. A. Parker, L. Queen and B. B. Venkov.

Cited in

(2)

• Formalizing Coppersmith's method in Isabelle/HOL
• Formalizing the hidden number problem in Isabelle/HOL

This page was built for publication: Verification of NP-Hardness Reduction Functions for Exact Lattice Problems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6492756)