ChristianZ97/putnambench-satp-v4.27 huggingface dataset:
Problem: putnam_2023_a6
Category: combinatorics

Alice and Bob play a game in which they take turns choosing integers from $1$ to $n$. Before any integers are chosen, Bob selects a goal of 'odd' or 'even'. On the first turn, Alice chooses one of the $n$ integers. On the second turn, Bob chooses one of the remaining integers. They continue alternately choosing one of the integers that has not yet been chosen, until the $n$th turn, which is forced and ends the game. Bob wins if the parity of $\{k : \mbox{the number $k$ was chosen on the $k$th turn}\}$ matches his goal. For which values of $n$ does Bob have a winning strategy?

Solution: Show that Bob has a winning strategy for all $n$.

Lean 4 formalization:
import Mathlib

open Finset

abbrev putnam_2023_a6_solution : Set ℕ := sorry
theorem putnam_2023_a6
    (IsValidGame : List ℕ → Prop)
    (IsValidGame_def : ∀ g, IsValidGame g ↔ g.Nodup ∧ (∀ i ∈ g, i ∈ Icc 1 g.length))
    (parityOf : List ℕ → ZMod 2)
    (parityOf_def : ∀ g, parityOf g = ((range g.length).filter fun i ↦ g[i]! = i + 1).card)
    (ConformsToStrategy : List ℕ → (List ℕ → ℕ) → Prop)
    (ConformsToStrategy_def : ∀ g s, ConformsToStrategy g s ↔
      ∀ (i) (h : i < g.length), Odd i → g[i] = s (g.take i))
    (IsValidStrategy : (List ℕ → ℕ) → Prop)
    (IsValidStrategy_def : ∀ s, IsValidStrategy s ↔
      ∀ (g : List ℕ), g.length > 0 → s g ∈ g)
    (IsWinningFor : ℕ → (List ℕ → ℕ) → Prop)
    (IsWinningFor_def : ∀ n s, IsWinningFor n s ↔
      IsValidStrategy s ∧ ∃ p, ∀ g, g.length = n → IsValidGame g → ConformsToStrategy g s → parityOf g = p) :
    {n : ℕ | 0 < n ∧ ∃ s, IsWinningFor n s} = putnam_2023_a6_solution := by
Problem: putnam_2023_b1
Category: combinatorics

Consider an $m$-by-$n$ grid of unit squares, indexed by $(i,j)$ with $1 \leq i \leq m$ and $1 \leq j \leq n$. There are $(m-1)(n-1)$ coins, which are initially placed in the squares $(i,j)$ with $1 \leq i \leq m-1$ and $1 \leq j \leq n-1$. If a coin occupies the square $(i,j)$ with $i \leq m-1$ and $j \leq n-1$ and the squares $(i+1,j)$, $(i,j+1)$, and $(i+1,j+1)$ are unoccupied, then a legal move is to slide the coin from $(i,j)$ to $(i+1,j+1)$. How many distinct configurations of coins can be reached starting from the initial configuration by a (possibly empty) sequence of legal moves?

Solution: Show that the number of such configurations is $\binom{m+n-2}{m-1}$.

Lean 4 formalization:
import Mathlib

open Nat

abbrev putnam_2023_b1_solution : ℕ → ℕ → ℕ := sorry
theorem putnam_2023_b1
(m n : ℕ)
(initcoins : ℕ → ℕ → Bool)
(hinitcoins : initcoins = (fun i j : ℕ => (i ≤ m - 2 ∧ j ≤ n - 2 : Bool)))
(IsLegalMove : (ℕ → ℕ → Bool) → (ℕ → ℕ → Bool) → Prop)
(IsLegalMove_def : ∀ coins1 coins2,
  IsLegalMove coins1 coins2 ↔
    ∃ i j, i < m - 1 ∧ j < n - 1 ∧
      coins1 i j ∧ !coins1 (i + 1) j ∧ !coins1 i (j + 1) ∧ !coins1 (i + 1) (j + 1) ∧
      !coins2 i j ∧ !coins2 (i + 1) j ∧ !coins2 i (j + 1) ∧ coins2 (i + 1) (j + 1) ∧
      (∀ i' j', ((i', j') ≠ (i, j) ∧ (i', j') ≠ (i + 1, j) ∧ (i', j') ≠ (i, j + 1) ∧ (i', j') ≠ (i + 1, j + 1))
        → coins1 i' j' = coins2 i' j'))
(IsLegalSeq : List (ℕ → ℕ → Bool) → Prop)
(IsLegalSeq_def : ∀ seq, IsLegalSeq seq ↔ seq.length ≥ 1 ∧ seq[0]! = initcoins ∧ (∀ i < seq.length - 1, IsLegalMove seq[i]! seq[i + 1]!))
(mnpos : 1 < m ∧ 1 < n)
: {config : ℕ → ℕ → Bool | ∃ seq : List (ℕ → ℕ → Bool), IsLegalSeq seq ∧ config = seq.getLast!}.encard = putnam_2023_b1_solution m n := by
Problem: putnam_2023_b2
Category: number_theory

For each positive integer $n$, let $k(n)$ be the number of ones in the binary representation of $2023 * n$. What is the minimum value of $k(n)$?

Solution: Show that the minimum value is 3.

Lean 4 formalization:
import Mathlib

open Nat

abbrev putnam_2023_b2_solution : ℕ := sorry
theorem putnam_2023_b2
: sInf {(digits 2 (2023*n)).sum | n > 0} = putnam_2023_b2_solution := by
Problem: putnam_2023_b3
Category: probability, combinatorics

A sequence $y_1, y_2, \ldots, y_k$ of real numbers is called zigzag if $k = 1$, or if $y_2 - y_1, y_3 - y_2, \ldots, y_k - y_{k-1}$ are nonzero and alternate in sign. Let $X_1, X_2,\ldots, X_n$ be chosen independently from the uniform distribution on $[0,1]$. Let $a(X_1, X_2, \ldots, X_n)$ be the largest value of $k$ for which there exists an increasing sequence of integers $i_1, i_2, \ldots, i_k$ such that $X_{i_1}, X_{i_2}, \ldots, X_{i_k}$ is zigzag. Find the expected value of $a(X_1, X_2, \ldots, X_n)$ for $n \ge 2$.

Solution: Show that the expected value is \frac{2n + 2}{3}.

Lean 4 formalization:
import Mathlib

open ProbabilityTheory Set

noncomputable abbrev putnam_2023_b3_solution : ℕ → ℝ := sorry
theorem putnam_2023_b3
    (IsZigZag : {k : ℕ} → (Fin k → ℝ) → Prop)
    (IsZigZag_def : ∀ (k : ℕ) [NeZero k] (y : Fin k → ℝ),
      IsZigZag y ↔ k = 1 ∨ ((∀ i : Fin k, i + 1 < k → y (i + 1) ≠ y i)) ∧
        (∀ i : Fin k, i + 2 < k → (y (i + 2) < y (i + 1) ↔ y i < y (i + 1))))
    (n : ℕ)
    (hn : 2 ≤ n)
    (a : (Fin n → Icc (0 : ℝ) 1) → ℕ)
    (ha : ∀ x, IsGreatest {k | ∃ i : Fin k ↪o Fin n, IsZigZag ((↑) ∘ x ∘ i)} (a x)) :
    𝔼[(↑) ∘ a] = putnam_2023_b3_solution n := by
Problem: putnam_2023_b4
Category: analysis

For a nonnegative integer $n$ and a strictly increasing sequence of real numbers $t_0,t_1,\dots,t_n$, let $f(t)$ be the corresponding real-valued function defined for $t \geq t_0$ by the following properties:
\begin{enumerate}
\item[(a)] $f(t)$ is continuous for $t \geq t_0$, and is twice differentiable for all $t>t_0$ other than $t_1,\dots,t_n$;
\item[(b)] $f(t_0)=1/2$;
\item[(c)] $\lim_{t \to t_k^+} f'(t)=0$ for $0 \leq k \leq n$;
\item[(d)] For $0 \leq k \leq n-1$, we have $f''(t)=k+1$ when $t_k<t<t_{k+1}$, and $f''(t)=n+1$ when $t>t_n$.
\end{enumerate}
Considering all choices of $n$ and $t_0,t_1,\dots,t_n$ such that $t_k \geq t_{k-1}+1$ for $1 \leq k \leq n$, what is the least possible value of $T$ for which $f(t_0+T)=2023$?

Solution: Show that the minimum value of $T$ is $29$.

Lean 4 formalization:
import Mathlib

open Nat Topology Filter

abbrev putnam_2023_b4_solution : ℝ := sorry
theorem putnam_2023_b4
    (tne : ℕ → (ℕ → ℝ) → Set ℝ)
    (htne : ∀ n ts, tne n ts = {t | t > ts 0 ∧ ∀ i : Fin n, t ≠ ts (i.1 + 1)}) :
    IsLeast
    {(T : ℝ) | 0 ≤ T ∧ ∃ (n : ℕ) (ts : ℕ → ℝ) (f : ℝ → ℝ),
      (∀ k : Fin n, ts (k.1 + 1) ≥ ts k.1 + 1) ∧
      ContinuousOn f (Set.Ici (ts 0)) ∧
      ContDiffOn ℝ 1 f (tne n ts) ∧
      DifferentiableOn ℝ (derivWithin f (tne n ts)) (tne n ts) ∧
      f (ts 0) = 0.5 ∧
      (∀ k : Fin (n + 1),
        Tendsto (derivWithin f (tne n ts)) (𝓝[>] (ts k.1)) (𝓝 0)) ∧
      (∀ k : Fin n,
        ∀ t ∈ Set.Ioo (ts k.1) (ts (k.1 + 1)),
          iteratedDerivWithin 2 f (tne n ts) t = k.1 + 1) ∧
      (∀ t > ts n,
        iteratedDerivWithin 2 f (tne n ts) t = n + 1) ∧
      f (ts 0 + T) = 2023}
    putnam_2023_b4_solution := by
Problem: putnam_2023_b5
Category: number_theory

Determine which positive integers $n$ have the following property: For all integers $m$ that are relatively prime to $n$, there exists a permutation $\pi:\{1,2,\dots,n\} \to \{1,2,\dots,n\}$ such that $\pi(\pi(k)) \equiv mk \pmod{n}$ for all $k \in \{1,2,\dots,n\}$.

Solution: Show that the desired property holds if and only if $n=1$ or $n \equiv 2 \pmod{4}$.

Lean 4 formalization:
import Mathlib

open Nat Topology Filter

abbrev putnam_2023_b5_solution : Set ℕ := sorry
theorem putnam_2023_b5
  (n : ℕ) :
  n ∈ putnam_2023_b5_solution ↔
    0 < n ∧
    (∀ m : ℤ, IsRelPrime m n → ∃ p : Equiv.Perm (Fin n),
      ∀ k : Fin n, (p (p k)).1 + 1 ≡ m * (k.1 + 1) [ZMOD n]) := by
Problem: putnam_2023_b6
Category: linear_algebra

Let $n$ be a positive integer. For $i$ and $j$ in $\{1,2,\dots,n\}$, let $s(i,j)$ be the number of pairs $(a,b)$ of nonnegative integers satisfying $ai+bj=n$. Let $S$ be the $n$-by-$n$ matrix whose $(i,j)$ entry is $s(i,j)$. For example, when $n=5$, we have $S = \begin{bmatrix}
6 & 3 & 2 & 2 & 2 \\
3 & 0 & 1 & 0 & 1 \\
2 & 1 & 0 & 0 & 1 \\
2 & 0 & 0 & 0 & 1 \\
2 & 1 & 1 & 1 & 2
\end{bmatrix}$. Compute the determinant of $S$.

Solution: Show that the determinant equals $(-1)^{\lceil n/2 \rceil-1}2\lceil\frac{n}{2}\rceil$.

Lean 4 formalization:
import Mathlib

open Nat Topology Filter

abbrev putnam_2023_b6_solution : ℕ → ℤ := sorry
theorem putnam_2023_b6
(n : ℕ)
(S : Matrix (Fin n) (Fin n) ℤ)
(npos : n > 0)
(hS : ∀ i j : Fin n, S i j = ∑' a : ℕ, ∑' b : ℕ, if a * (i.1 + 1) + b * (j.1 + 1) = (n : ℤ) then 1 else 0)
: S.det = putnam_2023_b6_solution n := by
Problem: putnam_2024_a1
Category: number_theory

Determine all positive integers $n$ for which there exist positive integers $a$, $b$ and $c$ satisfying $2a^n + 3b^n = 4c^n$.

Solution: Show that the only such positive integer is 1.

Lean 4 formalization:
import Mathlib

noncomputable 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 := by
Problem: putnam_2024_a2
Category: algebra

For which real polynomials $p$ is there a real polynomial $q$ such that
$p(p(x)) - x = (p(x) - x)^2q(x)$ for all real $x$?

Solution: Show that only the polynomials $\pm x + a$, where $a$ is a real number, are solutions.

Lean 4 formalization:
import Mathlib

open Polynomial

noncomputable abbrev putnam_2024_a2_solution : Set ℝ[X] := sorry
theorem putnam_2024_a2 :
    { p : Polynomial ℝ | ∃ (q : Polynomial ℝ),
      ∀ x, p.eval (p.eval x) - x = (p.eval x - x) ^ 2 * q.eval x } = putnam_2024_a2_solution := by
Problem: putnam_2024_a3
Category: combinatorics

Let $S$ be the set of bijections $$T : \{1, 2, 3\} \times \{1, 2, ..., 2024\} \to \{1, 2, ..., 6072\}$$
such that $T(1, j) < T(2, j) < T(3, j)$ for all $j \in \{1, 2, ..., 2024\}$ and
$T(i, j) < T(i, j + 1)$ for all $i \in \{1, 2, 3\}$ and $j \in \{1, 2, ..., 2023\}$.
Do there exist $a, c$ in $\{1, 2, 3\}$ and $b$ and $d$ in $\{1, 2, ..., 2024\}$ such that
the fraction of elements $T$ in $S$ for which $T(a, b) < T(c, d)$ is at least $1/3$ and at most $2/3$?

Solution: Shoe that there do such exist $a,c$.

Lean 4 formalization:
import Mathlib

noncomputable abbrev putnam_2024_a3_solution : Prop := sorry
theorem putnam_2024_a3
    (S : Set (ℕ × ℕ → ℕ))
    (hS : S = {T | Set.BijOn T (Finset.Icc 1 3 ×ˢ Finset.Icc 1 2024) (Finset.Icc 1 6072) ∧
      (∀ j ∈ Finset.Icc 1 2024, StrictMonoOn (fun i => T (i, j)) (Set.Icc 1 3)) ∧
      (∀ i ∈ Finset.Icc 1 3, StrictMonoOn (fun j => T (i, j)) (Set.Icc 1 2024)) ∧
      (∀ x, x ∉ Finset.Icc 1 3 ×ˢ Finset.Icc 1 2024 → T x = 0)}) :
    (∃ a ∈ Finset.Icc 1 3, ∃ b ∈ Finset.Icc 1 2024, ∃ c ∈ Finset.Icc 1 3, ∃ d ∈ Finset.Icc 1 2024,
      ({T | T ∈ S ∧ T (a, b) < T (c, d)}.ncard  / S.ncard : ℚ) ∈ Set.Icc (1/3) (2/3))
    ↔ putnam_2024_a3_solution := by
Problem: putnam_2024_a4
Category: number_theory

Find all primes $p > 5$ for which there exists an integer $a$ and an integer $r$ satisfying $1 \le r \le p - 1$ with the following property:
the sequence $1, a, a^2, ..., a^{p-5}$ can be rearranged to form a sequence $b_0, ..., b_{p-5}$ such that $b_n - b_{n-1} - r$ is divisible by $p$ for $1 \le n \le p - 5$.

Solution: Show that the only such prime is 7.

Lean 4 formalization:
import Mathlib

noncomputable abbrev putnam_2024_a4_solution : Set ℕ := sorry
theorem putnam_2024_a4 :
    {p : ℕ | p.Prime ∧ 5 < p ∧ ∃ a r : ℤ, 1 ≤ r ∧ r ≤ p - 1 ∧
      ∃ e : ℕ → ℕ, Set.BijOn e (Set.Icc 0 (p - 5 : ℕ)) (Set.Icc 0 (p - 5 : ℕ)) ∧
        ∀ n, 1 ≤ n ∧ n ≤ (p - 5 : ℕ) →
          (p : ℤ) ∣ a ^ (e n : ℕ) - a ^ (e (n - 1) : ℕ) - r} =
    putnam_2024_a4_solution := by
Problem: putnam_2024_a5
Category: geometry, probability

Consider a circle $\Omega$ with radius $9$ and center at the origin $(0, 0)$ and a disk $\Delta$ with radius $1$ and center at $(r, 0)$ where $0 \le r \le 8$. Two points $P$ and $Q$ are chosen independently and uniformly at random
on $\Omega$. Which value(s) of $r$ minimize the probability that the chord $\overline{PQ}$ intersects $\Delta$?

Solution: Show that the answer is 0.

Lean 4 formalization:
import Mathlib

open MeasureTheory
open scoped ENNReal
open scoped EuclideanGeometry

noncomputable abbrev putnam_2024_a5_solution : Set ℝ := sorry
theorem putnam_2024_a5
    (IsIntersecting : ℝ → EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → Prop)
    (IsIntersecting_def : ∀ r P Q,
      IsIntersecting r P Q ↔ (line[ℝ,P,Q] : Set (EuclideanSpace ℝ (Fin 2)))
      ∩ Metric.sphere ((WithLp.equiv _ _).symm ![r, 0]) 1 ≠ ∅)
    (ProbIntersect : ℝ → ℝ≥0∞)
    (ProbIntersect_def : ∀ r,
      ProbIntersect r = volume {(s, t) : ℝ × ℝ | s ∈ Set.Icc 0 1 ∧ t ∈ Set.Icc 0 1 ∧
        IsIntersecting r
          ((WithLp.equiv _ _).symm ![9 * Real.cos (2 * Real.pi * s), 9 * Real.sin (2 * Real.pi * s)])
          ((WithLp.equiv _ _).symm ![9 * Real.cos (2 * Real.pi * t), 9 * Real.sin (2 * Real.pi * t)]) }) :
    {r | r ∈ Set.Icc 0 8 ∧ ProbIntersect r = ⨅ x ∈ Set.Icc 0 8, ProbIntersect x} =
      putnam_2024_a5_solution := by
Problem: putnam_2024_a6
Category: linear_algebra

Let $c_0, c_1, c_2, ...$ be a sequence defined so that
$$\frac{1 - 3x - \sqrt{1 - 14x + 9x^2}}{4} = \sum_{k=0}^\infty c_k x^k$$
for sufficiently small $x$.
For a positive integer $n$, let $A$ be the $n$-by-$n$ matrix whose
$(i, j)$-entry is $c_{i+j-1}$ for $i$ and $j$ in $\{1, 2, ..., n\}$.
Find the determinant of $A$.

Solution: Show that the determinant is $10^{n * (n-1) / 2)}$.

Lean 4 formalization:
import Mathlib

open scoped Real
open scoped Topology

noncomputable abbrev putnam_2024_a6_solution : ℕ → ℝ := sorry
theorem putnam_2024_a6
    (c : ℕ → ℝ)
    (n : ℕ)
    (h₀ : ∀ᶠ x in 𝓝 0,
      HasSum (fun k => c k * x ^ k) ((1 - 3 * x - √(1 - 14 * x + 9 * x ^ 2)) / 4))
    (h₁ : 0 < n) :
    (Matrix.of fun (i j : Fin n) => c (i + j + 1)).det = putnam_2024_a6_solution n := by
Problem: putnam_2024_b1
Category: combinatorics

Let $n$ and $k$ be positive integers. The square in the $i$th row and
$j$th column of an $n$-by-$n$ grid contains the number $i + j - k$.
For which $n$ and $k$ is it possible to select $n$ squares from the
grid, no two in the same row or column, such that the numbers
contained in the selected squares are exactly $1, ..., n$?

Solution: Show that the only such $n$ and $k$ are of the form $n = 2^l + 1, k = l + 1$ for $l \in \mathbb{N}$.

Lean 4 formalization:
import Mathlib

noncomputable abbrev putnam_2024_b1_solution : Set (ℕ × ℕ) := sorry
theorem putnam_2024_b1
    (grid : (n : ℕ) → ℕ → Fin n → Fin n → ℤ)
    (grid_def : ∀ n k i j, grid n k i j = i.succ + j.succ - k)
    (valid : ℕ → ℕ → Prop)
    (valid_def : ∀ n k, valid n k ↔ 0 < n ∧ 0 < k ∧
      ∃ (f : Fin n → Fin n), f.Injective ∧
        Set.range (fun i => grid n k i (f i)) = Set.Icc (1 : ℤ) n) :
    { (n, k) | valid n k } = putnam_2024_b1_solution := by
Problem: putnam_2024_b3
Category: analysis

Let $r_n$ be the $n$th smallest positive solution to $\tan x = x$ where the argument of tangent is in radians.
Prove that
$$0 < r_{n+1} - r_n - \pi < \frac{1}{(n^2+n)\pi}$$
for $n \geq 1$.


Lean 4 formalization:
import Mathlib

theorem putnam_2024_b3
    (r : ℕ+ → ℝ)
    (r_def : StrictMono r ∧
      (∀ x ∈ Set.Ioo 0 (r 1), Real.tan x ≠ x) ∧ ∀ n,
        0 < r n ∧
        Real.tan (r n) = r n ∧
        ∀ x, x ∈ Set.Ioo (r n) (r (n + 1)) → Real.tan x ≠ x)
    (n : ℕ+) :
    r (n + 1) - r n - Real.pi ∈ Set.Ioo (0 : ℝ) (1 / ((n ^ 2 + n) * Real.pi)) := by
Problem: putnam_2024_b4
Category: probability

Let $n$ be a positive integer. Set $a_{n, 0} = 1$. For $k \geq 0$
choose an integer $m_{n, k}$ uniformly at random from the set
$\{1, 2, \ldots, n\}$, and let
$$a_{n, k+1} = \begin{cases}
a_{n, k} + 1 & \text{if } m_{n, k} > a_{n, k} \\
a_{n, k} & \text{ if } m_{n, k} = a_{n, k} \\
a_{n, k} -1 & \text{if } m_{n, k} < a_{n, k} \end{cases}$$.
Let $E(n)$ be the expected value of $a_{n, n}$. Determine
$\lim_{n \to \infty} E(n)/n$.

Solution: Show that the limit is $\frac{1 - e^{-2}}{2}$.

Lean 4 formalization:
import Mathlib

open MeasureTheory
open scoped ProbabilityTheory
open scoped Topology
open scoped Real

noncomputable abbrev putnam_2024_b4_solution : ℝ := sorry
theorem putnam_2024_b4
    {Ω : Type*}
    [MeasureSpace Ω]
    [IsProbabilityMeasure (ℙ : Measure Ω)]
    (m a : ℕ → ℕ → Ω → ℤ)
    (h₀ : ∀ n > 0, a n 0 = 1)
    (h₁ : ∀ n k, 0 < n → pdf.IsUniform (m n k) (Set.Icc 1 n) ℙ (ProbabilityTheory.uniformOn <| Set.Icc 1 n))
    (h₂ : ∀ n k ω, 0 < n →
      a n (k + 1) ω =
        if m n k ω > a n k ω then
          a n k ω + 1
        else if m n k ω = a n k ω then
          a n k ω
        else
          a n k ω - 1)
    (h₃ : ProbabilityTheory.iIndepFun m.uncurry ℙ) :
    Filter.Tendsto (fun n => (∫ ω, a n n ω : ℝ) / n) Filter.atTop (𝓝 putnam_2024_b4_solution) := by
Problem: putnam_2024_b5
Category: combinatorics, algebra

Let $k$ and $m$ be positive integers. For a positive integer $n$, let $f(n)$ be the number of integer sequences $x_1, ..., x_k, y_1, ..., y_m, z$ satisfying $1 \leq x_1 \leq ... \leq x_k \leq z \leq n$
and $1 \leq y_1 \leq ... \leq y_m \leq z \leq n$. Show that $f(n)$ can be expressed as a polynomial in $n$ with nonnegative coefficients.


Lean 4 formalization:
import Mathlib

open Polynomial

theorem putnam_2024_b5
    (IsQualifyingSeq : {q : ℕ} → (Fin q → ℕ) → ℕ → Prop)
    (IsQualifyingSeq_def : ∀ q w z, ∀ [NeZero q],
      IsQualifyingSeq w z ↔ Monotone w ∧ 1 ≤ w 0 ∧ w (-1 : Fin q) ≤ z)
    (k m : ℕ) [NeZero k] [NeZero m]
    (f : ℕ → ℕ)
    (f_def : ∀ n,
      f n = {(x, y, z) : (Fin k → ℕ) × (Fin m → ℕ) × ℕ |
        IsQualifyingSeq x z ∧ IsQualifyingSeq y z ∧ z ≤ n}.ncard) :
    ∃ P : ℚ[X],
      (∀ n > 0, f n = P.eval (n : ℚ)) ∧
      (∀ i, 0 ≤ P.coeff i) := by
Problem: putnam_2024_b6
Category: analysis

For a real number $a$, let $F_a(x) = \sum_{n\geq 1} n^a e^{2n}x^{n^2}$ for $0 \leq x < 1$.
Find a real number $c$ such that $\lim_{x \to 1^-} F_a(x)e^{-1/(1-x)} = 0$ for all $a < c$, and $\lim_{x \to 1^-} F_a(x)e^{-1/(1-x)} = \infty$ for all $a > c$.

Solution: Show that the solution is $-1/2$.

Lean 4 formalization:
import Mathlib

open scoped Real
open scoped Topology

noncomputable abbrev putnam_2024_b6_solution : ℝ := sorry
theorem putnam_2024_b6
    (F : ℝ → ℝ → ℝ) (c : ℝ)
    (hF : ∀ a, ∀ x ∈ Set.Ico 0 1,
      HasSum (fun (n : ℕ) => (n+1)^a * rexp (2*(n+1)) * x^(n+1)^2) (F a x)) :
    ((∀ a < c, Filter.Tendsto (fun x => F a x * rexp (- 1 / (1-x))) (𝓝[<] 1) (𝓝 0)) ∧
    (∀ a > c, Filter.Tendsto (fun x => F a x * rexp (- 1 / (1-x))) (𝓝[<] 1) Filter.atTop))
    ↔ c = putnam_2024_b6_solution := by
Problem: putnam_2025_a1
Category: number_theory

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$.


Lean 4 formalization:
import Mathlib

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 := by
Problem: putnam_2025_a2
Category: analysis

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]$.

Solution: Show that the optimal constants are $a = \tfrac{1}{\pi}$ and $b = \tfrac{4}{\pi^2}$.

Lean 4 formalization:
import Mathlib

open Real

noncomputable abbrev putnam_2025_a2_solution : ℝ × ℝ := sorry

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) := by
Problem: putnam_2025_a3
Category: combinatorics

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.

Solution: Show that Bob has a winning strategy for all $n \ge 1$.

Lean 4 formalization:
import Mathlib

open Finset Function

abbrev putnam_2025_a3_solution : ℕ → Prop := sorry

def GameString (n : ℕ) := Fin n → Fin 3

def initialState (n : ℕ) : GameString n := fun _ => 0

def 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)

def 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

def AliceHasWinningStrategy (n : ℕ) : Prop := HasWinningStrategy n []

theorem putnam_2025_a3 (n : ℕ) (hn : 1 ≤ n) :
    putnam_2025_a3_solution n ↔ AliceHasWinningStrategy n := by
Problem: putnam_2025_a4
Category: linear_algebra

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\}$.

Solution: Show that the minimal value is $3$.

Lean 4 formalization:
import Mathlib

abbrev putnam_2025_a4_solution : ℕ := sorry

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 := by
Problem: putnam_2025_a5
Category: combinatorics

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.

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$.

Lean 4 formalization:
import Mathlib

open Finset

abbrev putnam_2025_a5_solution : (n : ℕ) → Set (Fin n → ℤˣ) := sorry

def f (n : ℕ) (s : Fin n → ℤˣ) : ℕ :=
  Finset.card {σ : Equiv.Perm (Fin (n + 1)) |
    ∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))}

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
Problem: putnam_2025_a6
Category: number_theory

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}$.


Lean 4 formalization:
import Mathlib

def b : ℕ → ℤ
| 0 => 0
| n + 1 => 2 * (b n) ^ 2 + b n + 1

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
Problem: putnam_2025_b1
Category: geometry, combinatorics

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.

Solution: Show that all points of the plane must have the same color.

Lean 4 formalization:
import Mathlib

open Affine EuclideanGeometry

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