Add Lean statement for 2023 A4

lean4/src/putnam_2023_a4.lean

@@ -0,0 +1,16 @@
+import Mathlib
+
+theorem putnam_2023_a4
+    (v : Fin 12 → EuclideanSpace ℝ (Fin 3))
+    (hv :
+      letI α : ℝ := (1 + √5) / 4
+      letI h : ℝ := 1 / 2
+      letI e : (Fin 3 → ℝ) ≃ EuclideanSpace ℝ (Fin 3) := (WithLp.equiv _ _).symm
+      ∃ g : EuclideanSpace ℝ (Fin 3) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 3),
+      g ∘ v = e ∘ ![![h, α, 0], ![-h,  α,  0], ![ h, -α,  0], ![-h, -α,  0],
+                    ![α, 0, h], ![ α,  0, -h], ![-α,  0,  h], ![-α,  0, -h],
+                    ![0, h, α], ![ 0, -h,  α], ![ 0,  h, -α], ![ 0, -h, -α]])
+    (w : EuclideanSpace ℝ (Fin 3))
+    (ε : ℝ) (hε : ε > 0) :
+    ∃ a : Fin 12 → ℤ, ‖∑ i, a i • v i - w‖ < ε :=
+  sorry