ChristianZ97/putnambench-satp-v4.27 huggingface dataset:
Problem: putnam_2020_b4
Category: algebra

Let $n$ be a positive integer, and let $V_n$ be the set of integer $(2n+1)$-tuples $\mathbf{v} = (s_0, s_1, \cdots, s_{2n-1}, s_{2n})$ for which $s_0 = s_{2n} = 0$ and $|s_j - s_{j-1}| = 1$ for $j=1,2,\cdots,2n$. Define \[ q(\mathbf{v}) = 1 + \sum_{j=1}^{2n-1} 3^{s_j}, \] and let $M(n)$ be the average of $\frac{1}{q(\mathbf{v})}$ over all $\mathbf{v} \in V_n$. Evaluate $M(2020)$.

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

Lean 4 formalization:
import Mathlib

open Filter Topology Set

noncomputable abbrev putnam_2020_b4_solution : ℝ := sorry
theorem putnam_2020_b4
(V : ℕ → Set (ℕ → ℤ))
(q : ℕ → (ℕ → ℤ) → ℝ)
(M : ℕ → ℝ)
(hV : V = fun n ↦ ({s : ℕ → ℤ | s 0 = 0 ∧ (∀ j ≥ 2 * n, s j = 0) ∧ (∀ j ∈ Icc 1 (2 * n), |s j - s (j - 1)| = 1)}))
(hq : q = fun n s ↦ 1 + ∑ j ∈ Finset.Icc 1 (2 * n - 1), 3 ^ (s j))
(hM : M = fun n ↦ (∑' v : V n, 1 / (q n v)) / (V n).ncard)
: (M 2020 = putnam_2020_b4_solution) := by
Problem: putnam_2020_b5
Category: algebra

For $j \in \{1, 2, 3, 4\}$, let $z_j$ be a complex number with $|z_j| = 1$ and $z_j \neq 1$. Prove that \[ 3 - z_1 - z_2 - z_3 - z_4 + z_1 z_2 z_3 z_4 \neq 0. \]


Lean 4 formalization:
import Mathlib

open Filter Topology Set

theorem putnam_2020_b5
(z : Fin 4 → ℂ)
(hzle1 : ∀ n, ‖z n‖ = 1)
(hzne1 : ∀ n, z n ≠ 1)
: 3 - z 0 - z 1 - z 2 - z 3 + (z 0) * (z 1) * (z 2) * (z 3) ≠ 0:= by
Problem: putnam_2020_b6
Category: algebra

Let $n$ be a positive integer. Prove that $\sum_{k=1}^n(-1)^{\lfloor k(\sqrt{2}-1) \rfloor} \geq 0$.


Lean 4 formalization:
import Mathlib

open Filter Topology Set

theorem putnam_2020_b6
(n : ℕ)
(npos : n > 0)
: ∑ k ∈ Finset.Icc 1 n, ((-1) ^ Int.floor (k * (Real.sqrt 2 - 1)) : ℝ) ≥ 0 := by
Problem: putnam_2021_a1
Category: geometry

A grasshopper starts at the origin in the coordinate plane and makes a sequence of hops.
Each hop has length $5$, and after each hop the grasshopper is at a point whose coordinates are both integers; thus, there are $12$ possible locations for the grasshopper after the first hop.
What is the smallest number of hops needed for the grasshopper to reach the point $(2021, 2021)$?

Solution: The answer is $578$.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_2021_a1_solution : ℕ := sorry
theorem putnam_2021_a1
    (P : List (ℤ × ℤ) → Prop)
    (P_def : ∀ l, P l ↔ l.Chain' fun p q ↦ (p.1 - q.1) ^ 2 + (p.2 - q.2) ^ 2 = 25) :
    IsLeast
      {k | ∃ l, P ((0, 0) :: l) ∧ l.getLast! = (2021, 2021) ∧ l.length = k}
      putnam_2021_a1_solution := by
Problem: putnam_2021_a2
Category: analysis

For every positive real number $x$, let $g(x)=\lim_{r \to 0}((x+1)^{r+1}-x^{r+1})^\frac{1}{r}$. Find $\lim_{x \to \infty}\frac{g(x)}{x}$.

Solution: Show that the limit is $e$.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_2021_a2_solution : ℝ := sorry
theorem putnam_2021_a2
(g : ℝ → ℝ)
(hg : ∀ x > 0, Tendsto (fun r : ℝ => ((x + 1) ^ (r + 1) - x ^ (r + 1)) ^ (1 / r)) (𝓝[>] 0) (𝓝 (g x)))
: Tendsto (fun x : ℝ => g x / x) atTop (𝓝 putnam_2021_a2_solution) := by
Problem: putnam_2021_a3
Category: geometry

Determine all positive integers $N$ for which the sphere $x^2+y^2+z^2=N$ has an inscribed regular tetrahedron whose vertices have integer coordinates.

Solution: Show that the integers $N$ with this property are those of the form $3m^2$ for some positive integer $m$.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_2021_a3_solution : Set ℕ := sorry
theorem putnam_2021_a3
  (N : ℕ)
  (Nsphere : Set (EuclideanSpace ℝ (Fin 3)))
  (hNsphere : Nsphere = {p | (p 0) ^ 2 + (p 1) ^ 2 + (p 2) ^ 2 = (N : ℝ)})
  (intcoords : (EuclideanSpace ℝ (Fin 3)) → Prop)
  (intcoords_def : ∀ p, intcoords p ↔ ∀ i : Fin 3, p i = round (p i)) :
  (0 < N ∧ ∃ A B C D : EuclideanSpace ℝ (Fin 3),
    A ∈ Nsphere ∧ B ∈ Nsphere ∧ C ∈ Nsphere ∧ D ∈ Nsphere ∧
    intcoords A ∧ intcoords B ∧ intcoords C ∧ intcoords D ∧
    (∃ s > 0, dist A B = s ∧ dist A C = s ∧ dist A D = s ∧ dist B C = s ∧ dist B D = s ∧ dist C D = s))
  ↔ N ∈ putnam_2021_a3_solution := by
Problem: putnam_2021_a4
Category: analysis

Let
\[
I(R) = \iint_{x^2+y^2 \leq R^2} \left( \frac{1+2x^2}{1+x^4+6x^2y^2+y^4} - \frac{1+y^2}{2+x^4+y^4} \right)\,dx\,dy.
\]
Find
\[
\lim_{R \to \infty} I(R),
\]
or show that this limit does not exist.

Solution: The limit exists and equals $\frac{\sqrt{2}}{2} \pi \log 2$.

Lean 4 formalization:
import Mathlib

open Filter Topology Metric

noncomputable abbrev putnam_2021_a4_solution : ℝ := sorry
theorem putnam_2021_a4
  (S : ℝ → Set (EuclideanSpace ℝ (Fin 2)))
  (hS : S = fun R => ball (0 : EuclideanSpace ℝ (Fin 2)) R)
  (I : ℝ → ℝ)
  (hI : I = fun R => ∫ p in S R,
    (1 + 2*(p 0)^2)/(1 + (p 0)^4 + 6*(p 0)^2*(p 1)^2 + (p 1)^4) - (1 + (p 1)^2)/(2 + (p 0)^4 + (p 1)^4)) :
  Tendsto I atTop (𝓝 putnam_2021_a4_solution) := by
Problem: putnam_2021_a5
Category: number_theory

Let $A$ be the set of all integers $n$ such that $1 \leq n \leq 2021$ and $\gcd(n,2021)=1$. For every nonnegative integer $j$, let $S(j)=\sum_{n \in A}n^j$. Determine all values of $j$ such that $S(j)$ is a multiple of $2021$.

Solution: Show that the values of $j$ in question are those not divisible by either $42$ or $46$.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_2021_a5_solution : Set ℕ := sorry
theorem putnam_2021_a5
  (j : ℕ)
  (A : Finset ℕ)
  (S : ℕ → ℕ)
  (hA : A = {n | 1 ≤ n ∧ n ≤ 2021 ∧ Nat.gcd n 2021 = 1})
  (hS : ∀ j' : ℕ, S j' = ∑ n ∈ A, n ^ j') :
  (2021 ∣ S j) ↔ j ∈ putnam_2021_a5_solution := by
Problem: putnam_2021_a6
Category: number_theory, algebra

Let $P(x)$ be a polynomial whose coefficients are all either $0$ or $1$. Suppose that $P(x)$ can be written as a product of two nonconstant polynomials with integer coefficients. Does it follow that $P(2)$ is a composite integer?

Solution: Show that it does follow that $P(2)$ is a composite integer.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_2021_a6_solution : Prop := sorry
theorem putnam_2021_a6 :
  (∀ P, (∀ n : ℕ, P.coeff n = 0 ∨ P.coeff n = 1) →
    (∃ Q R : Polynomial ℤ, Q.degree > 0 ∧ R.degree > 0 ∧ P = Q * R) →
    (P.eval 2 ≠ 0 ∧ P.eval 2 ≠ 1 ∧ ¬Prime (P.eval 2)))
  ↔ putnam_2021_a6_solution := by
Problem: putnam_2021_b2
Category: analysis

Determine the maximum value of the sum $S = \sum_{n=1}^\infty \frac{n}{2^n}(a_1a_2 \dots a_n)^{1/n}$ over all sequences $a_1,a_2,a_3,\dots$ of nonnegative real numbers satisfying $\sum_{k=1}^\infty a_k=1$.

Solution: Show that the answer is $2/3$.

Lean 4 formalization:
import Mathlib

open Filter Topology

noncomputable abbrev putnam_2021_b2_solution : ℝ := sorry
theorem putnam_2021_b2 :
    IsGreatest
      {S | ∃ a : ℕ+ → ℝ, (∑' k, a k = 1) ∧ (∀ k, 0 ≤ a k) ∧
        S = ∑' n : ℕ+, n / 2 ^ (n : ℕ) * (∏ k ∈ Finset.Icc 1 n, a k) ^ (1 / n : ℝ)}
      putnam_2021_b2_solution := by
Problem: putnam_2021_b3
Category: analysis

Let $h(x,y)$ be a real-valued function that is twice continuously differentiable throughout $\mathbb{R}^2$, and define $\rho(x,y)=yh_x-xh_y$. Prove or disprove: For any positive constants $d$ and $r$ with $d>r$, there is a circle $\mathcal{S}$ of radius $r$ whose center is a distance $d$ away from the origin such that the integral of $\rho$ over the interior of $\mathcal{S}$ is zero.

Solution: Show that the given statement is true.

Lean 4 formalization:
import Mathlib

open Filter Topology Metric

abbrev putnam_2021_b3_solution : Prop := sorry
theorem putnam_2021_b3
  (rho : ((EuclideanSpace ℝ (Fin 2)) → ℝ) → (EuclideanSpace ℝ (Fin 2)) → ℝ)
  (rho_def : ∀ (h : (EuclideanSpace ℝ (Fin 2)) → ℝ) (p : EuclideanSpace ℝ (Fin 2)),
    rho h p = (p 1) *
      deriv (fun x' : ℝ => h !₂[x', p 1]) (p 0)
      - (p 0) * deriv (fun y' : ℝ => h !₂[p 0, y']) (p 1)) :
  (∀ h : (EuclideanSpace ℝ (Fin 2)) → ℝ, ContDiff ℝ 2 h →
    (∀ d > 0, ∀ r > 0, d > r → (∃ c : EuclideanSpace ℝ (Fin 2), dist c 0 = d ∧ (∫ p in (ball c r), rho h p) = 0)))
  ↔ putnam_2021_b3_solution := by
Problem: putnam_2021_b4
Category: number_theory

Let $F_0, F_1, \ldots$ be the sequence of Fibonacci numbers, with $F_0 = 0$, $F_1 = 1$, and $F_n = F_{n-1} + F_{n-2}$ for $n \geq 2$. For $m > 2$, let $R_m$ be the remainder when the product $\prod_{k=1}^{F_{m-1}} k^k$ is divided by $F_m$. Prove that $R_m$ is also a Fibonacci number.


Lean 4 formalization:
import Mathlib

open Filter Topology

theorem putnam_2021_b4
(F : ℕ → ℕ)
(hF : ∀ n, F (n + 2) = F (n + 1) + F n)
(F01 : F 0 = 0 ∧ F 1 = 1)
: ∀ m, m > 2 → (∃ p, (∏ k : Set.Icc 1 (F m - 1),  (k.1 ^ k.1)) % F m = F p) := by
Problem: putnam_2021_b5
Category: linear_algebra, number_theory

Say that an $n$-by-$n$ matrix $A=(a_{ij})_{1 \leq i,j \leq n}$ with integer entries is \emph{very odd} if, for every nonempty subset $S$ of $\{1,2,\dots,n\}$, the $|S|$-by-$|S|$ submatrix $(a_{ij})_{i,j \in S}$ has odd determinant. Prove that if $A$ is very odd, then $A^k$ is very odd for every $k \geq 1$.


Lean 4 formalization:
import Mathlib

open Filter Topology

theorem putnam_2021_b5
(n : ℕ)
(npos : n ≥ 1)
(veryodd : Matrix (Fin n) (Fin n) ℤ → Prop)
(hveryodd : ∀ A, veryodd A ↔ ∀ m ∈ Set.Icc 1 n, ∀ reind : Fin m → Fin n, Function.Injective reind → Odd (A.submatrix reind reind).det)
: ∀ A, veryodd A → (∀ k ≥ 1, veryodd (A ^ k)) := by
Problem: putnam_2022_a1
Category: algebra

Determine all ordered pairs of real numbers $(a,b)$ such that the line $y = ax+b$ intersects the curve $y = \ln(1+x^2)$ in exactly one point.

Solution: Show that the solution is the set of ordered pairs $(a,b)$ which satisfy at least one of (1) $a = b = 0$, (2) $|a| \geq 1$, and (3) $0 < |a| < 1$ and $b < \log(1 + r_{-}^2) - ar_{-}$ or $b > \log(1 + r_{+}^2) - ar_{+}$ where $r_{\pm} = \frac{1 \pm \sqrt{1 - a^2}}{a}$.

Lean 4 formalization:
import Mathlib

open Polynomial

abbrev putnam_2022_a1_solution : Set (ℝ × ℝ) := sorry
theorem putnam_2022_a1
: {(a, b) | ∃! x : ℝ, a * x + b = Real.log (1 + x^2)} = putnam_2022_a1_solution := by
Problem: putnam_2022_a2
Category: algebra

Let $n$ be an integer with $n \geq 2$. Over all real polynomials $p(x)$ of degree $n$, what is the largest possible number of negative coefficients of $p(x)^2$?

Solution: Show that the solution is $2n - 2$.

Lean 4 formalization:
import Mathlib

open Polynomial

abbrev putnam_2022_a2_solution : ℕ → ℕ := sorry
theorem putnam_2022_a2
(n : ℕ)
(hn : n ≥ 2)
(S : Set ℝ[X])
(hS : S = {P | natDegree P = n})
(negs : ℝ[X] → ℕ)
(hnegs : ∀ P : ℝ[X], negs P = ∑ i ∈ Finset.range (P.natDegree + 1), if P.coeff i < 0 then 1 else 0)
: sSup {negs (P^2) | P ∈ S} = putnam_2022_a2_solution n := by
Problem: putnam_2022_a3
Category: number_theory

Let $p$ be a prime number greater than 5. Let $f(p)$ denote the number of infinite sequences $a_1, a_2, a_3, \dots$ such that $a_n \in \{1, 2, \dots, p-1\}$ and $a_n a_{n+2} \equiv 1 + a_{n+1} \pmod{p}$ for all $n \geq 1$. Prove that $f(p)$ is congruent to 0 or 2 $\pmod{5}$.


Lean 4 formalization:
import Mathlib

open Polynomial

theorem putnam_2022_a3
(p f : ℕ)
(hp : Nat.Prime p ∧ p > 5)
(hf : f = {a : ℕ → (ZMod p) | ∀ n : ℕ, a n ≠ 0 ∧ a n * a (n + 2) = 1 + a (n + 1)}.ncard)
: f ≡ 0 [MOD 5] ∨ f ≡ 2 [MOD 5] := by
Problem: putnam_2022_a4
Category: probability

Suppose $X_1, X_2, ...$ real numbers between 0 and 1 that are chosen independently and uniformly at random. Let $S = \sum_{i=1}^k X_i / 2^i $ where $k$ is the least positive integer such that $X_k < X_{k+1}$ or $k = \infty$ if there is no such integer. Find the expected value of $S$

Solution: 2*e^{-1/2} - 3

Lean 4 formalization:
import Mathlib

open MeasureTheory ProbabilityTheory Classical

abbrev putnam_2022_a4_solution : ℝ := sorry

theorem putnam_2022_a4
    {Ω : Type*} [MeasureSpace Ω]
    [IsProbabilityMeasure (ℙ : Measure Ω)]
    (X : ℕ → Ω → ℝ)
    (hX : ∀ i, Measurable (X i))
    (hX' : ∀ i, MeasureTheory.pdf.IsUniform (X i) (Set.Icc 0 1) ℙ)
    (hX'' : iIndepFun X)
    (k : Ω → Set ℕ)
    /-
    If there is an `l` such that `X_l < X_{l+1}` then this is `Set.Iic l` for the smallest such `l`
    Otherwise, this is `sSup { (Set.Iic m : Set ℕ) | (m : ℕ) } = Set.univ`
    -/
    (hk : ∀ ω, k ω = sSup { s : Set ℕ |
      ∃ m, s = Set.Iic m ∧ ∀ l, l < m → X l ω > X (l + 1) ω })
    (S : Ω → ℝ)
    (hS : ∀ ω, S ω = ∑' (i : k ω), (X i ω) / (2 ^ (i.val + 1))) :
    ∫ ω, S ω ∂(ℙ : Measure Ω) = putnam_2022_a4_solution := by
Problem: putnam_2022_a5
Category: combinatorics

Alice and Bob play a game on a board consisting of one row of 2022 consecutive squares. They take turns placing tiles that cover two adjacent squares, with Alice going first. By rule, a tile must not cover a square that is already covered by another tile. The game ends when no tile can be placed according to this rule. Alice's goal is to maximize the number of uncovered squares when the game ends; Bob's goal is to minimize it. What is the greatest number of uncovered squares that Alice can ensure at the end of the game, no matter how Bob plays?

Solution: Show that the solution is 290.

Lean 4 formalization:
import Mathlib

noncomputable abbrev putnam_2022_a5_solution : ℕ := sorry
theorem putnam_2022_a5
    (IsValidMove : Set (Fin 2022) → Set (Fin 2022) → Prop)
    (IsValidMove_def : ∀ x y, IsValidMove x y ↔
      (x = y ∧ ∀ i < 2021, i ∉ x → i + 1 ∈ x) ∨
      ∃ i < 2021, i ∉ x ∧ i + 1 ∉ x ∧ y = x ∪ {i, i + 1})
    (IsValidGame : List (Set (Fin 2022)) → Prop)
    (IsValidGame_def : ∀ g, IsValidGame g ↔ (∃ gt, g = ∅ :: gt) ∧ g.Chain' IsValidMove)
    (ConformsToStrategy : List (Set (Fin 2022)) → (Set (Fin 2022) → Set (Fin 2022)) → Prop)
    (ConformsToStrategy_def : ∀ g s, ConformsToStrategy g s ↔
      ∀ (i) (h : i + 1 < g.length), Even i → g[i + 1] = s g[i]) :
    IsGreatest
      {n | ∃ s, (∀ x, IsValidMove x (s x)) ∧ ∀ g,
        IsValidGame g → ConformsToStrategy g s → ∃ gh x, g = gh ++ [x] ∧ n ≤ xᶜ.ncard}
      putnam_2022_a5_solution := by
Problem: putnam_2022_a6
Category: algebra

Let $n$ be a positive integer. Determine, in terms of $n$, the largest integer $m$ with the following property: There exist real numbers $x_1,\dots,x_{2n}$ with $-1<x_1<x_2<\cdots<x_{2n}<1$ such that the sum of the lengths of the $n$ intervals $[x_1^{2k-1},x_2^{2k-1}],[x_3^{2k-1},x_4^{2k-1}],\dots,[x_{2n-1}^{2k-1},x_{2n}^{2k-1}]$ is equal to $1$ for all integers $k$ with $1 \leq k \leq m$.

Solution: Show that the largest such $m$ is $n$.

Lean 4 formalization:
import Mathlib

open Set

abbrev putnam_2022_a6_solution : ℕ → ℕ := sorry
theorem putnam_2022_a6
    (n : ℕ) (hn : 0 < n) :
    IsGreatest
      {m : ℕ | ∃ x : ℕ → ℝ,
        StrictMono x ∧ -1 < x 1 ∧ x (2 * n) < 1 ∧
        ∀ k ∈ Icc 1 m, ∑ i ∈ Icc 1 n, ((x (2 * i) : ℝ) ^ (2 * k - 1) - (x (2 * i - 1)) ^ (2 * k - 1)) = 1}
    (putnam_2022_a6_solution n) := by
Problem: putnam_2022_b1
Category: analysis, algebra

Suppose that $P(x)=a_1x+a_2x^2+\cdots+a_nx^n$ is a polynomial with integer coefficients, with $a_1$ odd. Suppose that $e^{P(x)}=b_0+b_1x+b_2x^2+\dots$ for all $x$. Prove that $b_k$ is nonzero for all $k \geq 0$.


Lean 4 formalization:
import Mathlib

open Polynomial

theorem putnam_2022_b1
    (P : Polynomial ℤ)
    (b : ℕ → ℝ)
    (Pconst : P.coeff 0 = 0)
    (Podd : Odd (P.coeff 1))
    (hB : ∀ x : ℝ, HasSum (fun i => b i * x ^ i) (Real.exp (aeval x P))) :
    ∀ k : ℕ, b k ≠ 0 := by
Problem: putnam_2022_b2
Category: algebra

Let $\times$ represent the cross product in $\mathbb{R}^3$. For what positive integers $n$ does there exist a set $S \subset \mathbb{R}^3$ with exactly $n$ elements such that $S=\{v \times w:v,w \in S\}$?

Solution: Show that the possible values of $n$ are $1$ and $7$.

Lean 4 formalization:
import Mathlib

open Polynomial

abbrev putnam_2022_b2_solution : Set ℕ := sorry
theorem putnam_2022_b2
  (n : ℕ)
  (P : Finset (Fin 3 → ℝ) → Prop)
  (P_def : ∀ S : Finset (Fin 3 → ℝ), P S ↔ (S = {u : Fin 3 → ℝ | ∃ v w : S, u = crossProduct v w})) :
  (0 < n ∧ ∃ S : Finset (Fin 3 → ℝ), S.card = n ∧ P S) ↔ n ∈ putnam_2022_b2_solution := by
Problem: putnam_2022_b3
Category: algebra

Assign to each positive real number a color, either red or blue. Let $D$ be the set of all distances $d>0$ such that there are two points of the same color at distance $d$ apart. Recolor the positive reals so that the numbers in $D$ are red and the numbers not in $D$ are blue. If we iterate this recoloring process, will we always end up with all the numbers red after a finite number of steps?

Solution: Show that the answer is yes.

Lean 4 formalization:
import Mathlib

open Polynomial

abbrev putnam_2022_b3_solution : Prop := sorry
theorem putnam_2022_b3
  (recolor : (ℝ → Prop) → (ℝ → Prop))
  (hrecolor : ∀ isred d, recolor isred d ↔ ∃ p q : ℝ, p > 0 ∧ q > 0 ∧ p < q ∧ isred p = isred q ∧ q - p = d) :
  (∀ isred, (∃ k, ∀ p > 0, (recolor^[k] isred) p)) ↔ putnam_2022_b3_solution := by
Problem: putnam_2022_b4
Category: algebra

Find all integers $n$ with $n \geq 4$ for which there exists a sequence of distinct real numbers $x_1,\dots,x_n$ such that each of the sets $\{x_1,x_2,x_3\},\{x_2,x_3,x_4\},\dots,\{x_{n-2},x_{n-1},x_n\},\{x_{n-1},x_n,x_1\}$, and $\{x_n,x_1,x_2\}$ forms a $3$-term arithmetic progression when arranged in increasing order.

Solution: Show that the values of $n$ in question are the multiples of $3$ starting with $9$.

Lean 4 formalization:
import Mathlib

open Polynomial

abbrev putnam_2022_b4_solution : Set ℕ := sorry
theorem putnam_2022_b4
  (n : ℕ)
  (hn : n ≥ 4)
  (ap3 : ℝ → ℝ → ℝ → Prop)
  (xprog : (ℕ → ℝ) → Prop)
  (hap3 : ∀ x0 x1 x2, ap3 x0 x1 x2 ↔ ∀ o0 o1 o2 : ℝ, (o0 < o1 ∧ o1 < o2 ∧ ({o0, o1, o2} : Set ℝ) = {x0, x1, x2}) → (o1 - o0 = o2 - o1))
  (hxprog : ∀ x, xprog x ↔
    ((∀ i j : Fin n, i.1 ≠ j.1 → x i.1 ≠ x j.1) ∧ (∀ i : Fin n, ap3 (x i.1) (x ((i.1 + 1) % n)) (x ((i.1 + 2) % n))))) :
  (∃ x, xprog x) ↔ n ∈ putnam_2022_b4_solution := by
Problem: putnam_2022_b5
Category: probability, algebra

For $0 \leq p \leq 1/2$, let $X_1,X_2,\dots$ be independent random variables such that
$X_i=\begin{cases}
1 & \text{with probability $p$,} \\
-1 & \text{with probability $p$,} \\
0 & \text{with probability $1-2p$,}
\end{cases}$
for all $i \geq 1$. Given a positive integer $n$ and integers $b,a_1,\dots,a_n$, let $P(b,a_1,\dots,a_n)$ denote the probability that $a_1X_1+\dots+a_nX_n=b$. For which values of $p$ is it the case that $P(0,a_1,\dots,a_n) \geq P(b,a_1,\dots,a_n)$ for all positive integers $n$ and all integers $b,a_1,\dots,a_n$?

Solution: Show that the answer is $p \leq 1/4$.

Lean 4 formalization:
import Mathlib

open Polynomial

abbrev putnam_2022_b5_solution : Set ℝ := sorry
theorem putnam_2022_b5
(p : ℝ)
(Xset : (n : ℕ) → Set (Fin n → ℤ))
(Xprob : (n : ℕ) → (Fin n → ℤ) → ℝ)
(P : (n : ℕ) → ℤ → (Fin n → ℤ) → ℝ)
(hXset : ∀ n > 0, Xset n = {X : Fin n → ℤ | ∀ i : Fin n, X i = 1 ∨ X i = -1 ∨ X i = 0})
(hXprob : ∀ n > 0, ∀ X : Fin n → ℤ, Xprob n X = ∏ i : Fin n, if (X i = 1 ∨ X i = -1) then p else (1 - 2 * p))
(hP : ∀ n > 0, ∀ (b : ℤ) (a : Fin n → ℤ), P n b a = ∑' X : {X' ∈ Xset n | (∑ i : Fin n, a i * X' i) = b}, Xprob n X)
: (0 ≤ p ∧ p ≤ 1 / 2 ∧ (∀ n > 0, ∀ (b : ℤ) (a : Fin n → ℤ), P n 0 a ≥ P n b a)) ↔ p ∈ putnam_2022_b5_solution := by
Problem: putnam_2022_b6
Category: analysis

Find all continuous functions $f:\mathbb{R}^+ \to \mathbb{R}^+$ such that $f(xf(y))+f(yf(x))=1+f(x+y)$ for all $x,y>0$.

Solution: Show that the only such functions are the functions $f(x)=\frac{1}{1+cx}$ for some $c \geq 0$.

Lean 4 formalization:
import Mathlib

open Polynomial

abbrev putnam_2022_b6_solution : Set (Set.Ioi (0 : ℝ) → Set.Ioi (0 : ℝ)) := sorry
theorem putnam_2022_b6
  (f : Set.Ioi (0 : ℝ) → Set.Ioi (0 : ℝ))
  (hf : Continuous f) :
  (∃ fr : ℝ → ℝ, (∀ x : Set.Ioi (0 : ℝ), fr x = f x) ∧ (∀ x y : Set.Ioi (0 : ℝ), fr (x * fr y) + fr (y * fr x) = 1 + fr (x + y)))
  ↔ f ∈ putnam_2022_b6_solution := by
Problem: putnam_2023_a1
Category: analysis

For a positive integer $n$, let $f_n(x) = \cos(x) \cos(2x) \cos(3x) \cdots \cos(nx)$. Find the smallest $n$ such that $|f_n''(0)| > 2023$.

Solution: Show that the solution is $n = 18$.

Lean 4 formalization:
import Mathlib

open Nat

abbrev putnam_2023_a1_solution : ℕ := sorry
theorem putnam_2023_a1
  (f : ℕ → ℝ → ℝ)
  (hf : ∀ n > 0, f n = fun x : ℝ => ∏ i ∈ Finset.Icc 1 n, Real.cos (i * x)) :
  IsLeast {n | 0 < n ∧ |iteratedDeriv 2 (f n) 0| > 2023} putnam_2023_a1_solution := by
Problem: putnam_2023_a2
Category: algebra

Let $n$ be an even positive integer. Let $p$ be a monic, real polynomial of degree $2n$; that is to say, $p(x) = x^{2n} + a_{2n-1} x^{2n-1} + \cdots + a_1 x + a_0$ for some real coefficients $a_0, \dots, a_{2n-1}$. Suppose that $p(1/k) = k^2$ for all integers $k$ such that $1 \leq |k| \leq n$. Find all other real numbers $x$ for which $p(1/x) = x^2$.

Solution: Show that the other real numbers satisfying $p(1/x) = x^2$ are $\pm \frac{1}{n!}.$

Lean 4 formalization:
import Mathlib

open Nat

abbrev putnam_2023_a2_solution : ℕ → Set ℝ := sorry
theorem putnam_2023_a2
(n : ℕ)
(hn : n > 0 ∧ Even n)
(p : Polynomial ℝ)
(hp : Polynomial.Monic p ∧ p.degree = 2*n)
(S : Set ℝ)
(hS : S = {x : ℝ | ∃ k : ℤ, x = k ∧ 1 ≤ |k| ∧ |k| ≤ n})
(hpinv : ∀ k ∈ S, p.eval (1/k) = k^2)
: {x : ℝ | x ≠ 0 ∧ p.eval (1/x) = x^2} \ S = putnam_2023_a2_solution n := by
Problem: putnam_2023_a3
Category: analysis

Determine the smallest positive real number $r$ such that there exist differentiable functions $f\colon \mathbb{R} \to \mathbb{R}$ and $g\colon \mathbb{R} \to \mathbb{R}$ satisfying
\begin{enumerate}
 \item[(a)] $f(0) > 0$,
 \item[(b)] $g(0) = 0$,
 \item[(c)] $|f'(x)| \leq |g(x)|$ for all $x$,
 \item[(d)] $|g'(x)| \leq |f(x)|$ for all $x$, and
 \item[(e)] $f(r) = 0$. \end{enumerate}

Solution: Show that the solution is $r = \pi/2$.

Lean 4 formalization:
import Mathlib

open Nat

noncomputable abbrev putnam_2023_a3_solution : ℝ := sorry
theorem putnam_2023_a3
: sInf {r > 0 | ∃ f g : ℝ → ℝ,
    Differentiable ℝ f ∧ Differentiable ℝ g ∧
    (∀ x : ℝ, |deriv f x| ≤ |g x| ∧ |deriv g x| ≤ |f x|) ∧
    f 0 > 0 ∧ g 0 = 0 ∧ f r = 0} = putnam_2023_a3_solution := by
Problem: putnam_2023_a4
Category: geometry, number_theory

Let $v_1, \ldots, v_{12}$ be unit vectors in $\mathbb{R}^3$ from the origin to the vertices of a regular icosahedron. Show that for every vector $v \in \mathbb{R}^3$ and every $\epsilon > 0$, there exist integers $a_1, \ldots, a_{12}$ such that $\|a_1v_1 + \cdots + a_{12}v_{12} - v\| < ε$.


Lean 4 formalization:
import Mathlib

theorem putnam_2023_a4
    (v : Fin 12 → EuclideanSpace ℝ (Fin 3))
    (hv :
      letI φ : ℝ := (1 + √5) / 2
      letI e : (Fin 3 → ℝ) ≃ EuclideanSpace ℝ (Fin 3) := (WithLp.equiv _ _).symm
      letI s := √(1 + φ ^ 2)
      ∃ g : EuclideanSpace ℝ (Fin 3) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 3),
      g ∘ v = s⁻¹ • e ∘ ![![1, φ, 0], ![-1,  φ,  0], ![ 1, -φ,  0], ![-1, -φ,  0],
                          ![φ, 0, 1], ![ φ,  0, -1], ![-φ,  0,  1], ![-φ,  0, -1],
                          ![0, 1, φ], ![ 0, -1,  φ], ![ 0,  1, -φ], ![ 0, -1, -φ]])
    (w : EuclideanSpace ℝ (Fin 3))
    (ε : ℝ) (hε : ε > 0) :
    ∃ a : Fin 12 → ℤ, ‖∑ i, a i • v i - w‖ < ε := by
Problem: putnam_2023_a5
Category: algebra

For a nonnegative integer $k$, let $f(k)$ be the number of ones in the base 3 representation of $k$. Find all complex numbers $z$ such that \[ \sum_{k=0}^{3^{1010}-1} (-2)^{f(k)} (z+k)^{2023} = 0. \]

Solution: Show that the solution is the set of complex numbers $\{- \frac{3^{1010} - 1}{2}, - \frac{3^{1010} - 1}{2} \pm \frac{\sqrt{9^{1010} - 1}}{4}i \}$

Lean 4 formalization:
import Mathlib

open Nat

def num_ones : List ℕ → ℕ
| [] => (0 : ℕ)
| (h :: t) => if h = 1 then num_ones t + 1 else num_ones t
abbrev putnam_2023_a5_solution : Set ℂ := sorry
theorem putnam_2023_a5
: {z : ℂ | ∑ k ∈ Finset.Icc 0 (3^1010 - 1), (-2)^(num_ones (digits 3 k)) * (z + k)^2023 = 0} = putnam_2023_a5_solution := by