Babai's Nearest Plane Algorithm

γ-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 γ=2^n/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.