ChristianZ97/putnambench-satp-v4.27 huggingface dataset:
Problem: putnam_2012_a3
Category: analysis, algebra

Let $f: [-1, 1] \to \mathbb{R}$ be a continuous function such that
\begin{itemize}
\item[(i)]
$f(x) = \frac{2-x^2}{2} f \left( \frac{x^2}{2-x^2} \right)$ for every $x$ in $[-1, 1]$,
\item[(ii)]
$f(0) = 1$, and
\item[(iii)]
$\lim_{x \to 1^-} \frac{f(x)}{\sqrt{1-x}}$ exists and is finite.
\end{itemize}
Prove that $f$ is unique, and express $f(x)$ in closed form.

Solution: $f(x) = \sqrt{1-x^2}$ for all $x \in [-1,1]$.

Lean 4 formalization:
import Mathlib

open Matrix Function

noncomputable abbrev putnam_2012_a3_solution : ℝ → ℝ := sorry
theorem putnam_2012_a3
(S : Set ℝ)
(hS : S = Set.Icc (-1 : ℝ) 1)
(fsat : (ℝ → ℝ) → Prop)
(hfsat : fsat = fun f : ℝ → ℝ => ContinuousOn f S ∧
(∀ x ∈ S, f x = ((2 - x^2)/2)*f (x^2/(2 - x^2))) ∧ f 0 = 1 ∧
(∃ y : ℝ, leftLim (fun x : ℝ => (f x)/Real.sqrt (1 - x)) 1 = y))
: fsat putnam_2012_a3_solution ∧ ∀ f : ℝ → ℝ, fsat f → ∀ x ∈ S, f x = putnam_2012_a3_solution x := by
Problem: putnam_2012_a4
Category: algebra

Let $q$ and $r$ be integers with $q>0$, and let $A$ and $B$ be intervals on the real line. Let $T$ be the set of all $b+mq$ where $b$ and $m$ are integers with $b$ in $B$, and let $S$ be the set of all integers $a$ in $A$ such that $ra$ is in $T$. Show that if the product of the lengths of $A$ and $B$ is less than $q$, then $S$ is the intersection of $A$ with some arithmetic progression.


Lean 4 formalization:
import Mathlib

open Matrix Function

theorem putnam_2012_a4
    (IsFiniteAP : Set ℤ → Prop)
    (IsFiniteAP_def : ∀ s,
      IsFiniteAP s ↔ ∃ n : ℕ, ∃ a d : ℤ, 0 < d ∧ s = {a + i * d | i : Fin n})
    (q r : ℤ)
    (A B : Fin 2 → ℝ)
    (T : Set ℤ)
    (S : Set ℤ)
    (qpos : q > 0)
    (ABlt : A 0 < A 1 ∧ B 0 < B 1)
    (hT : T = {x : ℤ | ∃ b m : ℤ, (b : ℝ) ∈ Set.Icc (B 0) (B 1) ∧ x = b + m * q})
    (hS : S = {a : ℤ | (a : ℝ) ∈ Set.Icc (A 0) (A 1) ∧ r * a ∈ T})
    (prod_lt : (A 1 - A 0) * (B 1 - B 0) < q) :
    IsFiniteAP {x | x ∈ S ∧ (x : ℝ) ∈ Set.Icc (A 0) (A 1)} := by
Problem: putnam_2012_a5
Category: linear_algebra

Let $\FF_p$ denote the field of integers modulo a prime $p$, and let $n$ be a positive integer. Let $v$ be a fixed vector in $\FF_p^n$, let $M$ be an $n \times n$ matrix with entries of $\FF_p$, and define $G: \FF_p^n \to \FF_p^n$ by $G(x) = v + Mx$. Let $G^{(k)}$ denote the $k$-fold composition of $G$ with itself, that is, $G^{(1)}(x) = G(x)$ and $G^{(k+1)}(x) = G(G^{(k)}(x))$. Determine all pairs $p, n$ for which there exist $v$ and $M$ such that the $p^n$ vectors $G^{(k)}(0)$, $k=1,2,\dots,p^n$ are distinct.

Solution: Show that the solution is the pairs $(p,n)$ with $n = 1$ as well as the single pair $(2,2)$.

Lean 4 formalization:
import Mathlib

open Matrix Function

abbrev putnam_2012_a5_solution : Set (ℕ × ℕ) := sorry
theorem putnam_2012_a5
  (n p : ℕ)
  (hn : n > 0)
  (hp : Nat.Prime p)
  {F : Type*} [Field F] [Fintype F]
  (hK : Fintype.card F = p)
  (G : Matrix (Fin n) (Fin n) F → (Fin n → F) → (Fin n → F) → (Fin n → F))
  (hG : ∀ M v x, G M v x = v + mulVec M x) :
  (n, p) ∈ putnam_2012_a5_solution ↔
    ∃ᵉ (M : Matrix (Fin n) (Fin n) F) (v : (Fin n → F)),
      ¬(∃ i j : Finset.range (p^n), i ≠ j ∧ (G M v)^[i + 1] 0 = (G M v)^[j + 1] 0) := by
Problem: putnam_2012_a6
Category: analysis

Let $f(x,y)$ be a continuous, real-valued function on $\mathbb{R}^2$. Suppose that, for every rectangular region $R$ of area $1$, the double integral of $f(x,y)$ over $R$ equals $0$.
Must $f(x,y)$ be identically $0$?

Solution: Prove that $f(x,y)$ must be identically $0$.

Lean 4 formalization:
import Mathlib

open Matrix Function

abbrev putnam_2012_a6_solution : Prop := sorry
theorem putnam_2012_a6
(p : ((ℝ × ℝ) → ℝ) → Prop)
(hp : ∀ f, p f ↔
    Continuous f ∧
    ∀ x1 x2 y1 y2 : ℝ, x2 > x1 → y2 > y1
      → (x2 - x1) * (y2 - y1) = 1 → ∫ x in x1..x2, ∫ y in y1..y2, f (x, y) = 0)
: ((∀ f x y, p f → f (x, y) = 0) ↔ putnam_2012_a6_solution) := by
Problem: putnam_2012_b1
Category: algebra

Let $S$ be a class of functions from $[0, \infty)$ to $[0, \infty)$ that satisfies:
\begin{itemize}
\item[(i)]
The functions $f_1(x) = e^x - 1$ and $f_2(x) = \ln(x+1)$ are in $S$;
\item[(ii)]
If $f(x)$ and $g(x)$ are in $S$, the functions $f(x) + g(x)$ and $f(g(x))$ are in $S$;
\item[(iii)]
If $f(x)$ and $g(x)$ are in $S$ and $f(x) \geq g(x)$ for all $x \geq 0$, then the function
$f(x) - g(x)$ is in $S$.
\end{itemize}
Prove that if $f(x)$ and $g(x)$ are in $S$, then the function $f(x) g(x)$ is also in $S$.


Lean 4 formalization:
import Mathlib

open Matrix Function Real

theorem putnam_2012_b1
(S : Set (Set.Ici (0 : ℝ) → ℝ))
(rngS : ∀ f ∈ S, ∀ x : Set.Ici (0 : ℝ), f x ∈ Set.Ici (0 : ℝ))
(f1 : Set.Ici (0 : ℝ) → ℝ)
(hf1 : f1 = fun (x : Set.Ici (0 : ℝ)) ↦ exp x - 1)
(f2 : Set.Ici (0 : ℝ) → ℝ)
(hf2 : f2 = fun (x : Set.Ici (0 : ℝ)) ↦ Real.log (x + 1))
(hf1mem : f1 ∈ S)
(hf2mem : f2 ∈ S)
(hsum : ∀ f ∈ S, ∀ g ∈ S, (fun x ↦ (f x) + (g x)) ∈ S)
(hcomp : ∀ f ∈ S, ∀ g ∈ S, ∀ gnneg : Set.Ici (0 : ℝ) → Set.Ici (0 : ℝ), ((∀ x : Set.Ici (0 : ℝ), g x = gnneg x) → (fun x ↦ f (gnneg x)) ∈ S))
(hdiff : ∀ f ∈ S, ∀ g ∈ S, (∀ x : Set.Ici (0 : ℝ), f x ≥ g x) → (fun x ↦ (f x) - (g x)) ∈ S)
: (∀ f ∈ S, ∀ g ∈ S, (fun x ↦ (f x) * (g x)) ∈ S) := by
Problem: putnam_2012_b3
Category: combinatorics

A round-robin tournament of $2n$ teams lasted for $2n-1$ days, as follows. On each day, every team played one game against another team, with one team winning and one team losing in each of the $n$ games. Over the course of the tournament, each team played every other team exactly once. Can one necessarily choose one winning team from each day without choosing any team more than once?

Solution: Show that the answer is yes.

Lean 4 formalization:
import Mathlib

open Matrix Function Real

abbrev putnam_2012_b3_solution : Prop := sorry
theorem putnam_2012_b3
(nmatchupsgames nmatchupsall : (n : ℕ) → (Fin (2 * n - 1) → (Fin (2 * n) → Fin (2 * n))) → Prop)
(nmatchupswins nmatchupswinschoices: (n : ℕ) → (Fin (2 * n - 1) → (Fin (2 * n) → Fin (2 * n))) → (Fin (2 * n - 1) → (Fin (2 * n) → Bool)) → Prop)
(hnmatchupsall : ∀ n matchups, nmatchupsall n matchups ↔ ∀ t1 t2, t1 ≠ t2 → (∃ d, matchups d t1 = t2))
(hnmatchupsgames : ∀ n matchups, nmatchupsgames n matchups ↔ ∀ d, ∀ t, matchups d t ≠ t ∧ matchups d (matchups d t) = t)
(hnmatchupswins : ∀ n matchups wins, nmatchupswins n matchups wins ↔ ∀ d t, wins d t = !(wins d (matchups d t)))
(hnmatchupswinschoices : ∀ n matchups wins, nmatchupswinschoices n matchups wins ↔ ∃ choices, (∀ d, wins d (choices d)) ∧ Function.Injective choices) :
  (∀ n ≥ 1, ∀ matchups wins,
    (nmatchupsgames n matchups ∧ nmatchupsall n matchups ∧ nmatchupswins n matchups wins) →
    nmatchupswinschoices n matchups wins)
  ↔ putnam_2012_b3_solution := by
Problem: putnam_2012_b4
Category: analysis

Suppose that $a_0 = 1$ and that $a_{n+1} = a_n + e^{-a_n}$ for $n=0,1,2,\dots$. Does $a_n - \log n$
have a finite limit as $n \to \infty$? (Here $\log n = \log_e n = \ln n$.)

Solution: Prove that the sequence has a finite limit.

Lean 4 formalization:
import Mathlib

open Matrix Function Real Topology Filter

noncomputable abbrev putnam_2012_b4_solution : Prop := sorry
theorem putnam_2012_b4
(a : ℕ → ℝ)
(ha0 : a 0 = 1)
(han : ∀ n : ℕ, a (n + 1) = a n + exp (-a n))
: ((∃ L : ℝ, Tendsto (fun n ↦ a n - Real.log n) atTop (𝓝 L)) ↔ putnam_2012_b4_solution) := by
Problem: putnam_2012_b5
Category: analysis

Prove that, for any two bounded functions $g_1, g_2: \RR \to [1, \infty)$, there exist functions $h_1, h_2: \RR \to \RR$ such that, for every $x \in \RR$, \[ \sup_{s \in \RR} (g_1(s)^x g_2(s))  = \max_{t \in \RR} (x h_1(t) + h_2(t)).\]


Lean 4 formalization:
import Mathlib

open Matrix Function Real Topology Filter

theorem putnam_2012_b5
(g1 g2 : ℝ → ℝ)
(hgim : ∀ x : ℝ, g1 x ≥ 1 ∧ g2 x ≥ 1)
(hgbd : ∃ B1 B2 : ℝ, ∀ x : ℝ, g1 x ≤ B1 ∧ g2 x ≤ B2)
: ∃ h1 h2 : ℝ → ℝ, ∀ x : ℝ, sSup {((g1 s)^x * (g2 s)) | s : ℝ} = sSup {(x * (h1 t) + h2 t) | t : ℝ} := by
Problem: putnam_2012_b6
Category: number_theory

Let $p$ be an odd prime number such that $p \equiv 2 \pmod{3}$. Define a permutation $\pi$ of the residue classes modulo $p$ by $\pi(x) \equiv x^3 \pmod{p}$. Show that $\pi$ is an even permutation if and only if $p \equiv 3 \pmod{4}$.


Lean 4 formalization:
import Mathlib

open Matrix Function Real Topology Filter

theorem putnam_2012_b6
(p : ℕ)
(hpodd : Odd p)
(hpprime : Nat.Prime p)
(hpmod3 : p ≡ 2 [MOD 3])
(P : Equiv.Perm (Fin p))
(hP : ∀ i : Fin p, P i = (i * i * i))
: Equiv.Perm.signAux P = 1 ↔ (p ≡ 3 [MOD 4]) := by
Problem: putnam_2013_a2
Category: number_theory, algebra

Let $S$ be the set of all positive integers that are \emph{not} perfect squares. For $n$ in $S$, consider choices of integers
$a_1, a_2, \dots, a_r$ such that $n < a_1<  a_2 < \cdots < a_r$
and $n \cdot a_1 \cdot a_2 \cdots a_r$ is a perfect square, and
let $f(n)$ be the minumum of $a_r$ over all such choices. For example,
$2 \cdot 3 \cdot 6$ is a perfect square, while $2 \cdot 3$, $2 \cdot 4$,
$2 \cdot 5$, $2 \cdot 3 \cdot 4$, $2 \cdot 3 \cdot 5$, $2 \cdot 4 \cdot 5$, and $2 \cdot 3 \cdot 4 \cdot 5$ are not, and so $f(2) = 6$.
Show that the function $f$ from $S$ to the integers is one-to-one.


Lean 4 formalization:
import Mathlib

open Function Set

theorem putnam_2013_a2
  (S : Set ℤ)
  (hS : S = {n : ℤ | n > 0 ∧ ¬∃ m : ℤ, m ^ 2 = n})
  (P : ℤ → List ℤ → Prop)
  (hP : ∀ n a, P n a ↔
    a.length > 0 ∧ n < a[0]! ∧
    (∃ m : ℤ, m ^ 2 = n * a.prod) ∧
    (∀ i : Fin (a.length - 1), a[i] < a[i+(1:ℕ)]))
  (T : ℤ → Set ℤ)
  (hT : T = fun n : ℤ => {m : ℤ | ∃ a : List ℤ, P n a ∧ a[a.length - 1]! = m})
  (f : ℤ → ℤ)
  (hf : ∀ n ∈ S, ((∃ r ∈ T n, f n = r) ∧ ∀ r ∈ T n, f n ≤ r)) :
  InjOn f S := by
Problem: putnam_2013_a3
Category: analysis

Suppose that the real numbers \( a_0, a_1, \ldots, a_n \) and \( x \), with \( 0 < x < 1 \), satisfy $ \frac{a_0}{1-x} + \frac{a_1}{(1-x)^2} + \cdots + \frac{a_n}{(1-x)^{n+1}} = 0. $ Prove that there exists a real number \( y \) with \( 0 < y < 1 \) such that $ a_0 + a_1y + \cdots + a_ny^n = 0. $.


Lean 4 formalization:
import Mathlib

open Function Set

theorem putnam_2013_a3
(n : ℕ)
(a : Set.Icc 0 n → ℝ)
(x : ℝ)
(hx : 0 < x ∧ x < 1)
(hsum : (∑ i : Set.Icc 0 n, a i / (1 - x ^ (i.1 + 1))) = 0)
: ∃ y : ℝ, 0 < y ∧ y < 1 ∧ (∑ i : Set.Icc 0 n, a i * y ^ i.1) = 0 := by
Problem: putnam_2013_a4
Category: algebra

A finite collection of digits $0$ and $1$ is written around a circle. An \emph{arc} of length $L \geq 0$ consists of $L$ consecutive digits around the circle. For each arc $w$, let $Z(w)$ and $N(w)$ denote the number of $0$'s in $w$ and the number of $1$'s in $w$, respectively. Assume that $|Z(w)-Z(w')| \leq 1$ for any two arcs $w,w'$ of the same length. Suppose that some arcs $w_1,\dots,w_k$ have the property that $Z=\frac{1}{k}\sum_{j=1}^k Z(w_j)$ and $N=\frac{1}{k}\sum_{j=1}^k N(w_j)$ are both integers. Prove that there exists an arc $w$ with $Z(w)=Z$ and $N(w)=N$.


Lean 4 formalization:
import Mathlib

open Function Set

theorem putnam_2013_a4
(n k : ℕ)
(circle : Fin n → Fin 2)
(Z N : Fin n × Fin (n + 1) → ℤ)
(ws : Fin k → Fin n × Fin (n + 1))
(Zsum Nsum : ℤ)
(npos : n ≥ 1) (kpos : k ≥ 1)
(hZ : ∀ w, Z w = ∑ l ∈ {x : Fin n | x.1 < w.2.1}, if (circle (w.1 + l) = 0) then 1 else 0)
(hN : ∀ w, N w = ∑ l ∈ {x : Fin n | x.1 < w.2.1}, if (circle (w.1 + l) = 1) then 1 else 0)
(Zle1 : ∀ w w', w.2 = w'.2 → |(Z w : ℤ) - Z w'| ≤ 1)
(hZsum : Zsum = ((1 : ℝ) / k) * ∑ j : Fin k, Z (ws j))
(hNsum : Nsum = ((1 : ℝ) / k) * ∑ j : Fin k, N (ws j)) :
∃ w, Z w = Zsum ∧ N w = Nsum := by
Problem: putnam_2013_a5
Category: geometry, linear_algebra

For $m \geq 3$, a list of $\binom{m}{3}$ real numbers $a_{ijk}$ ($1 \leq i<j<k \leq m$) is said to be \emph{area definite} for $\mathbb{R}^n$ if the inequality $\sum_{1 \leq i<j<k \leq m} a_{ijk} \cdot \text{Area}(\Delta A_iA_jA_k) \geq 0$ holds for every choice of $m$ points $A_1,\dots,A_m$ in $\mathbb{R}^n$. For example, the list of four numbers $a_{123}=a_{124}=a_{134}=1$, $a_{234}=-1$ is area definite for $\mathbb{R}^2$. Prove that if a list of $\binom{m}{3}$ numbers is area definite for $\mathbb{R}^2$, then it is area definite for $\mathbb{R}^3$.


Lean 4 formalization:
import Mathlib

open Function Set MeasureTheory

theorem putnam_2013_a5
(m : ℕ)
(area2 : (Fin 2 → ℝ) → (Fin 2 → ℝ) → (Fin 2 → ℝ) → ℝ)
(area3 : (Fin 3 → ℝ) → (Fin 3 → ℝ) → (Fin 3 → ℝ) → ℝ)
(areadef2 : (Fin m → Fin m → Fin m → ℝ) → Prop)
(areadef3 : (Fin m → Fin m → Fin m → ℝ) → Prop)
(mge3 : m ≥ 3)
(harea2 : ∀ a b c, area2 a b c = (volume (convexHull ℝ {a, b, c})).toReal)
(harea3 : ∀ a b c, area3 a b c = (μH[2] (convexHull ℝ {a, b, c})).toReal)
(hareadef2 : ∀ a, areadef2 a ↔ ∀ A : Fin m → (Fin 2 → ℝ), (∑ i : Fin m, ∑ j : Fin m, ∑ k : Fin m, if (i < j ∧ j < k) then (a i j k * area2 (A i) (A j) (A k)) else 0) ≥ 0)
(hareadef3 : ∀ a, areadef3 a ↔ ∀ A : Fin m → (Fin 3 → ℝ), (∑ i : Fin m, ∑ j : Fin m, ∑ k : Fin m, if (i < j ∧ j < k) then (a i j k * area3 (A i) (A j) (A k)) else 0) ≥ 0)
: ∀ a, areadef2 a → areadef3 a := by
Problem: putnam_2013_a6
Category: algebra

Define a function $w:\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$ as follows. For $|a|,|b| \leq 2$, let $w(a,b)$ be as in the table shown; otherwise, let $w(a,b)=0$.
\begin{center}
\begin{tabular}{|cc|r|r|r|r|r|}
\hline
\multicolumn{2}{|c|}{\multirow{2}{*}{$w(a,b)$}} & \multicolumn{5}{|c|}{$b$} \\
& & -2 & -1 & 0 & 1 & 2 \\
\hline
& -2 & -1 & -2 & 2 & -2 & -1 \\
& -1 & -2 & 4 & -4 & 4 & -2 \\
$a$ & 0 & 2 & -4 & 12 & -4 & 2 \\
& 1 & -2 & 4 & -4 & 4 & -2 \\
& 2 & -1 & -2 & 2 & -2 & -1 \\
\hline
\end{tabular}
\end{center}
For every finite subset $S$ of $\mathbb{Z} \times \mathbb{Z}$, define $A(S)=\sum_{(\mathbf{s},\mathbf{s}') \in S \times S} w(\mathbf{s}-\mathbf{s}')$. Prove that if $S$ is any finite nonempty subset of $\mathbb{Z} \times \mathbb{Z}$, then $A(S)>0$. (For example, if $S=\{(0,1),(0,2),(2,0),(3,1)\}$, then the terms in $A(S)$ are $12,12,12,12,4,4,0,0,0,0,-1,-1,-2,-2,-4,-4$.)


Lean 4 formalization:
import Mathlib

open Function Set

theorem putnam_2013_a6
  (w : ℤ → ℤ → ℤ)
  (A : Finset (ℤ × ℤ) → ℤ)
  (hwn1 : w (-2) (-2) = -1 ∧ w 2 (-2) = -1 ∧ w (-2) 2 = -1 ∧ w 2 2 = -1)
  (hwn2 : w (-1) (-2) = -2 ∧ w 1 (-2) = -2 ∧ w (-2) (-1) = -2 ∧ w 2 (-1) = -2 ∧ w (-2) 1 = -2 ∧ w 2 1 = -2 ∧ w (-1) 2 = -2 ∧ w 1 2 = -2)
  (hw2 : w 0 (-2) = 2 ∧ w (-2) 0 = 2 ∧ w 2 0 = 2 ∧ w 0 2 = 2)
  (hw4 : w (-1) (-1) = 4 ∧ w 1 (-1) = 4 ∧ w (-1) 1 = 4 ∧ w 1 1 = 4)
  (hwn4 : w 0 (-1) = -4 ∧ w (-1) 0 = -4 ∧ w 1 0 = -4 ∧ w 0 1 = -4)
  (hw12 : w 0 0 = 12)
  (hw0 : ∀ a b : ℤ, (|a| > 2 ∨ |b| > 2) → w a b = 0)
  (hA : ∀ S, A S = ∑ s ∈ S, ∑ s' ∈ S, w (s - s').1 (s - s').2) :
  ∀ S : Finset (ℤ × ℤ), Nonempty S → A S > 0 := by
Problem: putnam_2013_b1
Category: algebra

For positive integers $n$, let the numbers $c(n)$ be determined by the rules $c(1)=1$, $c(2n)=c(n)$, and $c(2n+1)=(-1)^nc(n)$. Find the value of $\sum_{n=1}^{2013} c(n)c(n+2)$.

Solution: Show that the desired sum is $-1$.

Lean 4 formalization:
import Mathlib

open Function Set

abbrev putnam_2013_b1_solution : ℤ := sorry
theorem putnam_2013_b1
(c : ℕ → ℤ)
(hc1 : c 1 = 1)
(hceven : ∀ n : ℕ, n > 0 → c (2 * n) = c n)
(hcodd : ∀ n : ℕ, n > 0 → c (2 * n + 1) = (-1) ^ n * c n)
: (∑ n : Set.Icc 1 2013, c n * c (n.1 + 2)) = putnam_2013_b1_solution := by
Problem: putnam_2013_b2
Category: algebra

Let $C = \bigcup_{N=1}^\infty C_N$, where $C_N$ denotes the set of those `cosine polynomials' of the form
\[
f(x) = 1 + \sum_{n=1}^N a_n \cos(2 \pi n x)
\]
for which:
\begin{enumerate}
\item[(i)]
$f(x) \geq 0$ for all real $x$, and
\item[(ii)]
$a_n = 0$ whenever $n$ is a multiple of $3$.
\end{enumerate}
Determine the maximum value of $f(0)$ as $f$ ranges through $C$, and
prove that this maximum is attained.

Solution: The maximum value of $f(0)$ is $3$.

Lean 4 formalization:
import Mathlib

open Function Set

abbrev putnam_2013_b2_solution : ℝ := sorry
theorem putnam_2013_b2
  (CN : ℕ → Set (ℝ → ℝ))
  (hCN : ∀ N : ℕ, CN N =
    {f : ℝ → ℝ |
      (∀ x : ℝ, f x ≥ 0) ∧
      ∃ a : List ℝ, a.length = N + 1 ∧ (∀ n : Fin (N + 1), 3 ∣ (n : ℕ) → a[n]! = 0) ∧
      ∀ x : ℝ, f x = 1 + ∑ n ∈ Finset.Icc 1 N, a[(n : ℕ)]! * Real.cos (2*Real.pi*n*x)}) :
  IsGreatest {f 0 | f ∈ ⋃ N ∈ Ici 1, CN N} putnam_2013_b2_solution := by
Problem: putnam_2013_b3
Category: set_theory

Let $\mathcal{P}$ be a nonempty collection of subsets of $\{1,\dots, n\}$ such that: \begin{enumerate} \item[(i)] if $S, S' \in \mathcal{P}$, then $S \cup S' \in \mathcal{P}$ and $S \cap S' \in \mathcal{P}$, and \item[(ii)] if $S \in \mathcal{P}$ and $S \neq \emptyset$, then there is a subset $T \subset S$ such that $T \in \mathcal{P}$ and $T$ contains exactly one fewer element than $S$. \end{enumerate} Suppose that $f: \mathcal{P} \to \mathbb{R}$ is a function such that $f(\emptyset) = 0$ and \[f(S \cup S') = f(S) + f(S') - f(S \cap S') \mbox{ for all $S,S' \in \mathcal{P}$.} \] Must there exist real numbers $f_1,\dots,f_n$ such that\[f(S) = \sum_{i \in S} f_i\] \n for every $S \in \mathcal{P}$?


Lean 4 formalization:
import Mathlib

open Function Set

abbrev putnam_2013_b3_solution : Prop := sorry
theorem putnam_2013_b3
: (∀ (n : ℕ) (P : Finset (Finset (Fin n))) (f : Finset (Fin n) → ℝ),
      P ≠ ⊥ → (∀ S ∈ P, ∀ S' ∈ P, S ∪ S' ∈ P ∧ S ∩ S' ∈ P) →
      (∀ S ∈ P, S ≠ ⊥ → ∃ T ∈ P, T ⊂ S ∧ Finset.card T + 1 = Finset.card S) →
      f ⊥ = 0 → (∀ S ∈ P, ∀ S' ∈ P, f (S ∪ S') = f S + f S' - f (S ∩ S')) →
      ∃ r : Fin n → ℝ, ∀ S ∈ P, f S = ∑ i ∈ S, r i)
      ↔ putnam_2013_b3_solution := by
Problem: putnam_2013_b4
Category: analysis

For any continuous real-valued function $f$ defined on the interval $[0,1]$, let $\mu(f)=\int_0^1 f(x)\,dx,\text{Var}(f)=\int_0^1 (f(x)-\mu(f))^2\,dx,M(f)=\max_{0 \leq x \leq 1} |f(x)|$. Show that if $f$ and $g$ are continuous real-valued functions defined on the interval $[0,1]$, then $\text{Var}(fg) \leq 2\text{Var}(f)M(g)^2+2\text{Var}(g)M(f)^2$.


Lean 4 formalization:
import Mathlib

open Function Set

theorem putnam_2013_b4
    (μ Var M : C(Icc (0 : ℝ) 1, ℝ) → ℝ)
    (hμ : ∀ f, μ f = ∫ x, f x)
    (hVar : ∀ f, Var f = ∫ x, (f x - μ f) ^ 2)
    (hM : ∀ f : C(Icc (0 : ℝ) 1, ℝ), IsGreatest (range <| abs ∘ f) (M f))
    (f g : C(Icc (0 : ℝ) 1, ℝ)) :
    Var (f * g) ≤ 2 * Var f * (M g) ^ 2 + 2 * Var g * (M f) ^ 2 := by
Problem: putnam_2013_b5
Category: algebra

Let $X=\{1,2,\dots,n\}$, and let $k \in X$. Show that there are exactly $k \cdot n^{n-1}$ functions $f:X \to X$ such that for every $x \in X$ there is a $j \geq 0$ such that $f^{(j)}(x) \leq k$. [Here $f^{(j)}$ denotes the $j$\textsuperscript{th} iterate of $f$, so that $f^{(0)}(x)=x$ and $f^{(j+1)}(x)=f(f^{(j)}(x))$.]


Lean 4 formalization:
import Mathlib

open Function Set

theorem putnam_2013_b5
  (n : ℕ) (hn : n ≥ 1)
  (k : Set.Icc 1 n)
  (fiter : (Set.Icc 1 n → Set.Icc 1 n) → Prop)
  (hfiter : ∀ f, fiter f ↔ ∀ x : Set.Icc 1 n, ∃ j : ℕ, f^[j] x ≤ k) :
  {f | fiter f}.encard = k * n ^ (n - 1) := by
Problem: putnam_2014_a1
Category: analysis, number_theory

Prove that every nonzero coefficient of the Taylor series of \[(1 - x + x^2)e^x\] about $x=0$ is a rational number whose numerator (in lowest terms) is either $1$ or a prime number.


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_2014_a1
(f : ℝ → ℝ)
(hf : ∀ x : ℝ, f x = (1 - x + x ^ 2) * Real.exp x)
(hfdiff : ContDiff ℝ ⊤ f)
(c : ℕ → ℝ)
(hc : ∀ k : ℕ, c k = taylorCoeffWithin f k Set.univ 0)
: ∀ k : ℕ, c k ≠ 0 → ∃ q : ℚ, c k = q ∧ (q.num = 1 ∨ Prime q.num.natAbs) := by
Problem: putnam_2014_a2
Category: linear_algebra

Let $A$ be the $n \times n$ matrix whose entry in the $i$-th row and $j$-th column is $\frac{1}{\min(i,j)}$ for $1 \leq i,j \leq n$. Compute $\det(A)$.

Solution: Show that the determinant is $\frac{(-1)^{n-1}}{(n-1)!n!}$.

Lean 4 formalization:
import Mathlib

open Topology Filter Nat

abbrev putnam_2014_a2_solution : ℕ → ℝ := sorry
theorem putnam_2014_a2
(n : ℕ)
(A : Matrix (Fin n) (Fin n) ℝ)
(npos : n > 0)
(hA : ∀ i j : Fin n, A i j = 1 / min (i.1 + 1 : ℚ) (j.1 + 1))
: A.det = putnam_2014_a2_solution n := by
Problem: putnam_2014_a3
Category: algebra

Let \( a_0 = \frac{5}{2} \) and \( a_k = a_{k-1}^2 - 2 \) for \( k \geq 1 \). Compute \( \prod_{k=0}^{\infty} \left(1 - \frac{1}{a_k}\right) \) in closed form.

Solution: Show that the solution is 3/7.

Lean 4 formalization:
import Mathlib

open Topology Filter Nat

noncomputable abbrev putnam_2014_a3_solution : ℝ := sorry
theorem putnam_2014_a3
(a : ℕ → ℝ)
(a0 : a 0 = 5 / 2)
(ak : ∀ k ≥ 1, a k = (a (k - 1)) ^ 2 - 2)
: Tendsto (fun n : ℕ => ∏ k ∈ Finset.range n, (1 - 1 / a k)) atTop (𝓝 putnam_2014_a3_solution) := by
Problem: putnam_2014_a4
Category: probability, analysis

Suppose $X$ is a random variable that takes on only nonnegative integer values, with $E\left[X\right]=1$, $E\left[X^2\right]=2$, and $E\left[X^3\right]=5$. (Here $E\left[Y\right]$ denotes the expectation of the random variable $Y$.) Determine the smallest possible value of the probability of the event $X=0$.

Solution: Show that the answer is $\frac{1}{3}$.

Lean 4 formalization:
import Mathlib

open Topology Filter Nat

noncomputable abbrev putnam_2014_a4_solution : ℝ := sorry
theorem putnam_2014_a4
(Xrandvar : (ℕ → ℝ) → Prop)
(hXrandvar : Xrandvar = (fun X : ℕ → ℝ => (∀ n : ℕ, X n ∈ Set.Icc 0 1) ∧ ∑' n : ℕ, X n = 1))
(E : (ℕ → ℝ) → (ℕ → ℝ) → ℝ)
(hE : E = (fun (X : ℕ → ℝ) (f : ℕ → ℝ) => ∑' n : ℕ, f n * X n))
: sInf {X0 : ℝ | ∃ X : ℕ → ℝ, Xrandvar X ∧ E X (fun x : ℕ => x) = 1 ∧ E X (fun x : ℕ => x ^ 2) = 2 ∧ E X (fun x : ℕ => x ^ 3) = 5 ∧ X0 = X 0} = putnam_2014_a4_solution := by
Problem: putnam_2014_a5
Category: algebra

Let \[ P_n(x) = 1 + 2 x  + 3 x^2 + \cdots + n x^{n-1}.\] Prove that the polynomials $P_j(x)$ and $P_k(x)$ are relatively prime for all positive integers $j$ and $k$ with $j \neq k$.


Lean 4 formalization:
import Mathlib

open Topology Filter Nat

theorem putnam_2014_a5
(P : ℕ → Polynomial ℂ)
(hP : ∀ n, P n = ∑ i ∈ Finset.Icc 1 n, i * Polynomial.X ^ (i - 1))
: ∀ (j k : ℕ), (j > 0 ∧ k > 0) → j ≠ k → IsCoprime (P j) (P k) := by
Problem: putnam_2014_a6
Category: linear_algebra

Let \( n \) be a positive integer. What is the largest \( k \) for which there exist \( n \times n \) matrices \( M_1, \ldots, M_k \) and \( N_1, \ldots, N_k \) with real entries such that for all \( i \) and \( j \), the matrix product \( M_i N_j \) has a zero entry somewhere on its diagonal if and only if \( i \neq j \)?

Solution: Show that the solution has the form k \<= n ^ n.

Lean 4 formalization:
import Mathlib

open Topology Filter Nat

abbrev putnam_2014_a6_solution : ℕ → ℕ := sorry
theorem putnam_2014_a6
(n : ℕ)
(kex : ℕ → Prop)
(npos : n > 0)
(hkex : ∀ k ≥ 1, kex k = ∃ M N : Fin k → Matrix (Fin n) (Fin n) ℝ, ∀ i j : Fin k, ((∃ p : Fin n, (M i * N j) p p = 0) ↔ i ≠ j))
: (putnam_2014_a6_solution n ≥ 1 ∧ kex (putnam_2014_a6_solution n)) ∧ (∀ k ≥ 1, kex k → k ≤ putnam_2014_a6_solution n) := by
Problem: putnam_2014_b1
Category: algebra

A \emph{base $10$ over-expansion} of a positive integer $N$ is an expression of the form
\[
N = d_k 10^k + d_{k-1} 10^{k-1} + \cdots + d_0 10^0
\]
with $d_k \neq 0$ and $d_i \in \{0,1,2,\dots,10\}$ for all $i$. For instance, the integer $N = 10$ has two base $10$ over-expansions: $10 = 10 \cdot 10^0$ and the usual base $10$ expansion $10 = 1 \cdot 10^1 + 0 \cdot 10^0$. Which positive integers have a unique base $10$ over-expansion?

Solution: Prove that the answer is the integers with no $0$'s in their usual base $10$ expansion.

Lean 4 formalization:
import Mathlib

open Topology Filter Nat

abbrev putnam_2014_b1_solution : Set ℕ := sorry
theorem putnam_2014_b1
(overexpansion : ℕ → List ℕ → Prop)
(hoverexpansion : overexpansion = fun N d ↦ N = ∑ i : Fin d.length, (d.get i) * 10 ^ i.1 ∧ d.getLastI ≠ 0 ∧ ∀ a ∈ d, a ∈ Finset.range 11)
(S : Set ℕ)
(hS : ∀ N : ℕ, N ∈ S ↔ N > 0 ∧ ∃! d : List ℕ, overexpansion N d)
: (S = putnam_2014_b1_solution) := by