Add Lean statement for 2022 A5

lean4/src/putnam_2022_a5.lean

@@ -0,0 +1,20 @@
+import Mathlib
+
+noncomputable abbrev putnam_2022_a5_solution : ℕ := sorry
+-- 290
+
+theorem putnam_2022_a5
+    (IsValidMove : Set (Fin 2022) → Set (Fin 2022) → Prop)
+    (IsValidMove_def : ∀ x y, IsValidMove x y ↔
+      (x = y ∧ ∀ i < 2021, i ∉ x → i + 1 ∈ x) ∨
+      ∃ i < 2021, i ∉ x ∧ i + 1 ∉ x ∧ y = x ∪ {i, i + 1})
+    (IsValidGame : List (Set (Fin 2022)) → Prop)
+    (IsValidGame_def : ∀ g, IsValidGame g ↔ (∃ gt, g = ∅ :: gt) ∧ g.Chain' IsValidMove)
+    (ConformsToStrategy : List (Set (Fin 2022)) → (Set (Fin 2022) → Set (Fin 2022)) → Prop)
+    (ConformsToStrategy_def : ∀ g s, ConformsToStrategy g s ↔
+      ∀ (i) (h : i + 1 < g.length), Even i → g[i + 1] = s g[i]) :
+    IsGreatest
+      {n | ∃ s, (∀ x, IsValidMove x (s x)) ∧ ∀ g,
+        IsValidGame g → ConformsToStrategy g s → ∃ gh x, g = gh ++ [x] → n ≤ xᶜ.ncard}
+      putnam_2022_a5_solution :=
+  sorry