Import GapCVP hardness formalization

LeanPool.lean

@@ -1664,6 +1664,75 @@ import LeanPool.GKPCarry.ModularPrefix
 import LeanPool.GKPCarry.PowerResidues
 import LeanPool.GKPCarry.Statement
 import LeanPool.GKPCarry.UnitCarryCounting
+import LeanPool.GapCVP
+import LeanPool.GapCVP.Part01
+import LeanPool.GapCVP.Part01A
+import LeanPool.GapCVP.Part01B
+import LeanPool.GapCVP.Part02
+import LeanPool.GapCVP.Part03
+import LeanPool.GapCVP.Part03A
+import LeanPool.GapCVP.Part03B
+import LeanPool.GapCVP.Part03C
+import LeanPool.GapCVP.Part03D
+import LeanPool.GapCVP.Part03E
+import LeanPool.GapCVP.Part03F
+import LeanPool.GapCVP.Part03G
+import LeanPool.GapCVP.Part04
+import LeanPool.GapCVP.Part04A
+import LeanPool.GapCVP.Part04B
+import LeanPool.GapCVP.Part04C
+import LeanPool.GapCVP.Part04D
+import LeanPool.GapCVP.Part04E
+import LeanPool.GapCVP.Part04F
+import LeanPool.GapCVP.Part04G
+import LeanPool.GapCVP.Part05
+import LeanPool.GapCVP.Part05A
+import LeanPool.GapCVP.Part05B
+import LeanPool.GapCVP.Part05C
+import LeanPool.GapCVP.Part05D
+import LeanPool.GapCVP.Part05E
+import LeanPool.GapCVP.Part05F
+import LeanPool.GapCVP.Part06
+import LeanPool.GapCVP.Part06A
+import LeanPool.GapCVP.Part06B
+import LeanPool.GapCVP.Part06C
+import LeanPool.GapCVP.Part06D
+import LeanPool.GapCVP.Part07
+import LeanPool.GapCVP.Part07A
+import LeanPool.GapCVP.Part07B
+import LeanPool.GapCVP.Part07C
+import LeanPool.GapCVP.Part07D
+import LeanPool.GapCVP.Part07E
+import LeanPool.GapCVP.Part07F
+import LeanPool.GapCVP.Part07G
+import LeanPool.GapCVP.Part08
+import LeanPool.GapCVP.Part08A
+import LeanPool.GapCVP.Part08B
+import LeanPool.GapCVP.Part08C
+import LeanPool.GapCVP.Part08D
+import LeanPool.GapCVP.Part09
+import LeanPool.GapCVP.Part10
+import LeanPool.GapCVP.Part10A
+import LeanPool.GapCVP.Part10B
+import LeanPool.GapCVP.Part11
+import LeanPool.GapCVP.Part11A
+import LeanPool.GapCVP.Part11B
+import LeanPool.GapCVP.Part11C
+import LeanPool.GapCVP.Part12
+import LeanPool.GapCVP.Part12A
+import LeanPool.GapCVP.Part12B
+import LeanPool.GapCVP.Part12C
+import LeanPool.GapCVP.Part12D
+import LeanPool.GapCVP.Part13
+import LeanPool.GapCVP.Part14
+import LeanPool.GapCVP.Part14A
+import LeanPool.GapCVP.Part14B
+import LeanPool.GapCVP.Part15
+import LeanPool.GapCVP.Part16
+import LeanPool.GapCVP.Part16A
+import LeanPool.GapCVP.Part16B
+import LeanPool.GapCVP.Part17
+import LeanPool.GapCVP.Part18
 import LeanPool.GrothendieckVanishing
 import LeanPool.GrothendieckVanishing.ClosedImmersion
 import LeanPool.GrothendieckVanishing.ClosedImmersionCohomology

LeanPool/GapCVP.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2026 OpenAI and Dean Cureton. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: OpenAI, Dean Cureton
+-/
+
+import LeanPool.GapCVP.Part18
+
+/-!
+# Polynomial-factor hardness of the closest vector problem
+
+Source: url:https://github.com/openai/ten-proofs
+Authors: OpenAI, Dean Cureton
+Status: verified
+Main declarations: `GapCVP.Comparator.gapCVP400IsNPHard`
+Tags: computational-complexity, np-hardness, lattice-problems, coding-theory
+MSC: 68Q17, 68Q25, 11H06, 94B35
+-/
+
+/-! # Polynomial-factor hardness of the closest vector problem -/

LeanPool/GapCVP/Part01.lean

@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2026 OpenAI and Dean Cureton. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: OpenAI, Dean Cureton
+-/
+
+import LeanPool.GapCVP.Part01B
+
+/-! # GapCVP proof, part 01 -/