Add Putnam 2024 Lean files and some initial formalizations

lean4/src/putnam_2024_a1.lean

@@ -0,0 +1,10 @@
+import Mathlib
+
+abbrev putnam_2024_a1_solution : Set ℕ := sorry
+theorem putnam_2024_a1 :
+  {n : ℕ | 0 < n ∧
+    ∃ a b c : ℤ,
+      0 < a ∧ 0 < b ∧ 0 < c ∧
+      2 * a ^ n + 3 * b ^ n = 4 * c ^ n}
+  = putnam_2024_a1_solution :=
+sorry

lean4/src/putnam_2024_a2.lean

@@ -0,0 +1,11 @@
+import Mathlib
+
+open Polynomial
+
+abbrev putnam_2024_a2_solution : Set ℝ[X] := sorry
+theorem putnam_2024_a2 :
+  {P : ℝ[X] |
+    ∃ Q : ℝ[X],
+    ∀ x, P.eval (P.eval x) = (P.eval x - x) ^ 2 * Q.eval x}
+  = putnam_2024_a2_solution :=
+sorry

lean4/src/putnam_2024_a3.lean

@@ -0,0 +1,16 @@
+import Mathlib
+
+open Finset Function
+
+abbrev putnam_2024_a3_solution : Prop := sorry
+theorem putnam_2024_a3
+  (S : Finset (Fin 3 × Fin 2024 → Fin 6072))
+  (hS : ∀ T ∈ S, Bijective T)
+  (hS' : ∀ T ∈ S,
+    (∀ j : Icc 1 2024, T (0, j) < T (1, j) ∧ T (1, j) < T (2, j)) ∧
+    (∀ (i : Fin 3) (j : Fin 2023), T (i, j) < T (i, (j : Fin 2024) + 1))
+  ) :
+    putnam_2024_a3_solution ↔
+    ∃ (a : Fin 3) (c : Fin 3) (b : Fin 2024) (d : Fin 2024),
+      (({T ∈ S | T (a,b) < T (c,d)}.card : ℝ) / S.card) ∈ Set.Icc (1/3 : ℝ) (2/3) :=
+  sorry

lean4/src/putnam_2024_a4.lean

@@ -0,0 +1,22 @@
+import Mathlib
+
+open List
+
+#check List
+
+abbrev putnam_2024_a4_solution : Set ℕ := sorry
+theorem putnam_2024_a4
+  (IsRearrangeableWith : ℕ → ℤ → ℤ → Prop)
+  (IsRearrangeableWith_def : ∀ (p : ℕ) (a r : ℤ),
+    IsRearrangeableWith p a r ↔
+      ∃ b : List ℤ,
+        b ~ (map (fun i => a^i) (range (p - 5 + 1))) ∧
+        b.Chain' (fun s t ↦ (p : ℤ) ∣ t - s - r)
+  ) :
+    {p : ℕ |
+      Nat.Prime p ∧ 5 < p ∧
+      ∃ a r : ℤ,
+        1 ≤ r ∧ r ≤ p - 1 ∧
+        IsRearrangeableWith p a r}
+    = putnam_2024_a4_solution :=
+sorry

lean4/src/putnam_2024_a5.lean

@@ -0,0 +1,8 @@
+import Mathlib
+
+/- TODO -/
+
+abbrev putnam_2024_a5_solution : ℝ := sorry
+theorem putnam_2024_a5
+  : 1 = 1 :=
+sorry

lean4/src/putnam_2024_a6.lean

@@ -0,0 +1,13 @@
+import Mathlib
+
+open Matrix
+
+abbrev putnam_2024_a6_solution : ℝ := sorry
+theorem putnam_2024_a6
+  (c : ℕ → ℝ)
+  (hc : ∃ᵉ (r > 0), ∀ x, |x| < r → HasSum (fun n => c n * x ^ n) ((1 - 3 * x - √ (1 - 14 * x + 9 * x ^2) / 4)))
+  (n : ℕ) (hn : 0 < n)
+  (A : Matrix (Fin n) (Fin n) ℝ)
+  (A_def : ∀ i j, A i j = c ((i : ℕ) + (j : ℕ) - 1)) :
+    det A = putnam_2024_a6_solution :=
+sorry

lean4/src/putnam_2024_b1.lean

@@ -0,0 +1,16 @@
+import Mathlib
+
+open List
+
+abbrev putnam_2024_b1_solution : Set (ℕ × ℕ) := sorry
+theorem putnam_2024_b1
+  (n k : ℕ)
+  (hn : 0 < n) (hk : 0 < k)
+  (Grid : Fin n → Fin n → ℕ)
+  (Grid_def : ∀ i j, Grid i j = (i : ℕ) + (j : ℕ) - k)
+  : (n, k) ∈ putnam_2024_b1_solution ↔
+      ∃ L : List (Fin n × Fin n),
+        L.length = n ∧
+        L.Pairwise (fun i j => i.1 ≠ j.1 ∧ i.2 ≠ j.2) ∧
+        map (fun l => Grid l.1 l.2) L ~ map (fun q ↦ q + 1) (range n) :=
+sorry

lean4/src/putnam_2024_b2.lean

@@ -0,0 +1,6 @@
+import Mathlib
+
+/- Convex Quadrilaterals may be out of reach of mathlib. -/
+theorem putnam_2024_b2
+  : 1 = 1 :=
+  sorry

lean4/src/putnam_2024_b3.lean

@@ -0,0 +1,11 @@
+import Mathlib
+
+open Real
+
+theorem putnam_2024_b3
+  (r : ℕ → ℝ)
+  (hr : r 0 = 0)
+  (r_def : ∀ n, 1 ≤ n → IsLeast {x : ℝ | x > r (n - 1) ∧ tan x = x} (r n))
+  (n : ℕ) (hn: 1 ≤ n) :
+    0 < r (n + 1) - r n - π ∧ r (n + 1) - r n - π < 1 / ((n ^ 2 + n ) * π) :=
+sorry

lean4/src/putnam_2024_b4.lean

@@ -0,0 +1,6 @@
+import Mathlib
+
+/- TODO -/
+theorem putnam_2024_b4
+  : 1 = 1 :=
+  sorry

lean4/src/putnam_2024_b5.lean

@@ -0,0 +1,20 @@
+import Mathlib
+
+open Polynomial List
+
+abbrev putnam_2024_b5_solution : ℝ[X] := sorry
+theorem putnam_2024_b5
+  (k m : ℕ)
+  (hk : 0 < k) (hm : 0 < m)
+  (f : ℕ+ → ℕ)
+  (f_def : ∀ n, f n = Set.encard
+    {s : List ℤ × List ℤ × ℤ |
+      let (x,y,z) := s;
+      x.length = k ∧ y.length = m ∧
+      (Pairwise (·≤·) x ∧ 1 ≤ x.head! ∧ x.getLast! ≤ z) ∧
+      (Pairwise (·≤·) y ∧ 1 ≤ y.head! ∧ y.getLast! ≤ z) ∧
+      z ≤ n}
+  ) :
+    (∀ n, f n = putnam_2024_b5_solution.eval (n : ℝ)) ∧
+    (∀ i, 0 ≤ putnam_2024_b5_solution.coeff i) :=
+sorry

lean4/src/putnam_2024_b6.lean

@@ -0,0 +1,14 @@
+import Mathlib
+
+open Real Filter Topology Set
+
+abbrev putnam_2024_b6_solution : ℝ := sorry
+theorem putnam_2024_b6
+  (F : ℝ → ℝ → ℝ)
+  (F_def : ∀ a x, (0 ≤ x ∧ x < 1) → F a x = ∑' (n : ℕ+), (n : ℝ) ^ a * exp (2 * n) * x ^ ((n : ℕ) ^ 2)) :
+  ∀ a : ℝ,
+    (a < putnam_2024_b6_solution →
+      Tendsto (λ x ↦ F a x * exp (-1/(1-x))) (𝓝[<] 1) (𝓝 0)) ∧
+    (a > putnam_2024_b6_solution →
+      Tendsto (λ x ↦ F a x * exp (-1/(1-x))) (𝓝[<] 1) atTop) :=
+sorry