ChristianZ97/putnambench-satp-v4.27 huggingface dataset:
Problem: putnam_1982_b5
Category: analysis

For all $x > e^e$, let $S = u_0, u_1, \dots$ be a recursively defined sequence with $u_0 = e$ and $u_{n+1} = \log_{u_n} x$ for all $n \ge 0$. Prove that $S_x$ converges to some real number $g(x)$ and that this function $g$ is continuous for $x > e^e$.


Lean 4 formalization:
import Mathlib

open Set Function Filter Topology Polynomial Real

theorem putnam_1982_b5
(T : Set ℝ)
(hT : T = Ioi (Real.exp (Real.exp 1)))
(S : ℝ → ℕ → ℝ)
(hS : ∀ x ∈ T, S x 0 = (Real.exp 1) ∧ ∀ n : ℕ, S x (n + 1) = Real.logb (S x n) x)
(g : ℝ → ℝ)
: ∀ x ∈ T, (∃ L : ℝ, Tendsto (S x) atTop (𝓝 L)) ∧
(∀ x ∈ T, Tendsto (S x) atTop (𝓝 (g x))) → ContinuousOn g T := by
Problem: putnam_1983_a1
Category: number_theory

How many positive integers $n$ are there such that $n$ is an exact divisor of at least one of the numbers $10^{40},20^{30}$?

Solution: Show that the desired count is $2301$.

Lean 4 formalization:
import Mathlib

abbrev putnam_1983_a1_solution : ℕ := sorry
theorem putnam_1983_a1
: {n : ℤ | n > 0 ∧ (n ∣ 10 ^ 40 ∨ n ∣ 20 ^ 30)}.encard = putnam_1983_a1_solution := by
Problem: putnam_1983_a3
Category: number_theory, algebra

Let $p$ be in the set $\{3,5,7,11,\dots\}$ of odd primes and let $F(n)=1+2n+3n^2+\dots+(p-1)n^{p-2}$. Prove that if $a$ and $b$ are distinct integers in $\{0,1,2,\dots,p-1\}$ then $F(a)$ and $F(b)$ are not congruent modulo $p$, that is, $F(a)-F(b)$ is not exactly divisible by $p$.


Lean 4 formalization:
import Mathlib

theorem putnam_1983_a3
(p : ℕ)
(F : ℕ → ℕ)
(poddprime : Odd p ∧ p.Prime)
(hF : ∀ n : ℕ, F n = ∑ i ∈ Finset.range (p - 1), (i + 1) * n ^ i)
: ∀ a ∈ Finset.Icc 1 p, ∀ b ∈ Finset.Icc 1 p, a ≠ b → ¬(F a ≡ F b [MOD p]) := by
Problem: putnam_1983_a4
Category: algebra

Prove that for $m = 5 \pmod 6$,
\[
\binom{m}{2} - \binom{m}{5} + \binom{m}{8} - \binom{m}{11} + ... - \binom{m}{m-6} + \binom{m}{m-3} \neq 0.
\]


Lean 4 formalization:
import Mathlib

open Nat

theorem putnam_1983_a4
(k m : ℕ)
(S : ℤ)
(kpos : k > 0)
(hm : m = 6 * k - 1)
(hS : S = ∑ j ∈ Finset.Icc 1 (2 * k - 1), (-1 : ℤ) ^ (j + 1) * choose m (3 * j - 1))
: (S ≠ 0) := by
Problem: putnam_1983_a5
Category: analysis

Prove or disprove that there exists a positive real number $\alpha$ such that $[\alpha_n] - n$ is even for all integers $n > 0$. (Here $[x]$ denotes the greatest integer less than or equal to $x$.)

Solution: Prove that such an $\alpha$ exists.

Lean 4 formalization:
import Mathlib

open Nat

abbrev putnam_1983_a5_solution : Prop := sorry
theorem putnam_1983_a5 :
    (∃ α : ℝ, α > 0 ∧ ∀ n : ℕ, n > 0 → Even (⌊α ^ n⌋ - n)) ↔ putnam_1983_a5_solution := by
Problem: putnam_1983_a6
Category: analysis

Let $T$ be the triangle with vertices $(0, 0)$, $(a, 0)$, and $(0, a)$. Find $\lim_{a \to \infty} a^4 \exp(-a^3) \int_T \exp(x^3+y^3) \, dx \, dy$.

Solution: Show that the integral evaluates to $\frac{2}{9}$.

Lean 4 formalization:
import Mathlib

open Nat Filter Topology Real

noncomputable abbrev putnam_1983_a6_solution : ℝ := sorry
theorem putnam_1983_a6
(F : ℝ → ℝ)
(hF : F = fun a ↦ (a ^ 4 / exp (a ^ 3)) * ∫ x in (0)..a, ∫ y in (0)..(a - x), exp (x ^ 3 + y ^ 3))
: (Tendsto F atTop (𝓝 putnam_1983_a6_solution)) := by
Problem: putnam_1983_b2
Category: algebra

Let $f(n)$ be the number of ways of representing $n$ as a sum of powers of $2$ with no power being used more than $3$ times. For example, $f(7) = 4$ (the representations are $4 + 2 + 1$, $4 + 1 + 1 + 1$, $2 + 2 + 2 + 1$, $2 + 2 + 1 + 1 + 1$). Can we find a real polynomial $p(x)$ such that $f(n) = [p(n)]$, where $[u]$ denotes the greatest integer less than or equal to $u$?

Solution: Prove that such a polynomial exists.

Lean 4 formalization:
import Mathlib

open Nat Filter Topology Real

abbrev putnam_1983_b2_solution : Prop := sorry
theorem putnam_1983_b2
    (f : ℕ+ → ℕ)
    (hf : f = fun (n : ℕ+) ↦
      Set.ncard {M : Multiset ℕ |
        (∀ m ∈ M, ∃ k : ℕ, m = (2 ^ k : ℤ)) ∧
        (∀ m ∈ M, M.count m ≤ 3) ∧
        (M.sum : ℤ) = n}) :
    putnam_1983_b2_solution ↔
      (∃ p : Polynomial ℝ, ∀ n : ℕ+, ⌊p.eval (n : ℝ)⌋ = f n) := by
Problem: putnam_1983_b4
Category: algebra

Let $f(n) = n + [\sqrt n]$, where $[x]$ denotes the greatest integer less than or equal to $x$. Define the sequence $a_i$ by $a_0 = m$, $a_{n+1} = f(a_n)$. Prove that it contains at least one square.


Lean 4 formalization:
import Mathlib

open Nat Real

theorem putnam_1983_b4
    (f : ℕ → ℤ)
    (a : ℕ → ℕ)
    (hf : f = fun (n : ℕ) ↦ n + Int.floor (√n))
    (ha0 : a 0 > 0)
    (han : ∀ n : ℕ, a (n + 1) = f (a n)) :
    (∃ i : ℕ, ∃ s : ℤ, a i = s ^ 2) := by
Problem: putnam_1983_b5
Category: analysis

Define $\left\lVert x \right\rVert$ as the distance from $x$ to the nearest integer. Find $\lim_{n \to \infty} \frac{1}{n} \int_{1}^{n} \left\lVert \frac{n}{x} \right\rVert \, dx$. You may assume that $\prod_{n=1}^{\infty} \frac{2n}{(2n-1)} \cdot \frac{2n}{(2n+1)} = \frac{\pi}{2}$.

Solution: Show that the limit equals $\ln \left( \frac{4}{\pi} \right)$.

Lean 4 formalization:
import Mathlib

open Nat Filter Topology Real

noncomputable abbrev putnam_1983_b5_solution : ℝ := sorry
theorem putnam_1983_b5
(dist_fun : ℝ → ℝ)
(hdist_fun : dist_fun = fun (x : ℝ) ↦ min (x - ⌊x⌋) (⌈x⌉ - x))
(fact : Tendsto (fun N ↦ ∏ n ∈ Finset.Icc 1 N, (2 * n / (2 * n - 1)) * (2 * n / (2 * n + 1)) : ℕ → ℝ) atTop (𝓝 (Real.pi / 2)))
: (Tendsto (fun n ↦ (1 / n) * ∫ x in (1)..n, dist_fun (n / x) : ℕ → ℝ) atTop (𝓝 putnam_1983_b5_solution)) := by
Problem: putnam_1983_b6
Category: algebra

Let $n$ be a positive integer and let $\alpha \neq 1$ be a complex $(2n + 1)\textsuperscript{th}$ root of unity. Prove that there always exist polynomials $p(x)$, $q(x)$ with integer coefficients such that $p(\alpha)^2 + q(\alpha)^2 = -1$.


Lean 4 formalization:
import Mathlib

open Nat Filter Topology Real Polynomial

theorem putnam_1983_b6
(n : ℕ)
(npos : n > 0)
(α : ℂ)
(hα : α ^ (2 ^ n + 1) - 1 = 0 ∧ α ≠ 1)
: (∃ p q : Polynomial ℤ, (aeval α p) ^ 2 + (aeval α q) ^ 2 = -1) := by
Problem: putnam_1984_a2
Category: analysis

Express $\sum_{k=1}^\infty (6^k/(3^{k+1}-2^{k+1})(3^k-2^k))$ as a rational number.

Solution: Show that the sum converges to $2$.

Lean 4 formalization:
import Mathlib

abbrev putnam_1984_a2_solution : ℚ := sorry
theorem putnam_1984_a2
: ∑' k : Set.Ici 1, ((6 : ℝ) ^ (k : ℕ) / ((3 ^ ((k : ℕ) + 1) - 2 ^ ((k : ℕ) + 1)) * (3 ^ (k : ℕ) - 2 ^ (k : ℕ)))) = putnam_1984_a2_solution := by
Problem: putnam_1984_a3
Category: linear_algebra, analysis

Let $n$ be a positive integer. Let $a,b,x$ be real numbers, with $a \neq b$, and let $M_n$ denote the $2n \times 2n$ matrix whose $(i,j)$ entry $m_{ij}$ is given by
\[
m_{ij}=\begin{cases}
x & \text{if }i=j, \\
a & \text{if }i \neq j\text{ and }i+j\text{ is even}, \\
b & \text{if }i \neq j\text{ and }i+j\text{ is odd}.
\end{cases}
\]
Thus, for example, $M_2=\begin{pmatrix} x & b & a & b \\ b & x & b & a \\ a & b & x & b \\ b & a & b & x \end{pmatrix}$. Express $\lim_{x \to a} \det M_n/(x-a)^{2n-2}$ as a polynomial in $a$, $b$, and $n$, where $\det M_n$ denotes the determinant of $M_n$.

Solution: Show that $\lim_{x \to a} \frac{\det M_n}{(x-a)^{2n-2}}=n^2(a^2-b^2)$.

Lean 4 formalization:
import Mathlib

open Topology Filter

noncomputable abbrev putnam_1984_a3_solution : MvPolynomial (Fin 3) ℝ := sorry
theorem putnam_1984_a3
(n : ℕ)
(a b : ℝ)
(Mn : ℝ → Matrix (Fin (2 * n)) (Fin (2 * n)) ℝ)
(polyabn : Fin 3 → ℝ)
(npos : n > 0)
(aneb : a ≠ b)
(hMn : Mn = fun x : ℝ => fun i j : Fin (2 * n) => if i = j then x else if Even (i.1 + j.1) then a else b)
(hpolyabn : polyabn 0 = a ∧ polyabn 1 = b ∧ polyabn 2 = n)
: Tendsto (fun x : ℝ => (Mn x).det / (x - a) ^ (2 * n - 2)) (𝓝[≠] a) (𝓝 (MvPolynomial.eval polyabn putnam_1984_a3_solution)) := by
Problem: putnam_1984_a5
Category: analysis

Let $R$ be the region consisting of all triples $(x,y,z)$ of nonnegative real numbers satisfying $x+y+z \leq 1$. Let $w=1-x-y-z$. Express the value of the triple integral $\iiint_R x^1y^9z^8w^4\,dx\,dy\,dz$ in the form $a!b!c!d!/n!$, where $a$, $b$, $c$, $d$, and $n$ are positive integers.

Solution: Show that the integral we desire is $1!9!8!4!/25!$.

Lean 4 formalization:
import Mathlib

open Topology Filter Nat

abbrev putnam_1984_a5_solution : ℕ × ℕ × ℕ × ℕ × ℕ := sorry
theorem putnam_1984_a5
    (R : Set (Fin 3 → ℝ))
    (w : (Fin 3 → ℝ) → ℝ)
    (hR : R = {p | (∀ i : Fin 3, p i ≥ 0) ∧ p 0 + p 1 + p 2 ≤ 1})
    (hw : ∀ p, w p = 1 - p 0 - p 1 - p 2) :
      let (a, b, c, d, n) := putnam_1984_a5_solution;
      a > 0 ∧ b > 0 ∧ c > 0 ∧ d > 0 ∧ n > 0 ∧
      (∫ p in R, (p 0) ^ 1 * (p 1) ^ 9 * (p 2) ^ 8 * (w p) ^ 4 = ((a)! * (b)! * (c)! * (d)! : ℝ) / (n)!) := by
Problem: putnam_1984_a6
Category: algebra, number_theory

Let $n$ be a positive integer, and let $f(n)$ denote the last nonzero digit in the decimal expansion of $n!$. For instance, $f(5)=2$.
\begin{enumerate}
\item[(a)] Show that if $a_1,a_2,\dots,a_k$ are \emph{distinct} nonnegative integers, then $f(5^{a_1}+5^{a_2}+\dots+5^{a_k})$ depends only on the sum $a_1+a_2+\dots+a_k$.
\item[(b)] Assuming part (a), we can define $g(s)=f(5^{a_1}+5^{a_2}+\dots+5^{a_k})$, where $s=a_1+a_2+\dots+a_k$. Find the least positive integer $p$ for which $g(s)=g(s + p)$, for all $s \geq 1$, or else show that no such $p$ exists.
\end{enumerate}

Solution: Show that the least such $p$ is $p=4$.

Lean 4 formalization:
import Mathlib

open Topology Filter Function Nat

abbrev putnam_1984_a6_solution : ℕ := sorry
theorem putnam_1984_a6
    (f : ℕ → ℕ)
    (hf : ∀ n, some (f n) = (Nat.digits 10 (n !)).find? (fun d ↦ d ≠ 0))
    (IsPeriodicFrom : ℕ → (ℕ → ℕ) → ℕ → Prop)
    (IsPeriodicFrom_def : ∀ x f p, IsPeriodicFrom x f p ↔ Periodic (f ∘ (· + x)) p)
    (P : ℕ → (ℕ → ℕ) → ℕ → Prop)
    (P_def : ∀ x g p, P x g p ↔ if p = 0 then (∀ q > 0, ¬ IsPeriodicFrom x g q) else
        IsLeast {q | 0 < q ∧ IsPeriodicFrom x g q} p) :
    ∃ g : ℕ → ℕ,
      (∀ᵉ (k > 0) (a : Fin k → ℕ) (ha : Injective a), f (∑ i, 5 ^ (a i)) = g (∑ i, a i)) ∧
      P 1 g putnam_1984_a6_solution := by
Problem: putnam_1984_b1
Category: algebra

Let $n$ be a positive integer, and define $f(n)=1!+2!+\dots+n!$. Find polynomials $P(x)$ and $Q(x)$ such that $f(n+2)=P(n)f(n+1)+Q(n)f(n)$ for all $n \geq 1$.

Solution: Show that we can take $P(x)=x+3$ and $Q(x)=-x-2$.

Lean 4 formalization:
import Mathlib

open Topology Filter Nat

noncomputable abbrev putnam_1984_b1_solution : Polynomial ℝ × Polynomial ℝ := sorry
theorem putnam_1984_b1
(f : ℕ → ℤ)
(hf : ∀ n > 0, f n = ∑ i : Set.Icc 1 n, ((i)! : ℤ))
: let (P, Q) := putnam_1984_b1_solution; ∀ n ≥ 1, f (n + 2) = P.eval (n : ℝ) * f (n + 1) + Q.eval (n : ℝ) * f n := by
Problem: putnam_1984_b2
Category: geometry, analysis

Find the minimum value of $(u-v)^2+(\sqrt{2-u^2}-\frac{9}{v})^2$ for $0<u<\sqrt{2}$ and $v>0$.

Solution: Show that the minimum value is $8$.

Lean 4 formalization:
import Mathlib

open Topology Filter Nat

abbrev putnam_1984_b2_solution : ℝ := sorry
theorem putnam_1984_b2
    (f : ℝ → ℝ → ℝ)
    (hf : ∀ u v : ℝ, f u v = (u - v) ^ 2 + (Real.sqrt (2 - u ^ 2) - 9 / v) ^ 2) :
    IsLeast {y | ∃ᵉ (u : Set.Ioo 0 √2) (v > 0), f u v = y} putnam_1984_b2_solution := by
Problem: putnam_1984_b3
Category: abstract_algebra

Prove or disprove the following statement: If $F$ is a finite set with two or more elements, then there exists a binary operation $*$ on F such that for all $x,y,z$ in $F$,
\begin{enumerate}
\item[(i)] $x*z=y*z$ implies $x=y$ (right cancellation holds), and
\item[(ii)] $x*(y*z) \neq (x*y)*z$ (\emph{no} case of associativity holds).
\end{enumerate}

Solution: Show that the statement is true.

Lean 4 formalization:
import Mathlib

open Topology Filter Nat

abbrev putnam_1984_b3_solution : Prop := sorry
theorem putnam_1984_b3
: (∀ (F : Type*) (_ : Fintype F), Fintype.card F ≥ 2 → (∃ mul : F → F → F, ∀ x y z : F, (mul x z = mul y z → x = y) ∧ (mul x (mul y z) ≠ mul (mul x y) z))) ↔ putnam_1984_b3_solution := by
Problem: putnam_1984_b5
Category: algebra, analysis

For each nonnegative integer $k$, let $d(k)$ denote the number of $1$'s in the binary expansion of $k$ (for example, $d(0)=0$ and $d(5)=2$). Let $m$ be a positive integer. Express $\sum_{k=0}^{2^m-1} (-1)^{d(k)}k^m$ in the form $(-1)^ma^{f(m)}(g(m))!$, where $a$ is an integer and $f$ and $g$ are polynomials.

Solution: Show that $\sum_{k=0}^{2^m-1} (-1)^{d(k)}k^m=(-1)^m2^{m(m-1)/2}m!$.

Lean 4 formalization:
import Mathlib

open Topology Filter Nat

noncomputable abbrev putnam_1984_b5_solution : ℤ × Polynomial ℝ × Polynomial ℕ := sorry
theorem putnam_1984_b5
    (m : ℕ) (mpos : m > 0)
    (d : ℕ → ℕ)
    (sumbits : List ℕ → ℕ)
    (hsumbits : ∀ bits : List ℕ, sumbits bits = ∑ i : Fin bits.length, bits[i])
    (hd : ∀ k : ℕ, d k = sumbits (Nat.digits 2 k)) :
    let (a, f, g) := putnam_1984_b5_solution;
    ∑ k : Set.Icc 0 (2 ^ m - 1), (-(1 : ℤ)) ^ (d k) * (k : ℕ) ^ m = (-1) ^ m * (a : ℝ) ^ (f.eval (m : ℝ)) * (g.eval m)! := by
Problem: putnam_1985_a1
Category: algebra

Determine, with proof, the number of ordered triples $(A_1, A_2, A_3)$ of sets which have the property that
\begin{enumerate}
\item[(i)] $A_1 \cup A_2 \cup A_3 = \{1,2,3,4,5,6,7,8,9,10\}$, and
\item[(ii)] $A_1 \cap A_2 \cap A_3 = \emptyset$.
\end{enumerate}
Express your answer in the form $2^a 3^b 5^c 7^d$, where $a,b,c,d$ are nonnegative integers.

Solution: Prove that the number of such triples is $2^{10}3^{10}$.

Lean 4 formalization:
import Mathlib

open Set

abbrev putnam_1985_a1_solution : ℕ × ℕ × ℕ × ℕ := sorry
theorem putnam_1985_a1 :
  let (a, b, c, d) := putnam_1985_a1_solution;
  {(A1, A2, A3) : Set ℤ × Set ℤ × Set ℤ | A1 ∪ A2 ∪ A3 = Icc 1 10 ∧ A1 ∩ A2 ∩ A3 = ∅}.ncard = 2 ^ a * 3 ^ b * 5 ^ c * 7 ^ d := by
Problem: putnam_1985_a3
Category: analysis

Let $d$ be a real number. For each integer $m \geq 0$, define a sequence $\{a_m(j)\}$, $j=0,1,2,\dots$ by the condition
\begin{align*}
a_m(0) &= d/2^m, \\
a_m(j+1) &= (a_m(j))^2 + 2a_m(j), \qquad j \geq 0.
\end{align*}
Evaluate $\lim_{n \to \infty} a_n(n)$.

Solution: Show that the limit equals $e^d - 1$.

Lean 4 formalization:
import Mathlib

open Set Filter Topology Real

noncomputable abbrev putnam_1985_a3_solution : ℝ → ℝ := sorry
theorem putnam_1985_a3
(d : ℝ)
(a : ℕ → ℕ → ℝ)
(ha0 : ∀ m : ℕ, a m 0 = d / 2 ^ m)
(ha : ∀ m : ℕ, ∀ j : ℕ, a m (j + 1) = (a m j) ^ 2 + 2 * a m j)
: Tendsto (fun n ↦ a n n) atTop (𝓝 (putnam_1985_a3_solution d)) := by
Problem: putnam_1985_a4
Category: number_theory

Define a sequence $\{a_i\}$ by $a_1=3$ and $a_{i+1}=3^{a_i}$ for $i \geq 1$. Which integers between $00$ and $99$ inclusive occur as the last two digits in the decimal expansion of infinitely many $a_i$?

Solution: Prove that the only number that occurs infinitely often is $87$.

Lean 4 formalization:
import Mathlib

open Set Filter Topology Real

abbrev putnam_1985_a4_solution : Set (Fin 100) := sorry
theorem putnam_1985_a4
    (a : ℕ → ℕ)
    (ha1 : a 1 = 3)
    (ha : ∀ i ≥ 1, a (i + 1) = 3 ^ a i) :
    {k : Fin 100 | ∀ N : ℕ, ∃ i ≥ N, a i % 100 = k} = putnam_1985_a4_solution := by
Problem: putnam_1985_a5
Category: analysis

Let $I_m = \int_0^{2\pi} \cos(x)\cos(2x)\cdots \cos(mx)\,dx$. For which integers $m$, $1 \leq m \leq 10$ is $I_m \neq 0$?

Solution: Prove that the integers $m$ with $1 \leq m \leq 10$ and $I_m \neq 0$ are $m = 3, 4, 7, 8$.

Lean 4 formalization:
import Mathlib

open Set Filter Topology Real

abbrev putnam_1985_a5_solution : Set ℕ := sorry
theorem putnam_1985_a5
    (I : ℕ → ℝ)
    (hI : I = fun (m : ℕ) ↦ ∫ x in (0)..(2 * Real.pi), ∏ k ∈ Finset.Icc 1 m, cos (k * x)) :
    {m ∈ Finset.Icc 1 10 | I m ≠ 0} = putnam_1985_a5_solution := by
Problem: putnam_1985_a6
Category: algebra

If $p(x)= a_0 + a_1 x + \cdots + a_m x^m$ is a polynomial with real coefficients $a_i$, then set
\[
\Gamma(p(x)) = a_0^2 + a_1^2 + \cdots + a_m^2.
\]
Let $F(x) = 3x^2+7x+2$. Find, with proof, a polynomial $g(x)$ with real coefficients such that
\begin{enumerate}
\item[(i)] $g(0)=1$, and
\item[(ii)] $\Gamma(f(x)^n) = \Gamma(g(x)^n)$
\end{enumerate}
for every integer $n \geq 1$.

Solution: Show that $g(x) = 6x^2 + 5x + 1$ satisfies the conditions.

Lean 4 formalization:
import Mathlib

open Set Filter Topology Real Polynomial

noncomputable abbrev putnam_1985_a6_solution : Polynomial ℝ := sorry
theorem putnam_1985_a6
  (Γ : Polynomial ℝ → ℝ)
  (f : Polynomial ℝ)
  (hΓ : Γ = fun p ↦ ∑ k ∈ Finset.range (p.natDegree + 1), coeff p k ^ 2)
  (hf : f = 3 * X ^ 2 + 7 * X + 2) :
  let g := putnam_1985_a6_solution;
  g.eval 0 = 1 ∧ ∀ n : ℕ, n ≥ 1 → Γ (f ^ n) = Γ (g ^ n) := by
Problem: putnam_1985_b1
Category: algebra

Let $k$ be the smallest positive integer for which there exist distinct integers $m_1, m_2, m_3, m_4, m_5$ such that the polynomial
\[
p(x) = (x-m_1)(x-m_2)(x-m_3)(x-m_4)(x-m_5)
\]
has exactly $k$ nonzero coefficients. Find, with proof, a set of integers $m_1, m_2, m_3, m_4, m_5$ for which this minimum $k$ is achieved.

Solution: Show that the minimum $k = 3$ is obtained for $\{m_1, m_2, m_3, m_4, m_5\} = \{-2, -1, 0, 1, 2\}$.

Lean 4 formalization:
import Mathlib

open Set Filter Topology Real Polynomial Function

abbrev putnam_1985_b1_solution : Fin 5 → ℤ := sorry
theorem putnam_1985_b1
(p : (Fin 5 → ℤ) → (Polynomial ℝ))
(hp : p = fun m ↦ ∏ i : Fin 5, ((X : Polynomial ℝ) - m i))
(numnzcoeff : Polynomial ℝ → ℕ)
(hnumnzcoeff : numnzcoeff = fun p ↦ {j ∈ Finset.range (p.natDegree + 1) | coeff p j ≠ 0}.card)
: (Injective putnam_1985_b1_solution ∧ ∀ m : Fin 5 → ℤ, Injective m → numnzcoeff (p putnam_1985_b1_solution) ≤ numnzcoeff (p m)) := by
Problem: putnam_1985_b2
Category: algebra

Define polynomials $f_n(x)$ for $n \geq 0$ by $f_0(x)=1$, $f_n(0)=0$ for $n \geq 1$, and
\[
\frac{d}{dx} f_{n+1}(x) = (n+1)f_n(x+1)
\]
for $n \geq 0$. Find, with proof, the explicit factorization of $f_{100}(1)$ into powers of distinct primes.

Solution: Show that $f_{100}(1) = 101^{99}$.

Lean 4 formalization:
import Mathlib

open Set Filter Topology Real Polynomial Function

abbrev putnam_1985_b2_solution : ℕ → ℕ := sorry
theorem putnam_1985_b2
  (f : ℕ -> Polynomial ℕ)
  (hf0x : f 0 = 1)
  (hfn0 : ∀ n ≥ 1, (f n).eval 0 = 0)
  (hfderiv : ∀ n : ℕ, derivative (f (n + 1)) = (n + 1) * (Polynomial.comp (f n) (X + 1)))
  : Nat.factorization ((f 100).eval 1) = putnam_1985_b2_solution := by
Problem: putnam_1985_b3
Category: algebra

Let
\[
\begin{array}{cccc} a_{1,1} & a_{1,2} & a_{1,3} & \dots \\
a_{2,1} & a_{2,2} & a_{2,3} & \dots \\
a_{3,1} & a_{3,2} & a_{3,3} & \dots \\
\vdots & \vdots & \vdots & \ddots
\end{array}
\]
be a doubly infinite array of positive integers, and suppose each positive integer appears exactly eight times in the array. Prove that $a_{m,n} > mn$ for some pair of positive integers $(m,n)$.


Lean 4 formalization:
import Mathlib

open Set Filter Topology Real Polynomial Function

theorem putnam_1985_b3
(a : ℕ → ℕ → ℕ)
(apos : ∀ m n : ℕ, a m n > 0)
(ha : ∀ k : ℕ, k > 0 → {(m, n) : ℕ × ℕ | m > 0 ∧ n > 0 ∧ a m n = k}.encard = 8)
: (∃ m n, m > 0 ∧ n > 0 ∧ a m n > m * n) := by
Problem: putnam_1985_b5
Category: analysis

Evaluate $\int_0^\infty t^{-1/2}e^{-1985(t+t^{-1})}\,dt$. You may assume that $\int_{-\infty}^\infty e^{-x^2}\,dx = \sqrt{\pi}$.

Solution: Show that the integral evaluates to $\sqrt{\frac{\pi}{1985}}e^{-3970}$.

Lean 4 formalization:
import Mathlib

open Set Filter Topology Real Polynomial Function

noncomputable abbrev putnam_1985_b5_solution : ℝ := sorry
theorem putnam_1985_b5
(fact : ∫ x in univ, exp (- x ^ 2) = sqrt (Real.pi))
: (∫ t in Set.Ioi 0, t ^ (- (1 : ℝ) / 2) * exp (-1985 * (t + t ^ (-(1 : ℝ)))) = putnam_1985_b5_solution) := by
Problem: putnam_1985_b6
Category: abstract_algebra, linear_algebra

Let $G$ be a finite set of real $n\times n$ matrices $\{M_i\}$, $1 \leq i \leq r$, which form a group under matrix
multiplication. Suppose that $\sum_{i=1}^r \mathrm{tr}(M_i)=0$, where $\mathrm{tr}(A)$ denotes the trace of the matrix $A$. Prove that $\sum_{i=1}^r M_i$ is the $n \times n$ zero matrix.


Lean 4 formalization:
import Mathlib

open Set Filter Topology Real Polynomial Function

theorem putnam_1985_b6
(n : ℕ)
(npos : n > 0)
(G : Finset (Matrix (Fin n) (Fin n) ℝ))
(groupG : (∀ g ∈ G, ∀ h ∈ G, g * h ∈ G) ∧ 1 ∈ G ∧ (∀ g ∈ G, ∃ h ∈ G, g * h = 1))
(hG : ∑ M ∈ G, Matrix.trace M = 0)
: (∑ M ∈ G, M = 0) := by
Problem: putnam_1986_a1
Category: algebra, analysis

Find, with explanation, the maximum value of $f(x)=x^3-3x$ on the set of all real numbers $x$ satisfying $x^4+36 \leq 13x^2$.

Solution: Show that the maximum value is $18$.

Lean 4 formalization:
import Mathlib

abbrev putnam_1986_a1_solution : ℝ := sorry
theorem putnam_1986_a1
    (S : Set ℝ) (f : ℝ → ℝ)
    (hS : S = {x : ℝ | x ^ 4 + 36 ≤ 13 * x ^ 2})
    (hf : f = fun x ↦ x ^ 3 - 3 * x) :
    IsGreatest
    {f x | x ∈ S}
    putnam_1986_a1_solution := by
Problem: putnam_1986_a2
Category: algebra

What is the units (i.e., rightmost) digit of
\[
\left\lfloor \frac{10^{20000}}{10^{100}+3}\right\rfloor ?
\]

Solution: Show that the answer is $3$.

Lean 4 formalization:
import Mathlib

abbrev putnam_1986_a2_solution : ℕ := sorry
theorem putnam_1986_a2
: (Nat.floor ((10 ^ 20000 : ℝ) / (10 ^ 100 + 3)) % 10 = putnam_1986_a2_solution) := by
Problem: putnam_1986_a3
Category: analysis

Evaluate $\sum_{n=0}^\infty \mathrm{Arccot}(n^2+n+1)$, where $\mathrm{Arccot}\,t$ for $t \geq 0$ denotes the number $\theta$ in the interval $0 < \theta \leq \pi/2$ with $\cot \theta = t$.

Solution: Show that the sum equals $\pi/2$.

Lean 4 formalization:
import Mathlib

open  Real

noncomputable abbrev putnam_1986_a3_solution : ℝ := sorry
theorem putnam_1986_a3
(cot : ℝ → ℝ)
(fcot : cot = fun θ ↦ cos θ / sin θ)
(arccot : ℝ → ℝ)
(harccot : ∀ t : ℝ, t ≥ 0 → arccot t ∈ Set.Ioc 0 (Real.pi / 2) ∧ cot (arccot t) = t)
: (∑' n : ℕ, arccot (n ^ 2 + n + 1) = putnam_1986_a3_solution) := by
Problem: putnam_1986_a4
Category: linear_algebra

A \emph{transversal} of an $n\times n$ matrix $A$ consists of $n$ entries of $A$, no two in the same row or column. Let $f(n)$ be the number of $n \times n$ matrices $A$ satisfying the following two conditions:
\begin{enumerate}
\item[(a)] Each entry $\alpha_{i,j}$ of $A$ is in the set
$\{-1,0,1\}$.
\item[(b)] The sum of the $n$ entries of a transversal is the same for all transversals of $A$.
\end{enumerate}
An example of such a matrix $A$ is
\[
A = \left( \begin{array}{ccc} -1 & 0 & -1 \\ 0 & 1 & 0 \\ 0 & 1 & 0
\end{array}
\right).
\]
Determine with proof a formula for $f(n)$ of the form
\[
f(n) = a_1 b_1^n + a_2 b_2^n + a_3 b_3^n + a_4,
\]
where the $a_i$'s and $b_i$'s are rational numbers.

Solution: Prove that $f(n) = 4^n + 2 \cdot 3^n - 4 \cdot 2^n + 1$.

Lean 4 formalization:
import Mathlib

open  Real Equiv

abbrev putnam_1986_a4_solution : ℚ × ℚ × ℚ × ℚ × ℚ × ℚ × ℚ := sorry
theorem putnam_1986_a4
  (f : ℕ → ℕ)
  (hf : f = fun n ↦
    Set.ncard {A : Matrix (Fin n) (Fin n) ℤ |
    (∀ i j : Fin n, A i j ∈ ({-1, 0, 1} : Set ℤ)) ∧
    ∃ S : ℤ, ∀ ϕ : Perm (Fin n), ∑ i : Fin n, A i (ϕ i) = S}) :
  let (a1, b1, a2, b2, a3, b3, a4) := putnam_1986_a4_solution;
  (∀ n > 0, f n = a1 * b1 ^ n + a2 * b2 ^ n + a3 * b3 ^ n + a4) := by
Problem: putnam_1986_a5
Category: analysis, linear_algebra

Suppose $f_1(x),f_2(x),\dots,f_n(x)$ are functions of $n$ real variables $x=(x_1,\dots,x_n)$ with continuous second-order partial derivatives everywhere on $\mathbb{R}^n$. Suppose further that there are constants $c_{ij}$ such that $\frac{\partial f_i}{\partial x_j}-\frac{\partial f_j}{\partial x_i}=c_{ij}$ for all $i$ and $j$, $1 \leq i \leq n$, $1 \leq j \leq n$. Prove that there is a function $g(x)$ on $\mathbb{R}^n$ such that $f_i+\partial g/\partial x_i$ is linear for all $i$, $1 \leq i \leq n$. (A linear function is one of the form $a_0+a_1x_1+a_2x_2+\dots+a_nx_n$.)


Lean 4 formalization:
import Mathlib

theorem putnam_1986_a5
  (n : ℕ) (hn : 1 ≤ n)
  (f : Fin n → ((Fin n → ℝ) → ℝ))
  (hf : ∀ i, ContDiff ℝ 2 (f i))
  (C : Fin n → Fin n → ℝ)
  (hf' : ∀ i j : Fin n, ∀ x : Fin n → ℝ, fderiv ℝ (f i) x (Pi.single j 1) - fderiv ℝ (f j) x (Pi.single i 1) = C i j)
  : ∃ g : (Fin n → ℝ) → ℝ, ∀ i : Fin n, IsLinearMap ℝ (λ x ↦ f i x + fderiv ℝ g x (Pi.single i 1)) := by