Merge branch 'george' of https://github.com/trishullab/PutnamBench in…

…to george

lean4/src/putnam_1984_a6.lean

@@ -15,10 +15,12 @@ Let $n$ be a positive integer, and let $f(n)$ denote the last nonzero digit in t
 theorem putnam_1984_a6
     (f : ℕ → ℕ)
     (hf : ∀ n, some (f n) = (Nat.digits 10 (n !)).find? (fun d ↦ d ≠ 0))
-    (P : (ℕ → ℕ) → ℕ → Prop)
-    (P_def : ∀ g p, P g p ↔
-      if p = 0 then (∀ q > 0, ¬ Periodic g q) else IsLeast {q | 0 < q ∧ Periodic g q} p) :
+    (IsPeriodicFrom : ℕ → (ℕ → ℕ) → ℕ → Prop)
+    (IsPeriodicFrom_def : ∀ x f p, IsPeriodicFrom x f p ↔ Periodic (f ∘ (· + x)) p)
+    (P : ℕ → (ℕ → ℕ) → ℕ → Prop)
+    (P_def : ∀ x g p, P x g p ↔ if p = 0 then (∀ q > 0, ¬ IsPeriodicFrom x g q) else
+        IsLeast {q | 0 < q ∧ IsPeriodicFrom x g q} p) :
     ∃ g : ℕ → ℕ,
       (∀ᵉ (k > 0) (a : Fin k → ℕ) (ha : Injective a), f (∑ i, 5 ^ (a i)) = g (∑ i, a i)) ∧
-      P g putnam_1984_a6_solution :=
+      P 1 g putnam_1984_a6_solution :=
   sorry

lean4/src/putnam_2021_a1.lean

@@ -10,8 +10,9 @@ Each hop has length $5$, and after each hop the grasshopper is at a point whose
 What is the smallest number of hops needed for the grasshopper to reach the point $(2021, 2021)$?
 -/
 theorem putnam_2021_a1
-  (P : List (ℤ × ℤ) → Prop)
-  (hP : ∀ l, P l ↔ l.length ≥ 1 ∧ l[0]! = (0, 0) ∧ l[l.length-1]! = (2021, 2021) ∧
-    ∀ n ∈ Finset.range (l.length-1), Real.sqrt ((l[n]!.1 - l[n + 1]!.1)^2 + (l[n]!.2 - l[n + 1]!.2)^2) = 5) :
-  IsLeast {n | ∃ l, P l ∧ l.length = n} putnam_2021_a1_solution :=
-sorry
+    (P : List (ℤ × ℤ) → Prop)
+    (P_def : ∀ l, P l ↔ l.Chain' fun p q ↦ (p.1 - q.1) ^ 2 + (p.2 - q.2) ^ 2 = 25) :
+    IsLeast
+      {k | ∃ l, P ((0, 0) :: l) ∧ l.getLast! = (2021, 2021) ∧ l.length = k}
+      putnam_2021_a1_solution :=
+  sorry