From d252cd92e2b2bdec9ac3cb141f7b61c728bb74fb Mon Sep 17 00:00:00 2001 From: George Tsoukalas Date: Mon, 9 Dec 2024 18:41:27 +0000 Subject: [PATCH] Add files and some initial formalizations for Putnam 2024. --- lean4/src/putnam_2024_a1.lean | 10 ++++++++++ lean4/src/putnam_2024_a2.lean | 11 +++++++++++ lean4/src/putnam_2024_a3.lean | 16 ++++++++++++++++ lean4/src/putnam_2024_a4.lean | 22 ++++++++++++++++++++++ lean4/src/putnam_2024_a5.lean | 8 ++++++++ lean4/src/putnam_2024_a6.lean | 13 +++++++++++++ lean4/src/putnam_2024_b1.lean | 16 ++++++++++++++++ lean4/src/putnam_2024_b2.lean | 6 ++++++ lean4/src/putnam_2024_b3.lean | 11 +++++++++++ lean4/src/putnam_2024_b4.lean | 6 ++++++ lean4/src/putnam_2024_b5.lean | 20 ++++++++++++++++++++ lean4/src/putnam_2024_b6.lean | 14 ++++++++++++++ 12 files changed, 153 insertions(+) create mode 100644 lean4/src/putnam_2024_a1.lean create mode 100644 lean4/src/putnam_2024_a2.lean create mode 100644 lean4/src/putnam_2024_a3.lean create mode 100644 lean4/src/putnam_2024_a4.lean create mode 100644 lean4/src/putnam_2024_a5.lean create mode 100644 lean4/src/putnam_2024_a6.lean create mode 100644 lean4/src/putnam_2024_b1.lean create mode 100644 lean4/src/putnam_2024_b2.lean create mode 100644 lean4/src/putnam_2024_b3.lean create mode 100644 lean4/src/putnam_2024_b4.lean create mode 100644 lean4/src/putnam_2024_b5.lean create mode 100644 lean4/src/putnam_2024_b6.lean diff --git a/lean4/src/putnam_2024_a1.lean b/lean4/src/putnam_2024_a1.lean new file mode 100644 index 0000000..9aab623 --- /dev/null +++ b/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 diff --git a/lean4/src/putnam_2024_a2.lean b/lean4/src/putnam_2024_a2.lean new file mode 100644 index 0000000..ee5bdae --- /dev/null +++ b/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 diff --git a/lean4/src/putnam_2024_a3.lean b/lean4/src/putnam_2024_a3.lean new file mode 100644 index 0000000..b66b46d --- /dev/null +++ b/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 diff --git a/lean4/src/putnam_2024_a4.lean b/lean4/src/putnam_2024_a4.lean new file mode 100644 index 0000000..da50df2 --- /dev/null +++ b/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 diff --git a/lean4/src/putnam_2024_a5.lean b/lean4/src/putnam_2024_a5.lean new file mode 100644 index 0000000..8fdc69e --- /dev/null +++ b/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 diff --git a/lean4/src/putnam_2024_a6.lean b/lean4/src/putnam_2024_a6.lean new file mode 100644 index 0000000..84443ff --- /dev/null +++ b/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 diff --git a/lean4/src/putnam_2024_b1.lean b/lean4/src/putnam_2024_b1.lean new file mode 100644 index 0000000..7bb3782 --- /dev/null +++ b/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 diff --git a/lean4/src/putnam_2024_b2.lean b/lean4/src/putnam_2024_b2.lean new file mode 100644 index 0000000..aa1bd4a --- /dev/null +++ b/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 diff --git a/lean4/src/putnam_2024_b3.lean b/lean4/src/putnam_2024_b3.lean new file mode 100644 index 0000000..2ccbbfa --- /dev/null +++ b/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 diff --git a/lean4/src/putnam_2024_b4.lean b/lean4/src/putnam_2024_b4.lean new file mode 100644 index 0000000..48b9810 --- /dev/null +++ b/lean4/src/putnam_2024_b4.lean @@ -0,0 +1,6 @@ +import Mathlib + +/- TODO -/ +theorem putnam_2024_b4 + : 1 = 1 := + sorry diff --git a/lean4/src/putnam_2024_b5.lean b/lean4/src/putnam_2024_b5.lean new file mode 100644 index 0000000..dab6b43 --- /dev/null +++ b/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 diff --git a/lean4/src/putnam_2024_b6.lean b/lean4/src/putnam_2024_b6.lean new file mode 100644 index 0000000..80e6e7d --- /dev/null +++ b/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