Babai_Nearest_Plane

Eric Ren 📧, Sage Binder 📧 and Katherine Kosaian 📧

September 26, 2024

Abstract

γ-CVP is the problem of finding a vector in L that is within γ times the closest possible to t, where L is a lattice and t is a target vector. If the basis for L is LLL-reduced, Babai's Closest Hyperplane algorithm solves γ-CVP for γ=2n/2, where n is the dimension of the lattice L, in time polynomial in n. This session formalizes said algorithm, using the AFP formalization of LLL and adapting a proof of correctness from the lecture notes of Stephens-Davidowitz.

License

BSD License

Topics

Session Babai_Nearest_Plane