Statements from 2025

README.md

@@ -19,7 +19,7 @@ We are hosting a [**leaderboard**](https://trishullab.github.io/PutnamBench/lead
 ## Statistics 
 | Language      | Count          |
 | ------------- | -------------- |
-| Lean 4        | 660            |
+| Lean 4        | 672            |
 | Isabelle      | 640            |
 | Coq           | 412            |
 

informal/putnam.json

@@ -5424,5 +5424,105 @@
         "tags": [
             "analysis"
         ]
+    },
+    {
+        "problem_name": "putnam_2025_a1",
+        "informal_statement": "Let $m_0$ and $n_0$ be distinct positive integers. For every positive integer $k$, define $m_k$ and $n_k$ to be the relatively prime positive integers such that \\[ \\frac{m_k}{n_k} = \\frac{2m_{k-1} + 1}{2n_{k-1} + 1}. \\] Prove that $2m_k + 1$ and $2n_k + 1$ are relatively prime for all but finitely many positive integers $k$.",
+        "informal_solution": "None.",
+        "tags": [
+            "number_theory"
+        ]
+    },
+    {
+        "problem_name": "putnam_2025_a2",
+        "informal_statement": "Find the largest real number $a$ and the smallest real number $b$ such that \\[ ax(\\pi - x) \\le \\sin x \\le bx(\\pi - x) \\] for all $x$ in the interval $[0, \\pi]$.",
+        "informal_solution": "Show that the optimal constants are $a = \\tfrac{1}{\\pi}$ and $b = \\tfrac{4}{\\pi^2}$.",
+        "tags": [
+            "analysis"
+        ]
+    },
+    {
+        "problem_name": "putnam_2025_a3",
+        "informal_statement": "Alice and Bob play a game with a string of $n$ digits, each of which is restricted to be 0, 1, or 2. Initially all the digits are 0. A legal move is to add or subtract 1 from one digit to create a new string that has not appeared before. A player with no legal move loses, and the other player wins. Alice goes first, and the players alternate moves. For each $n \\ge 1$, determine which player has a strategy that guarantees winning.",
+        "informal_solution": "Show that Bob has a winning strategy for all $n \\ge 1$.",
+        "tags": [
+            "combinatorics"
+        ]
+    },
+    {
+        "problem_name": "putnam_2025_a4",
+        "informal_statement": "Find the minimal value of $k$ such that there exist $k$-by-$k$ real matrices $A_1, \\ldots, A_{2025}$ with the property that $A_i A_j = A_j A_i$ if and only if $|i - j| \\in \\{0, 1, 2024\\}$.",
+        "informal_solution": "Show that the minimal value is $3$.",
+        "tags": [
+            "linear_algebra"
+        ]
+    },
+    {
+        "problem_name": "putnam_2025_a5",
+        "informal_statement": "Let $n$ be an integer with $n \\ge 2$. For a sequence $s = (s_1, \\ldots, s_{n-1})$ where each $s_i = \\pm 1$, let $f(s)$ be the number of permutations $(a_1, \\ldots, a_n)$ of $\\{1, 2, \\ldots, n\\}$ such that $s_i(a_{i+1} - a_i) > 0$ for all $i$. For each $n$, determine the sequences $s$ for which $f(s)$ is maximal.",
+        "informal_solution": "Show that $f(s)$ is maximized exactly when the signs alternate, that is, when $s_i = (-1)^{i+1}$ for all $i$ or $s_i = (-1)^i$ for all $i$.",
+        "tags": [
+            "combinatorics"
+        ]
+    },
+    {
+        "problem_name": "putnam_2025_a6",
+        "informal_statement": "Let $b_0 = 0$ and, for $n \\ge 0$, define $b_{n+1} = 2b_n^2 + b_n + 1$. For each $k \\ge 1$, show that $b_{2^{k+1}} - 2b_{2^k}$ is divisible by $2^{2k+2}$ but not by $2^{2k+3}$.",
+        "informal_solution": "None.",
+        "tags": [
+            "number_theory"
+        ]
+    },
+    {
+        "problem_name": "putnam_2025_b1",
+        "informal_statement": "Suppose that each point in the plane is colored either red or green, subject to the following condition: For every three noncollinear points $A$, $B$, $C$ of the same color, the center of the circle passing through $A$, $B$, $C$ is also this color. Prove that all points of the plane are the same color.",
+        "informal_solution": "Show that all points of the plane must have the same color.",
+        "tags": [
+            "geometry",
+            "combinatorics"
+        ]
+    },
+    {
+        "problem_name": "putnam_2025_b2",
+        "informal_statement": "Let $f: [0,1] \\to [0, \\infty)$ be strictly increasing and continuous. Let $R$ be the region bounded by $x = 0$, $x = 1$, $y = 0$, and $y = f(x)$. Let $x_1$ be the $x$-coordinate of the centroid of $R$. Let $x_2$ be the $x$-coordinate of the centroid of the solid generated by rotating $R$ about the $x$-axis. Prove that $x_1 < x_2$.",
+        "informal_solution": "None.",
+        "tags": [
+            "analysis",
+            "geometry"
+        ]
+    },
+    {
+        "problem_name": "putnam_2025_b3",
+        "informal_statement": "Suppose $S$ is a nonempty set of positive integers with the property that if $n$ is in $S$, then every positive divisor of $2025^n - 15^n$ is in $S$. Must $S$ contain all positive integers?",
+        "informal_solution": "Yes, $S$ must contain all positive integers.",
+        "tags": [
+            "number_theory"
+        ]
+    },
+    {
+        "problem_name": "putnam_2025_b4",
+        "informal_statement": "For $n \\geq 2$, let $A = [a_{i,j}]_{i,j=1}^n$ be an $n$-by-$n$ matrix of nonnegative integers such that: (a) $a_{i,j} = 0$ when $i + j \\leq n$; (b) $a_{i+1,j} \\in \\{a_{i,j}, a_{i,j} + 1\\}$ when $1 \\leq i \\leq n-1$ and $1 \\leq j \\leq n$; and (c) $a_{i,j+1} \\in \\{a_{i,j}, a_{i,j} + 1\\}$ when $1 \\leq i \\leq n$ and $1 \\leq j \\leq n-1$. Let $S$ be the sum of the entries of $A$, and let $N$ be the number of nonzero entries of $A$. Prove that $S \\leq \\frac{(n+2)N}{3}$.",
+        "informal_solution": "None.",
+        "tags": [
+            "linear_algebra",
+            "combinatorics"
+        ]
+    },
+    {
+        "problem_name": "putnam_2025_b5",
+        "informal_statement": "Let $p$ be a prime number greater than 3. For each $k \\in \\{1, \\ldots, p-1\\}$, let $I(k) \\in \\{1, 2, \\ldots, p-1\\}$ be such that $k \\cdot I(k) \\equiv 1 \\pmod{p}$. Prove that the number of integers $k \\in \\{1, \\ldots, p-2\\}$ such that $I(k+1) < I(k)$ is greater than $p/4 - 1$.",
+        "informal_solution": "None.",
+        "tags": [
+            "number_theory"
+        ]
+    },
+    {
+        "problem_name": "putnam_2025_b6",
+        "informal_statement": "Let $\\mathbb{N} = \\{1, 2, 3, \\ldots\\}$. Find the largest real constant $r$ such that there exists a function $g: \\mathbb{N} \\to \\mathbb{N}$ such that $$g(n+1) - g(n) \\geq (g(g(n)))^r$$ for all $n \\in \\mathbb{N}$.",
+        "informal_solution": "Show that the largest possible value of $r$ is $1/4$.",
+        "tags": [
+            "analysis",
+            "number_theory"
+        ]
     }
 ]

lean4/src/putnam_2025_a1.lean

@@ -0,0 +1,19 @@
+import Mathlib
+
+/--
+Let $m_0$ and $n_0$ be distinct positive integers. For every positive integer $k$,
+define $m_k$ and $n_k$ to be the relatively prime positive integers such that
+$$\frac{m_k}{n_k} = \frac{2m_{k-1} + 1}{2n_{k-1} + 1}.$$
+Prove that $2m_k + 1$ and $2n_k + 1$ are relatively prime for all but finitely many
+positive integers $k$.
+-/
+theorem putnam_2025_a1
+  (m n : ℕ → ℕ)
+  (hm : ∀ k : ℕ, 0 < m k)
+  (hn : ∀ k : ℕ, 0 < n k)
+  (h_distinct : m 0 ≠ n 0)
+  (h_coprime : ∀ k : ℕ, 0 < k → Nat.Coprime (m k) (n k))
+  (h_recurrence : ∀ k : ℕ,
+    (m (k + 1) : ℚ) / (n (k + 1) : ℚ) = (2 * (m k : ℚ) + 1) / (2 * (n k : ℚ) + 1)) :
+  {k : ℕ | ¬Nat.Coprime (2 * m k + 1) (2 * n k + 1)}.Finite :=
+sorry

lean4/src/putnam_2025_a2.lean

@@ -0,0 +1,17 @@
+import Mathlib
+
+open Real
+
+noncomputable abbrev putnam_2025_a2_solution : ℝ × ℝ := sorry
+-- (1 / π, 4 / π ^ 2)
+
+/--
+Find the largest real number $a$ and the smallest real number $b$ such that
+$$ax(\pi - x) \le \sin x \le bx(\pi - x)$$
+for all $x$ in the interval $[0, \pi]$.
+-/
+theorem putnam_2025_a2 (a b : ℝ) :
+  ((a, b) = putnam_2025_a2_solution) ↔
+  (IsGreatest {a' : ℝ | ∀ x ∈ Set.Icc 0 π, a' * x * (π - x) ≤ sin x} a ∧
+   IsLeast {b' : ℝ | ∀ x ∈ Set.Icc 0 π, sin x ≤ b' * x * (π - x)} b) :=
+sorry

lean4/src/putnam_2025_a3.lean

@@ -0,0 +1,39 @@
+import Mathlib
+
+open Finset Function
+
+/--
+Alice and Bob play a game with a string of $n$ digits, each of which is restricted
+to be 0, 1, or 2. Initially all the digits are 0. A legal move is to add or subtract 1
+from one digit to create a new string that has not appeared before. A player with no
+legal move loses, and the other player wins. Alice goes first, and the players alternate
+moves. For each $n \ge 1$, determine which player has a strategy that guarantees winning.
+-/
+
+abbrev GameString (n : ℕ) := Fin n → Fin 3
+
+abbrev initialState (n : ℕ) : GameString n := fun _ => 0
+
+abbrev isValidMove {n : ℕ} (s1 s2 : GameString n) : Prop :=
+  (∃! i : Fin n, s1 i ≠ s2 i) ∧
+  ∀ i : Fin n, s1 i ≠ s2 i →
+    ((s1 i).val + 1 = (s2 i).val ∨ (s2 i).val + 1 = (s1 i).val)
+
+abbrev IsValidGamePlay {n : ℕ} (play : List (GameString n)) : Prop :=
+  play.Chain isValidMove (initialState n) ∧
+  (initialState n :: play).Nodup
+
+inductive HasWinningStrategy (n : ℕ) : List (GameString n) → Prop where
+  | win (play : List (GameString n)) (s : GameString n) :
+      IsValidGamePlay (play ++ [s]) →
+      (∀ s', IsValidGamePlay (play ++ [s, s']) → HasWinningStrategy n (play ++ [s, s'])) →
+      HasWinningStrategy n play
+
+abbrev AliceHasWinningStrategy (n : ℕ) : Prop := HasWinningStrategy n []
+
+abbrev putnam_2025_a3_solution : ℕ → Prop := sorry
+-- fun _ => False
+
+theorem putnam_2025_a3 (n : ℕ) (hn : 1 ≤ n) :
+    putnam_2025_a3_solution n ↔ AliceHasWinningStrategy n := by
+  sorry

lean4/src/putnam_2025_a4.lean

@@ -0,0 +1,16 @@
+import Mathlib
+
+abbrev putnam_2025_a4_solution : ℕ := sorry
+-- 3
+
+/--
+Find the minimal value of $k$ such that there exist $k$-by-$k$ real matrices
+$A_1, \ldots, A_{2025}$ with the property that $A_i A_j = A_j A_i$ if and only if
+$|i - j| \in \{0, 1, 2024\}$.
+-/
+theorem putnam_2025_a4 :
+  IsLeast {k : ℕ | ∃ A : Fin 2025 → Matrix (Fin k) (Fin k) ℝ,
+    ∀ i j : Fin 2025, i ≤ j →
+      (A i * A j = A j * A i ↔ j.val - i.val ∈ ({0, 1, 2024} : Set ℕ))}
+  putnam_2025_a4_solution :=
+sorry

lean4/src/putnam_2025_a5.lean

@@ -0,0 +1,23 @@
+import Mathlib
+
+open Finset
+
+abbrev putnam_2025_a5_solution : (n : ℕ) → Set (Fin n → ℤˣ) := sorry
+-- fun n => {s | (∀ i : Fin n, s i = (-1) ^ (i.val + 1)) ∨ (∀ i : Fin n, s i = (-1) ^ i.val)}
+
+abbrev f (n : ℕ) (s : Fin n → ℤˣ) : ℕ :=
+  Finset.card {σ : Equiv.Perm (Fin (n + 1)) |
+    ∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))}
+
+/--
+Let $n$ be an integer with $n \ge 2$. For a sequence $s = (s_1, \ldots, s_{n-1})$ where each
+$s_i = \pm 1$, let $f(s)$ be the number of permutations $(a_1, \ldots, a_n)$ of $\{1, 2, \ldots, n\}$
+such that $s_i(a_{i+1} - a_i) > 0$ for all $i$. For each $n$, determine the sequences $s$ for which
+$f(s)$ is maximal.
+-/
+theorem putnam_2025_a5
+    (n : ℕ)
+    (hn : 1 ≤ n)
+    (s : Fin n → ℤˣ) :
+    (∀ t : Fin n → ℤˣ, f n t ≤ f n s) ↔ s ∈ putnam_2025_a5_solution n := by
+  sorry

lean4/src/putnam_2025_a6.lean

@@ -0,0 +1,15 @@
+import Mathlib
+
+abbrev b : ℕ → ℤ
+| 0 => 0
+| n + 1 => 2 * (b n) ^ 2 + b n + 1
+
+/--
+Let $b_0 = 0$ and, for $n \ge 0$, define $b_{n+1} = 2b_n^2 + b_n + 1$.
+For each $k \ge 1$, show that $b_{2^{k+1}} - 2b_{2^k}$ is divisible by $2^{2k+2}$
+but not by $2^{2k+3}$.
+-/
+theorem putnam_2025_a6 (k : ℕ) (hk : 1 ≤ k) :
+    (2 ^ (2 * k + 2) : ℤ) ∣ (b (2 ^ (k + 1)) - 2 * b (2 ^ k)) ∧
+    ¬((2 ^ (2 * k + 3) : ℤ) ∣ (b (2 ^ (k + 1)) - 2 * b (2 ^ k))) := by
+  sorry

lean4/src/putnam_2025_b1.lean

@@ -0,0 +1,17 @@
+import Mathlib
+
+open Affine EuclideanGeometry
+
+/--
+Suppose that each point in the plane is colored either red or green, subject to the following
+condition: For every three noncollinear points $A$, $B$, $C$ of the same color, the center of the
+circle passing through $A$, $B$, $C$ is also this color. Prove that all points of the plane are the
+same color.
+-/
+theorem putnam_2025_b1
+    (color : EuclideanSpace ℝ (Fin 2) → Bool)
+    (h : ∀ (s : Simplex ℝ (EuclideanSpace ℝ (Fin 2)) 2),
+      (∀ i j : Fin 3, color (s.points i) = color (s.points j)) →
+      color s.circumcenter = color (s.points 0)) :
+    ∃ c : Bool, ∀ P : EuclideanSpace ℝ (Fin 2), color P = c := by
+  sorry

lean4/src/putnam_2025_b2.lean

@@ -0,0 +1,19 @@
+import Mathlib
+
+open Set Real MeasureTheory Interval
+
+/--
+Let $f: [0,1] \to [0, \infty)$ be strictly increasing and continuous.
+Let $R$ be the region bounded by $x = 0$, $x = 1$, $y = 0$, and $y = f(x)$.
+Let $x_1$ be the $x$-coordinate of the centroid of $R$.
+Let $x_2$ be the $x$-coordinate of the centroid of the solid generated by rotating $R$ about the $x$-axis.
+Prove that $x_1 < x_2$.
+-/
+theorem putnam_2025_b2
+    (f : ℝ → ℝ)
+    (hf_cont : ContinuousOn f (Icc 0 1))
+    (hf_mono : StrictMonoOn f (Icc 0 1))
+    (hf_nonneg : ∀ x ∈ Icc (0 : ℝ) 1, 0 ≤ f x) :
+    (∫ x in (0:ℝ)..1, x * f x) / (∫ x in (0:ℝ)..1, f x) <
+    (∫ x in (0:ℝ)..1, x * (f x) ^ 2) / (∫ x in (0:ℝ)..1, (f x) ^ 2) := by
+  sorry

lean4/src/putnam_2025_b3.lean

@@ -0,0 +1,19 @@
+import Mathlib
+
+open Finset
+
+abbrev putnam_2025_b3_solution : Prop := sorry
+-- True
+
+/--
+Suppose $S$ is a nonempty set of positive integers with the property that if $n$ is in $S$,
+then every positive divisor of $2025^n - 15^n$ is in $S$. Must $S$ contain all positive integers?
+-/
+theorem putnam_2025_b3 :
+    putnam_2025_b3_solution ↔
+    ∀ S : Set ℕ,
+      S.Nonempty →
+      (∀ n ∈ S, 0 < n) →
+      (∀ n ∈ S, ∀ d : ℕ, 0 < d → d ∣ (2025 ^ n - 15 ^ n) → d ∈ S) →
+      S = {n : ℕ | 0 < n} := by
+  sorry

lean4/src/putnam_2025_b4.lean

@@ -0,0 +1,35 @@
+import Mathlib
+
+open BigOperators Finset Matrix
+
+/--
+For $n \geq 2$, let $A = [a_{i,j}]_{i,j=1}^n$ be an $n$-by-$n$ matrix of nonnegative integers such that:
+(a) $a_{i,j} = 0$ when $i + j \leq n$;
+(b) $a_{i+1,j} \in \{a_{i,j}, a_{i,j} + 1\}$ when $1 \leq i \leq n-1$ and $1 \leq j \leq n$; and
+(c) $a_{i,j+1} \in \{a_{i,j}, a_{i,j} + 1\}$ when $1 \leq i \leq n$ and $1 \leq j \leq n-1$.
+
+Let $S$ be the sum of the entries of $A$, and let $N$ be the number of nonzero entries of $A$.
+Prove that $S \leq \frac{(n+2)N}{3}$.
+
+Note: We parameterize by $m$ where $n = m + 2$, so $m \geq 0$ and the matrix is $(m+2) \times (m+2)$.
+With 0-indexing (indices $0, \ldots, m+1$), the conditions become:
+(a) $a_{i,j} = 0$ when $i + j \leq m$ (since original $i + j \leq n$ with 1-indexing becomes $(i'+1) + (j'+1) \leq m+2$)
+(b) $a_{i+1,j} \in \{a_{i,j}, a_{i,j}+1\}$ when $i \leq m$
+(c) $a_{i,j+1} \in \{a_{i,j}, a_{i,j}+1\}$ when $j \leq m$
+-/
+theorem putnam_2025_b4
+    (m : ℕ)
+    (A : Matrix (Fin (m + 2)) (Fin (m + 2)) ℕ)
+    (ha : ∀ (i j : Fin (m + 2)), (i : ℕ) + (j : ℕ) ≤ m → A i j = 0)
+    (hb : ∀ (i : Fin (m + 1)) (j : Fin (m + 2)),
+      A (Fin.succ i) j = A (Fin.castSucc i) j ∨
+      A (Fin.succ i) j = A (Fin.castSucc i) j + 1)
+    (hc : ∀ (i : Fin (m + 2)) (j : Fin (m + 1)),
+      A i (Fin.succ j) = A i (Fin.castSucc j) ∨
+      A i (Fin.succ j) = A i (Fin.castSucc j) + 1)
+    (S : ℕ)
+    (hS : S = ∑ i : Fin (m + 2), ∑ j : Fin (m + 2), A i j)
+    (N : ℕ)
+    (hN : N = #{p : Fin (m + 2) × Fin (m + 2) | A p.1 p.2 ≠ 0}) :
+    3 * S ≤ (m + 4) * N := by
+  sorry

lean4/src/putnam_2025_b5.lean

@@ -0,0 +1,21 @@
+import Mathlib
+
+open Finset BigOperators
+
+abbrev modInv (p : ℕ) (k : ℕ) : ℕ := ZMod.val ((k : ZMod p)⁻¹)
+
+abbrev descentCount (p : ℕ) : ℕ :=
+  #{k ∈ Finset.Icc 1 (p - 2) | modInv p (k + 1) < modInv p k}
+
+/--
+Let $p$ be a prime number greater than 3. For each $k \in \{1, \ldots, p-1\}$,
+let $I(k) \in \{1, 2, \ldots, p-1\}$ be such that $k \cdot I(k) \equiv 1 \pmod{p}$.
+Prove that the number of integers $k \in \{1, \ldots, p-2\}$ such that
+$I(k+1) < I(k)$ is greater than $p/4 - 1$.
+-/
+theorem putnam_2025_b5
+    (p : ℕ)
+    (hp_prime : p.Prime)
+    (hp_gt : 3 < p) :
+    (p : ℚ) / 4 - 1 < descentCount p := by
+  sorry

lean4/src/putnam_2025_b6.lean

@@ -0,0 +1,19 @@
+import Mathlib
+
+open Real
+
+noncomputable abbrev putnam_2025_b6_solution : ℝ := sorry
+-- 1 / 4
+
+/--
+Let $\mathbb{N} = \{1, 2, 3, \ldots\}$. Find the largest real constant $r$ such that
+there exists a function $g: \mathbb{N} \to \mathbb{N}$ such that
+$$g(n+1) - g(n) \geq (g(g(n)))^r$$
+for all $n \in \mathbb{N}$.
+-/
+theorem putnam_2025_b6 :
+    IsGreatest
+      {r : ℝ | ∃ g : ℕ → ℕ, (∀ n : ℕ, 0 < n → 0 < g n) ∧
+        ∀ n : ℕ, 0 < n → ((g (g n) : ℝ) ^ r) ≤ (g (n + 1) : ℝ) - (g n : ℝ)}
+      putnam_2025_b6_solution := by
+  sorry