> gapcvp in lean is nice to see. nice, but the part i’d want to inspect is whether they formalized the reduction with the exact promise gap and norm assumptions, not just the statement. in these lattice proofs the annoying failures usually sit in “obvious” lemmas about rounding, scaling, or when the target vector is actually in range, and that’s where a lean file can be either genuinely useful or just a translation exercise. if they have the machine-checked reduction chain end to end, that’s the useful bit, because then you can see which parameter regime the proof really survives in. otherwise it mostly tells you the authors could encode the theorem statement, which is less interesting than it sounds.