Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Babai's Nearest Plane Algorithm

Email Gateway (Oct 31 2024 at 10:39):

From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

I'm glad to announce a new AFP entry:

Babai's Nearest Plane Algorithm
by Eric Ren, Sage Binder and Katherine Kosaian

Gamma-CVP is the problem of finding a vector in L that is within gamma 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
gamma-CVP for gamma = 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.

https://www.isa-afp.org/entries/Babai_Nearest_Plane.html

Best,
René

Last updated: Jan 04 2025 at 20:18 UTC