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

Prove that if
\[
11z^{10}+10iz^9+10iz-11=0,
\]
then $|z|=1.$ (Here $z$ is a complex number and $i^2=-1$.)


Lean 4 formalization:
import Mathlib
open Complex

theorem putnam_1989_a3
(z : ℂ)
(hz : 11 * z ^ 10 + 10 * I * z ^ 9 + 10 * I * z - 11 = 0)
: (‖z‖ = 1) := by
Problem: putnam_1989_a6
Category: algebra, abstract_algebra

Let $\alpha=1+a_1x+a_2x^2+\cdots$ be a formal power series with coefficients in the field of two elements. Let
\[
a_n =
\begin{cases}
1 & \parbox{2in}{if every block of zeros in the binary expansion of $n$ has an even number of zeros in the block} \\[.3in]
0 & \text{otherwise.}
\end{cases}
\]
(For example, $a_{36}=1$ because $36=100100_2$ and $a_{20}=0$ because $20=10100_2.$) Prove that $\alpha^3+x\alpha+1=0.$


Lean 4 formalization:
import Mathlib

open Nat

set_option synthInstance.maxSize 127

theorem putnam_1989_a6
(F : Type*) [Field F] [Fintype F]
(hF : Fintype.card F = 2)
(α : PowerSeries F)
(hα : ∀ n : ℕ, let bin := [1] ++ (digits 2 n) ++ [1]; PowerSeries.coeff n α = ite (∀ i j : Fin bin.length, i < j → bin.get i = 1 → bin.get j = 1 → (∀ k, i < k → k < j → bin.get k = 0) → Even ((j : ℕ) - (i : ℕ) - 1)) 1 0)
: (α ^ 3 + PowerSeries.X * α + 1 = 0) := by
Problem: putnam_1989_b1
Category: probability, geometry

A dart, thrown at random, hits a square target. Assuming that any two parts of the target of equal area are equally likely to be hit, find the probability that the point hit is nearer to the center than to any edge. Express your answer in the form $(a\sqrt{b}+c)/d$, where $a$, $b$, $c$, $d$ are integers and $b$, $d$ are positive.

Solution: Show that the probability is $(4\sqrt{2}-5)/3$.

Lean 4 formalization:
import Mathlib

open Nat MeasureTheory

abbrev putnam_1989_b1_solution : ℤ × ℤ × ℤ × ℤ := sorry
theorem putnam_1989_b1
    (square Scloser perimeter: Set (EuclideanSpace ℝ (Fin 2)))
    (center : EuclideanSpace ℝ (Fin 2))
    (square_def : square = {p | ∀ i : Fin 2, p i ∈ Set.Icc 0 1})
    (perimeter_def : perimeter = {p ∈ square | p 0 = 0 ∨ p 0 = 1 ∨ p 1 = 0 ∨ p 1 = 1})
    (center_def : center =  WithLp.toLp 2 (fun i : Fin 2 => 1 / 2))
    (hScloser : Scloser = {p ∈ square | ∀ q ∈ perimeter, dist p center < dist p q}) :
    let (a, b, c, d) := putnam_1989_b1_solution;
    b > 0 ∧ d > 0 ∧ (¬∃ n : ℤ, n^2 = b) ∧
    (volume Scloser).toReal / (volume square).toReal = (a * Real.sqrt b + c) / d := by
Problem: putnam_1989_b2
Category: abstract_algebra

Let $S$ be a non-empty set with an associative operation that is left and right cancellative ($xy=xz$ implies $y=z$, and $yx=zx$ implies $y=z$). Assume that for every $a$ in $S$ the set $\{a^n:\,n=1, 2, 3, \ldots\}$ is finite. Must $S$ be a group?

Solution: Prove that $S$ must be a group.

Lean 4 formalization:
import Mathlib

open Nat

abbrev putnam_1989_b2_solution : Prop := sorry
theorem putnam_1989_b2 :
    (∀ (S : Type) [Nonempty S] [Semigroup S] [IsCancelMul S]
      (h_fin : ∀ a : S, {(a * ·)^[n] a | n : ℕ}.Finite),
      ∃ e : S, ∀ x, e * x = x ∧ x * e = x ∧ ∃ y, x * y = e ∧ y * x = e) ↔
    putnam_1989_b2_solution := by
Problem: putnam_1989_b3
Category: analysis

Let $f$ be a function on $[0,\infty)$, differentiable and satisfying
\[
f'(x)=-3f(x)+6f(2x)
\]
for $x>0$. Assume that $|f(x)|\le e^{-\sqrt{x}}$ for $x\ge 0$ (so that $f(x)$ tends rapidly to $0$ as $x$ increases). For $n$ a non-negative integer, define
\[
\mu_n=\int_0^\infty x^n f(x)\,dx
\]
(sometimes called the $n$th moment of $f$).
\begin{enumerate}
\item[a)] Express $\mu_n$ in terms of $\mu_0$.
\item[b)] Prove that the sequence $\{\mu_n \frac{3^n}{n!}\}$ always converges, and that the limit is $0$ only if $\mu_0=0$.
\end{enumerate}

Solution: Show that for each $n \geq 0$, $\mu_n = \frac{n!}{3^n} \left( \prod_{m=1}^{n}(1 - 2^{-m}) \right)^{-1} \mu_0$.

Lean 4 formalization:
import Mathlib

open Nat Filter Topology

noncomputable abbrev putnam_1989_b3_solution : ℕ → ℝ → ℝ := sorry
theorem putnam_1989_b3
    (f : ℝ → ℝ)
    (hfdiff : Differentiable ℝ f)
    (hfderiv : ∀ x > 0, deriv f x = -3 * f x + 6 * f (2 * x))
    (hdecay : ∀ x ≥ 0, |f x| ≤ Real.exp (- √x))
    (μ : ℕ → ℝ)
    (μ_def : ∀ n, μ n = ∫ x in Set.Ioi 0, x ^ n * f x) :
    (∀ n, μ n = putnam_1989_b3_solution n (μ 0)) ∧
    (∃ L, Tendsto (fun n ↦ (μ n) * 3 ^ n / n !) atTop (𝓝 L)) ∧
    (Tendsto (fun n ↦ (μ n) * 3 ^ n / n !) atTop (𝓝 0) → μ 0 = 0) := by
Problem: putnam_1989_b4
Category: set_theory

Can a countably infinite set have an uncountable collection of non-empty subsets such that the intersection of any two of them is finite?

Solution: Prove that such a collection exists.

Lean 4 formalization:
import Mathlib

open Nat Filter Topology Set

abbrev putnam_1989_b4_solution : Prop := sorry
theorem putnam_1989_b4 :
  (∃ S : Type,
    Countable S ∧ Infinite S ∧
    ∃ C : Set (Set S),
      ¬Countable C ∧
      (∀ R ∈ C, R ≠ ∅) ∧
      (∀ A ∈ C, ∀ B ∈ C, A ≠ B → (A ∩ B).Finite)
  ) ↔ putnam_1989_b4_solution := by
Problem: putnam_1989_b6
Category: probability, analysis, algebra

Let $(x_1,x_2,\dots,x_n)$ be a point chosen at random from the $n$-dimensional region defined by $0<x_1<x_2<\dots<x_n<1$. Let $f$ be a continuous function on $[0,1]$ with $f(1)=0$. Set $x_0=0$ and $x_{n+1}=1$. Show that the expected value of the Riemann sum $\sum_{i=0}^n (x_{i+1}-x_i)f(x_{i+1})$ is $\int_0^1 f(t)P(t)\,dt$, where $P$ is a polynomial of degree $n$, independent of $f$, with $0 \leq P(t) \leq 1$ for $0 \leq t \leq 1$.


Lean 4 formalization:
import Mathlib

open Nat Filter Topology Set ProbabilityTheory

theorem putnam_1989_b6
    (n : ℕ) [NeZero n]
    (I : (Fin n → ℝ) → Fin (n + 2) → ℝ)
    (I_def : ∀ x, I x = Fin.cons 0 (Fin.snoc x 1))
    (X : Set (Fin n → ℝ))
    (X_def : ∀ x, x ∈ X ↔ 0 < x 0 ∧ x (-1) < 1 ∧ StrictMono x)
    (S : (ℝ → ℝ) → (Fin (n + 2) → ℝ) → ℝ)
    (S_def : ∀ f x, S f x = ∑ i : Fin n.succ, (x i.succ - x i.castSucc) * f (x i.succ)) :
    ∃ P : Polynomial ℝ,
      P.degree = n ∧
      (∀ t ∈ Icc 0 1, P.eval t ∈ Icc 0 1) ∧
      (∀ f : ℝ → ℝ, f 1 = 0 → ContinuousOn f (Icc 0 1) →
        ∫ x, S f (I x) ∂ℙ[|X] = ∫ t in (0)..1, f t * P.eval t) := by
Problem: putnam_1990_a1
Category: algebra

Let $T_0=2,T_1=3,T_2=6$, and for $n \geq 3$, $T_n=(n+4)T_{n-1}-4nT_{n-2}+(4n-8)T_{n-3}$. The first few terms are $2,3,6,14,40,152,784,5168,40576$. Find, with proof, a formula for $T_n$ of the form $T_n=A_n+B_n$, where $\{A_n\}$ and $\{B_n\}$ are well-known sequences.

Solution: Show that we have $T_n=n!+2^n$.

Lean 4 formalization:
import Mathlib

open Filter Topology Nat

abbrev putnam_1990_a1_solution : (ℕ → ℤ) × (ℕ → ℤ) := sorry
theorem putnam_1990_a1
    (T : ℕ → ℤ)
    (hT012 : T 0 = 2 ∧ T 1 = 3 ∧ T 2 = 6)
    (hTn : ∀ n, T (n + 3) = (n + 7) * T (n + 2) - 4 * (n + 3) * T (n + 1) + (4 * n + 4) * T n) :
    T = putnam_1990_a1_solution.1 + putnam_1990_a1_solution.2 := by
Problem: putnam_1990_a2
Category: analysis

Is $\sqrt{2}$ the limit of a sequence of numbers of the form $\sqrt[3]{n}-\sqrt[3]{m}$ ($n,m=0,1,2,\dots$)?

Solution: Show that the answer is yes.

Lean 4 formalization:
import Mathlib

open Filter Topology Nat

abbrev putnam_1990_a2_solution : Prop := sorry
theorem putnam_1990_a2
  (numform : ℝ → Prop)
  (hnumform : ∀ x : ℝ, numform x ↔ ∃ n m : ℕ, x = n ^ ((1 : ℝ) / 3) - m ^ ((1 : ℝ) / 3)) :
  putnam_1990_a2_solution ↔
  (∃ s : ℕ → ℝ,
    (∀ i : ℕ, numform (s i)) ∧
    Tendsto s atTop (𝓝 (Real.sqrt 2))) := by
Problem: putnam_1990_a4
Category: set_theory, number_theory

Consider a paper punch that can be centered at any point of the plane and that, when operated, removes from the plane precisely those points whose distance from the center is irrational. How many punches are needed to remove every point?

Solution: Show that three punches are needed.

Lean 4 formalization:
import Mathlib

open Filter Topology Nat

abbrev putnam_1990_a4_solution : ℕ := sorry
theorem putnam_1990_a4
: sInf {n : ℕ | ∃ S : Set (EuclideanSpace ℝ (Fin 2)), S.encard = n ∧ ∀ Q : EuclideanSpace ℝ (Fin 2), ∃ P ∈ S, Irrational (dist P Q)} = putnam_1990_a4_solution := by
Problem: putnam_1990_a5
Category: linear_algebra

If $\mathbf{A}$ and $\mathbf{B}$ are square matrices of the same size such that $\mathbf{ABAB}=\mathbf{0}$, does it follow that $\mathbf{BABA}=\mathbf{0}$?

Solution: Show that the answer is no.

Lean 4 formalization:
import Mathlib

open Filter Topology Nat

abbrev putnam_1990_a5_solution : Prop := sorry
theorem putnam_1990_a5 :
  putnam_1990_a5_solution ↔
  (∀ n ≥ 1, ∀ A B : Matrix (Fin n) (Fin n) ℝ,
    A * B * A * B = 0 → B * A * B * A = 0) := by
Problem: putnam_1990_a6
Category: algebra

If $X$ is a finite set, let $|X|$ denote the number of elements in $X$. Call an ordered pair $(S,T)$ of subsets of $\{1,2,\dots,n\}$ \emph{admissible} if $s>|T|$ for each $s \in S$, and $t>|S|$ for each $t \in T$. How many admissible ordered pairs of subsets of $\{1,2,\dots,10\}$ are there? Prove your answer.

Solution: Show that the number of admissible ordered pairs of subsets of $\{1,2,\dots,10\}$ equals the $22$nd Fibonacci number $F_{22}=17711$.

Lean 4 formalization:
import Mathlib

open Filter Topology Nat

abbrev putnam_1990_a6_solution : ℕ := sorry
theorem putnam_1990_a6 :
    ((Finset.univ : Finset <| Finset (Set.Icc 1 10) × Finset (Set.Icc 1 10)).filter
      fun ⟨S, T⟩ ↦ (∀ s ∈ S, T.card < s) ∧ (∀ t ∈ T, S.card < t)).card =
    putnam_1990_a6_solution := by
Problem: putnam_1990_b1
Category: analysis

Find all real-valued continuously differentiable functions $f$ on the real line such that for all $x$, $(f(x))^2=\int_0^x [(f(t))^2+(f'(t))^2]\,dt+1990$.

Solution: Show that there are two such functions, namely $f(x)=\sqrt{1990}e^x$, and $f(x)=-\sqrt{1990}e^x$.

Lean 4 formalization:
import Mathlib

open Filter Topology Nat

abbrev putnam_1990_b1_solution : Set (ℝ → ℝ) := sorry
theorem putnam_1990_b1
    (P : (ℝ → ℝ) → Prop)
    (P_def : ∀ f, P f ↔ ∀ x,
      (f x) ^ 2 = (∫ t in (0 : ℝ)..x, (f t) ^ 2 + (deriv f t) ^ 2) + 1990)
    (f : ℝ → ℝ) :
    (ContDiff ℝ 1 f ∧ P f) ↔ f ∈ putnam_1990_b1_solution := by
Problem: putnam_1990_b2
Category: analysis

Prove that for $|x|<1$, $|z|>1$, $1+\sum_{j=1}^\infty (1+x^j)P_j=0$, where $P_j$ is $\frac{(1-z)(1-zx)(1-zx^2) \cdots (1-zx^{j-1})}{(z-x)(z-x^2)(z-x^3) \cdots (z-x^j)}$.


Lean 4 formalization:
import Mathlib

open Filter Topology Nat

theorem putnam_1990_b2
(x z : ℝ)
(P : ℕ → ℝ)
(xlt1 : |x| < 1)
(zgt1 : |z| > 1)
(hP : ∀ j ≥ 1, P j = (∏ i : Fin j, (1 - z * x ^ (i : ℕ))) / (∏ i : Set.Icc 1 j, (z - x ^ (i : ℕ))))
: 1 + (∑' j : Set.Ici 1, (1 + x ^ (j : ℕ)) * P j) = 0 := by
Problem: putnam_1990_b3
Category: linear_algebra

Let $S$ be a set of $2 \times 2$ integer matrices whose entries $a_{ij}$ (1) are all squares of integers, and, (2) satisfy $a_{ij} \leq 200$. Show that if $S$ has more than $50387$ ($=15^4-15^2-15+2$) elements, then it has two elements that commute.


Lean 4 formalization:
import Mathlib

open Filter Topology Nat

theorem putnam_1990_b3
(S : Set (Matrix (Fin 2) (Fin 2) ℕ))
(hS : ∀ A ∈ S, ∀ i j : Fin 2, (∃ x : ℤ, A i j = x ^ 2) ∧ A i j ≤ 200)
: (S.encard > 50387) → (∃ A ∈ S, ∃ B ∈ S, A ≠ B ∧ A * B = B * A) := by
Problem: putnam_1990_b4
Category: abstract_algebra

Let $G$ be a finite group of order $n$ generated by $a$ and $b$. Prove or disprove: there is a sequence $g_1,g_2,g_3,\dots,g_{2n}$ such that
\begin{itemize}
\item[(1)] every element of $G$ occurs exactly twice, and
\item[(2)] $g_{i+1}$ equals $g_ia$ or $g_ib$ for $i=1,2,\dots,2n$. (Interpret $g_{2n+1}$ as $g_1$.)
\end{itemize}

Solution: Show that such a sequence does exist.

Lean 4 formalization:
import Mathlib

open Filter Topology Nat

abbrev putnam_1990_b4_solution : Prop := sorry
theorem putnam_1990_b4
: (∀ (G : Type*) (_ : Fintype G) (_ : Group G) (n : ℕ) (a b : G), (n = Fintype.card G ∧ G = Subgroup.closure {a, b} ∧ G ≠ Subgroup.closure {a} ∧ G ≠ Subgroup.closure {b}) → (∃ g : ℕ → G, (∀ x : G, {i : Fin (2 * n) | g i = x}.encard = 2)
  ∧ (∀ i : Fin (2 * n), (g ((i + 1) % (2 * n)) = g i * a) ∨ (g ((i + 1) % (2 * n)) = g i * b))) ↔ putnam_1990_b4_solution) := by
Problem: putnam_1990_b5
Category: algebra, analysis

Is there an infinite sequence $a_0,a_1,a_2,\dots$ of nonzero real numbers such that for $n=1,2,3,\dots$ the polynomial $p_n(x)=a_0+a_1x+a_2x^2+\cdots+a_nx^n$ has exactly $n$ distinct real roots?

Solution: Show that the answer is yes, such an infinite sequence exists.

Lean 4 formalization:
import Mathlib

open Filter Polynomial Topology Nat

abbrev putnam_1990_b5_solution : Prop := sorry
theorem putnam_1990_b5 :
    (∃ a : ℕ → ℝ, (∀ i, a i ≠ 0) ∧
      (∀ n ≥ 1, (∑ i ∈ Finset.Iic n, a i • X ^ i : Polynomial ℝ).roots.toFinset.card = n)) ↔
    putnam_1990_b5_solution := by
Problem: putnam_1991_a2
Category: linear_algebra

Let $\mathbf{A}$ and $\mathbf{B}$ be different $n \times n$ matrices with real entries. If $\mathbf{A}^3=\mathbf{B}^3$ and $\mathbf{A}^2\mathbf{B}=\mathbf{B}^2\mathbf{A}$, can $\mathbf{A}^2+\mathbf{B}^2$ be invertible?

Solution: Show that the answer is no.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_1991_a2_solution : Prop := sorry
theorem putnam_1991_a2
  (n : ℕ) (hn : 1 ≤ n) :
  putnam_1991_a2_solution ↔ (∃ A B : Matrix (Fin n) (Fin n) ℝ,
    A ≠ B ∧ A ^ 3 = B ^ 3 ∧
    A ^ 2 * B = B ^ 2 * A ∧
    Nonempty (Invertible (A ^ 2 + B ^ 2))) := by
Problem: putnam_1991_a3
Category: algebra, analysis

Find all real polynomials $p(x)$ of degree $n \geq 2$ for which there exist real numbers $r_1<r_2<\cdots<r_n$ such that
\begin{enumerate}
\item $p(r_i)=0, \qquad i=1,2,\dots,n$, and
\item $p'(\frac{r_i+r_{i+1}}{2})=0 \qquad i=1,2,\dots,n-1$,
\end{enumerate}
where $p'(x)$ denotes the derivative of $p(x)$.

Solution: Show that the real polynomials with the required property are exactly those that are of degree $2$ with $2$ distinct real zeros.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_1991_a3_solution : Set (Polynomial ℝ) := sorry
theorem putnam_1991_a3
  (p : Polynomial ℝ)
  (n : ℕ)
  (hn : n = p.degree)
  (hge : n ≥ 2) :
  p ∈ putnam_1991_a3_solution ↔
    (∃ r : ℕ → ℝ, (∀ i : Fin (n - 1), r i < r (i + 1)) ∧
    (∀ i : Fin n, p.eval (r i) = 0) ∧
    (∀ i : Fin (n - 1), (Polynomial.derivative p).eval ((r i + r (i + 1)) / 2) = 0)) := by
Problem: putnam_1991_a4
Category: geometry, analysis

Does there exist an infinite sequence of closed discs $D_1,D_2,D_3,\dots$ in the plane, with centers $c_1,c_2,c_3,\dots$, respectively, such that
\begin{enumerate}
\item the $c_i$ have no limit point in the finite plane,
\item the sum of the areas of the $D_i$ is finite, and
\item every line in the plane intersects at least one of the $D_i$?
\end{enumerate}

Solution: Show that the answer is yes, such a sequence of closed discs exists.

Lean 4 formalization:
import Mathlib

open Filter Metric Topology

abbrev putnam_1991_a4_solution : Prop := sorry
theorem putnam_1991_a4 :
    (∃ (c : ℕ → EuclideanSpace ℝ (Fin 2)) (r : ℕ → ℝ),
      (¬ ∃ p, MapClusterPt p atTop c) ∧
      (Summable <| fun i ↦ r i ^ 2) ∧
      (∀ L : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)),
        Module.finrank ℝ L.direction = 1 → ∃ i, (↑L ∩ closedBall (c i) (r i)).Nonempty)) ↔
    putnam_1991_a4_solution := by
Problem: putnam_1991_a5
Category: analysis

Find the maximum value of $\int_0^y \sqrt{x^4+(y-y^2)^2}\,dx$ for $0 \leq y \leq 1$.

Solution: Show that the maximum value of the integral is $1/3$.

Lean 4 formalization:
import Mathlib

open Filter Topology

noncomputable abbrev putnam_1991_a5_solution : ℝ := sorry
theorem putnam_1991_a5
  (f : Set.Icc (0 : ℝ) 1 → ℝ)
  (hf : ∀ y : Set.Icc 0 1, f y = ∫ x in Set.Ioo 0 y, Real.sqrt (x ^ 4 + (y - y ^ 2) ^ 2)) :
  IsGreatest (f '' (Set.Icc 0 1)) putnam_1991_a5_solution := by
Problem: putnam_1991_a6
Category: algebra

Let $A(n)$ denote the number of sums of positive integers $a_1+a_2+\cdots+a_r$ which add up to $n$ with $a_1>a_2+a_3,a_2>a_3+a_4,\dots,a_{r-2}>a_{r-1}+a_r,a_{r-1}>a_r$. Let $B(n)$ denote the number of $b_1+b_2+\cdots+b_s$ which add up to $n$, with
\begin{enumerate}
\item $b_1 \geq b_2 \geq \dots \geq b_s$,
\item each $b_i$ is in the sequence $1,2,4,\dots,g_j,\dots$ defined by $g_1=1$, $g_2=2$, and $g_j=g_{j-1}+g_{j-2}+1$, and
\item if $b_1=g_k$ then every element in $\{1,2,4,\dots,g_k\}$ appears at least once as a $b_i$.
\end{enumerate}
Prove that $A(n)=B(n)$ for each $n \geq 1$. (For example, $A(7)=5$ because the relevant sums are $7,6+1,5+2,4+3,4+2+1$, and $B(7)=5$ because the relevant sums are $4+2+1,2+2+2+1,2+2+1+1+1,2+1+1+1+1+1,1+1+1+1+1+1+1$.)


Lean 4 formalization:
import Mathlib

open Filter Topology

theorem putnam_1991_a6
  (nabsum : ℕ → ℕ × (ℕ → ℕ) → Prop)
  (agt bge bg1 bg2 : ℕ × (ℕ → ℕ) → Prop)
  (A g B: ℕ → ℕ)
  (hnabsum : ∀ᵉ (n ≥ 1) (ab), nabsum n ab ↔
    (ab.1 ≥ 1 ∧ (∀ i < ab.1, ab.2 i > 0) ∧
    (∀ i ≥ ab.1, ab.2 i = 0) ∧ (∑ i : Fin ab.1, ab.2 i) = n))
  (hA : ∀ n ≥ 1, A n = {a | nabsum n a ∧
    (∀ i : Fin (a.1 - 2), a.2 i > a.2 (i + 1) + a.2 (i + 2)) ∧ 1 < a.1 → a.2 (a.1 - 2) > a.2 (a.1 - 1)}.encard)
  (hg : g 0 = 1 ∧ g 1 = 2 ∧ (∀ j ≥ 2, g j = g (j - 1) + g (j - 2) + 1))
  (hB : ∀ n ≥ 1, B n = {b | nabsum n b ∧
    (∀ i : Fin (b.1 - 1), b.2 i ≥ b.2 (i + 1)) ∧
    (∀ i : Fin b.1, ∃ j : ℕ, b.2 i = g j) ∧
    (∃ k : ℕ, b.2 0 = g k ∧ (∀ j ≤ k, ∃ i : Fin b.1, b.2 i = g j))}.encard) :
  ∀ n ≥ 1, (A n) = (B n) := by
Problem: putnam_1991_b1
Category: algebra

For each integer $n \geq 0$, let $S(n)=n-m^2$, where $m$ is the greatest integer with $m^2 \leq n$. Define a sequence $(a_k)_{k=0}^\infty$ by $a_0=A$ and $a_{k+1}=a_k+S(a_k)$ for $k \geq 0$. For what positive integers $A$ is this sequence eventually constant?

Solution: Show that this sequence is eventually constant if and only if $A$ is a perfect square.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_1991_b1_solution : Set ℤ := sorry
theorem putnam_1991_b1
  (m S : ℤ → ℤ)
  (A : ℤ)
  (a : ℕ → ℤ)
  (hm : ∀ n, 0 ≤ n → (m n) ^ 2 ≤ n ∧ (∀ m' : ℤ, m' ^ 2 ≤ n → m' ≤ m n))
  (hS : ∀ n, 0 ≤ n → S n = n - (m n) ^ 2)
  (ha : a 0 = A ∧ (∀ k, a (k + 1) = a k + S (a k)))
  (hA : A > 0) :
  (∃ (K : ℕ) (c : ℕ), ∀ k ≥ K, a k = c) ↔ A ∈ putnam_1991_b1_solution := by
Problem: putnam_1991_b2
Category: analysis

Suppose $f$ and $g$ are non-constant, differentiable, real-valued functions defined on $(-\infty,\infty)$. Furthermore, suppose that for each pair of real numbers $x$ and $y$,
\begin{align*}
f(x+y)&=f(x)f(y)-g(x)g(y), \\
g(x+y)&=f(x)g(y)+g(x)f(y).
\end{align*}
If $f'(0)=0$, prove that $(f(x))^2+(g(x))^2=1$ for all $x$.


Lean 4 formalization:
import Mathlib

open Filter Topology

theorem putnam_1991_b2
  (f g : ℝ → ℝ)
  (fgnconst : ¬∃ c, f = Function.const ℝ c ∨ g = Function.const ℝ c)
  (fgdiff : Differentiable ℝ f ∧ Differentiable ℝ g)
  (fadd : ∀ x y, f (x + y) = f x * f y - g x * g y)
  (gadd : ∀ x y, g (x + y) = f x * g y + g x * f y) :
  (deriv f 0 = 0) → (∀ x, (f x) ^ 2 + (g x) ^ 2 = 1) := by
Problem: putnam_1991_b4
Category: number_theory, algebra

Suppose $p$ is an odd prime. Prove that $\sum_{j=0}^p \binom{p}{j}\binom{p+j}{j} \equiv 2^p+1 \pmod{p^2}$.


Lean 4 formalization:
import Mathlib

open Filter Topology

theorem putnam_1991_b4
(p : ℕ)
(podd : Odd p)
(pprime : Prime p)
: (∑ j : Fin (p + 1), (p.choose j) * ((p + j).choose j)) ≡ (2 ^ p + 1) [MOD (p ^ 2)] := by
Problem: putnam_1991_b5
Category: number_theory

Let $p$ be an odd prime and let $\mathbb{Z}_p$ denote (the field of) integers modulo $p$. How many elements are in the set $\{x^2:x \in \mathbb{Z}_p\} \cap \{y^2+1:y \in \mathbb{Z}_p\}$?

Solution: Show that the number of elements in the intersection is $\lceil p/4 \rceil$.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_1991_b5_solution : ℕ → ℕ := sorry
theorem putnam_1991_b5
(p : ℕ)
(podd : Odd p)
(pprime : Prime p)
: ({z : ZMod p | ∃ x : ZMod p, z = x ^ 2} ∩ {z : ZMod p | ∃ y : ZMod p, z = y ^ 2 + 1}).encard = putnam_1991_b5_solution p := by
Problem: putnam_1991_b6
Category: analysis

Let $a$ and $b$ be positive numbers. Find the largest number $c$, in terms of $a$ and $b$, such that $a^xb^{1-x} \leq a\frac{\sinh ux}{\sinh u}+b\frac{\sinh u(1-x)}{\sinh u}$ for all $u$ with $0<|u| \leq c$ and for all $x$, $0<x<1$. (Note: $\sinh u=(e^u-e^{-u})/2$.)

Solution: Show that the largest $c$ for which the inequality holds for $0<|u| \leq c$ is $c=|\ln(a/b)|$.

Lean 4 formalization:
import Mathlib

open Filter Topology

noncomputable abbrev putnam_1991_b6_solution : ℝ → ℝ → ℝ := sorry
theorem putnam_1991_b6
  (a b : ℝ)
  (abpos : a > 0 ∧ b > 0) :
  IsGreatest {c | ∀ u,
    (0 < |u| ∧ |u| ≤ c) →
    (∀ x ∈ Set.Ioo 0 1, a ^ x * b ^ (1 - x) ≤ a * (Real.sinh (u * x) / Real.sinh u) + b * (Real.sinh (u * (1 - x)) / Real.sinh u))}
  (putnam_1991_b6_solution a b) := by
Problem: putnam_1992_a1
Category: algebra

Prove that $f(n) = 1-n$ is the only integer-valued function defined on the integers that satisfies the following conditions.
\begin{itemize}
\item[(i)] $f(f(n)) = n$, for all integers $n$;
\item[(ii)] $f(f(n+2)+2) = n$ for all integers $n$;
\item[(iii)] $f(0) = 1$.
\end{itemize}


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_1992_a1
  (f : ℤ → ℤ) :
  (f = fun n ↦ 1 - n) ↔
  (∀ n : ℤ, f (f n) = n) ∧ (∀ n : ℤ, f (f (n + 2) + 2) = n) ∧ (f 0 = 1) := by
Problem: putnam_1992_a2
Category: analysis, algebra

Define $C(\alpha)$ to be the coefficient of $x^{1992}$ in the power series about $x=0$ of $(1 + x)^\alpha$. Evaluate
\[
\int_0^1 \left( C(-y-1) \sum_{k=1}^{1992} \frac{1}{y+k} \right)\,dy.
\]

Solution: Prove that the integral evaluates to $1992$.

Lean 4 formalization:
import Mathlib

open Topology Filter

abbrev putnam_1992_a2_solution : ℝ := sorry
theorem putnam_1992_a2
(C : ℝ → ℝ)
(hC : C = fun α ↦ taylorCoeffWithin (fun x ↦ (1 + x) ^ α) 1992 Set.univ 0)
: (∫ y in (0)..1, C (-y - 1) * ∑ k ∈ Finset.Icc (1 : ℕ) 1992, 1 / (y + k) = putnam_1992_a2_solution) := by
Problem: putnam_1992_a3
Category: algebra, number_theory

For a given positive integer $m$, find all triples $(n, x, y)$ of positive integers, with $n$ relatively prime to $m$, which satisfy
\[
(x^2 + y^2)^m = (xy)^n.
\]

Solution: Prove that if $m$ is odd, there are no solutions, and if $m$ is even, the only solution is
$(n, x, y) = (m + 1, 2 ^ {m/2}, 2 ^{m/2})$.

Lean 4 formalization:
import Mathlib

open Topology Filter Nat

abbrev putnam_1992_a3_solution : ℕ → Set (ℕ × ℕ × ℕ) := sorry
theorem putnam_1992_a3
(m : ℕ)
(mpos : m > 0)
(S : Set (ℕ × ℕ × ℕ))
(hS : ∀ n x y : ℕ, (n, x, y) ∈ S ↔ n > 0 ∧ x > 0 ∧ y > 0 ∧ Coprime n m ∧ (x ^ 2 + y ^ 2) ^ m = (x * y) ^ n)
: (S = putnam_1992_a3_solution m) := by
Problem: putnam_1992_a4
Category: analysis

Let $f$ be an infinitely differentiable real-valued function defined on the real numbers. If
\[
f\left( \frac{1}{n} \right) = \frac{n^2}{n^2 + 1}, \qquad n = 1, 2, 3, \dots,
\]
compute the values of the derivatives $f^{(k)}(0), k = 1, 2, 3, \dots$.

Solution: Prove that
\[
f^{(k)}(0) =
\begin{cases}
(-1)^{k/2}k! & \text{if $k$ is even;} \\
0 & \text{if $k$ is odd.} \\
\end{cases}
\]

Lean 4 formalization:
import Mathlib

open Topology Filter Nat Function

abbrev putnam_1992_a4_solution : ℕ → ℝ := sorry
theorem putnam_1992_a4
(f : ℝ → ℝ)
(hfdiff : ContDiff ℝ ⊤ f)
(hf : ∀ n : ℕ, n > 0 → f (1 / n) = n ^ 2 / (n ^ 2 + 1))
: (∀ k : ℕ, k > 0 → iteratedDeriv k f 0 = putnam_1992_a4_solution k) := by
Problem: putnam_1992_a5
Category: algebra

For each positive integer $n$, let $a_n = 0$ (or $1$) if the number of $1$'s in the binary representation of $n$ is even (or odd), respectively. Show that there do not exist positive integers $k$ and $m$ such that
\[
a_{k+j} = a_{k+m+j} = a_{k+2m+j},
\]
for $0 \leq j \leq m-1$.


Lean 4 formalization:
import Mathlib

open Topology Filter Nat Function

theorem putnam_1992_a5
  (a : ℕ → ℕ)
  (ha : a = fun n ↦ ite (Even {i | (digits 2 n).get i = 1}.ncard) 0 1) :
  ¬∃ k > 0, ∃ m > 0, ∀ j ≤ m - 1,
    a (k + j) = a (k + m + j) ∧ a (k + m + j) = a (k + 2 * m + j) := by