ChristianZ97/putnambench-satp-v4.27 huggingface dataset:
Problem: putnam_1998_b5
Category: number_theory

Let $N$ be the positive integer with 1998 decimal digits, all of them 1; that is, \[N=1111\cdots 11.\] Find the thousandth digit after the decimal point of $\sqrt N$.

Solution: Show that the thousandth digit is 1.

Lean 4 formalization:
import Mathlib

open Set Function Metric

abbrev putnam_1998_b5_solution : ℕ := sorry
theorem putnam_1998_b5
(N : ℕ)
(hN : N = ∑ i ∈ Finset.range 1998, 10^i)
: putnam_1998_b5_solution = (Nat.floor (10^1000 * Real.sqrt N)) % 10 := by
Problem: putnam_1998_b6
Category: number_theory

Prove that, for any integers $a, b, c$, there exists a positive integer $n$ such that $\sqrt{n^3+an^2+bn+c}$ is not an integer.


Lean 4 formalization:
import Mathlib

open Set Function Metric

theorem putnam_1998_b6
: ∀ a b c : ℤ, ∃ n : ℤ, n > 0 ∧ ¬(∃ k : ℤ, k = Real.sqrt (n^3 + a * n^2 + b * n + c)) := by
Problem: putnam_1999_a1
Category: algebra

Find polynomials $f(x)$,$g(x)$, and $h(x)$, if they exist, such that for all $x$, \[|f(x)|-|g(x)|+h(x) = \begin{cases} -1 & \mbox{if $x<-1$} \\3x+2 & \mbox{if $-1 \leq x \leq 0$} \\-2x+2 & \mbox{if $x>0$.}\end{cases}\]?

Solution: Show that the answer is such functions do exist.

Lean 4 formalization:
import Mathlib

abbrev putnam_1999_a1_solution : Prop := sorry
theorem putnam_1999_a1
: putnam_1999_a1_solution ↔ ∃ f g h : Polynomial ℝ, ∀ x : ℝ, |f.eval x| - |g.eval x| + h.eval x = if x < -1 then -1 else (if (x ≤ 0) then 3 * x + 2 else -2 * x + 2) := by
Problem: putnam_1999_a2
Category: algebra

Let $p(x)$ be a polynomial that is nonnegative for all real $x$.  Prove that for some $k$, there are polynomials $f_1(x),\dots,f_k(x$) such that \[p(x) =  \sum_{j=1}^k (f_j(x))^2.\]


Lean 4 formalization:
import Mathlib

theorem putnam_1999_a2
(p : Polynomial ℝ)
(hp : ∀ x, p.eval x ≥ 0)
: ∃ᵉ (k) (f : Fin k → Polynomial ℝ),
    k > 0 ∧
    ∀ x : ℝ, p.eval x = ∑ j : Fin k, ((f j).eval x) ^ 2 := by
Problem: putnam_1999_a3
Category: algebra

Consider the power series expansion \[\frac{1}{1-2x-x^2} = \sum_{n=0}^\infty a_n x^n.\] Prove that, for each integer $n\geq 0$, there is an integer $m$ such that \[a_n^2 + a_{n+1}^2 = a_m .\]


Lean 4 formalization:
import Mathlib

open Filter Topology Metric

theorem putnam_1999_a3
    (f : ℝ → ℝ)
    (hf : f = fun x ↦ 1 / (1 - 2 * x - x ^ 2))
    (a : ℕ → ℝ)
    (hf' : ∀ᶠ x in 𝓝 0, Tendsto (fun N : ℕ ↦ ∑ n ∈ Finset.range N, (a n) * x ^ n) atTop (𝓝 (f x)))
    (n : ℕ) :
    ∃ m : ℕ, (a n) ^ 2 + (a (n + 1)) ^ 2 = a m := by
Problem: putnam_1999_a4
Category: number_theory

Sum the series \[\sum_{m=1}^\infty \sum_{n=1}^\infty \frac{m^2 n}{3^m(n3^m+m3^n)}.\]

Solution: Show that the solution is 9/32.

Lean 4 formalization:
import Mathlib

open Filter Topology Metric

noncomputable abbrev putnam_1999_a4_solution : ℝ := sorry
theorem putnam_1999_a4
: Tendsto (fun i => ∑ m ∈ Finset.range i, ∑' n : ℕ, (((m + 1)^2*(n+1))/(3^(m + 1) * ((n+1)*3^(m + 1) + (m + 1)*3^(n+1))) : ℝ)) atTop (𝓝 putnam_1999_a4_solution) := by
Problem: putnam_1999_a5
Category: analysis

Prove that there is a constant $C$ such that, if $p(x)$ is a polynomial of degree 1999, then \[|p(0)|\leq C \int_{-1}^1 |p(x)|\,dx.\]


Lean 4 formalization:
import Mathlib

open Filter Topology Metric

theorem putnam_1999_a5
: ∃ C : ℝ, ∀ p : Polynomial ℝ, p.degree = 1999 → ‖p.eval 0‖ ≤ C * ∫ x in (-1)..1, ‖p.eval x‖ := by
Problem: putnam_1999_a6
Category: algebra

The sequence $(a_n)_{n\geq 1}$ is defined by $a_1=1, a_2=2, a_3=24,$ and, for $n\geq 4$, \[a_n = \frac{6a_{n-1}^2a_{n-3} - 8a_{n-1}a_{n-2}^2}{a_{n-2}a_{n-3}}.\] Show that, for all n, $a_n$ is an integer multiple of $n$.


Lean 4 formalization:
import Mathlib

open Filter Topology Metric

theorem putnam_1999_a6
(a : ℤ → ℝ)
(ha1 : a 1 = 1)
(ha2 : a 2 = 2)
(ha3 : a 3 = 24)
(hange4 : ∀ n : ℕ, n ≥ 4 → a n = (6 * (a (n - 1))^2 * (a (n - 3)) - 8 * (a (n - 1)) * (a (n - 2))^2)/(a (n - 2) * a (n - 3)))
: ∀ n, n ≥ 1 → (∃ k : ℤ, a n = k * n) := by
Problem: putnam_1999_b2
Category: analysis

Let $P(x)$ be a polynomial of degree $n$ such that $P(x)=Q(x)P''(x)$, where $Q(x)$ is a quadratic polynomial and $P''(x)$ is the second derivative of $P(x)$.  Show that if $P(x)$ has at least two distinct roots then it must have $n$ distinct roots.


Lean 4 formalization:
import Mathlib

open Filter Topology Metric

theorem putnam_1999_b2
  (P Q : Polynomial ℂ)
  (hQ : Q.natDegree = 2)
  (hP : ∀ x : ℂ, P.eval x = (Q.eval x) * (Polynomial.derivative^[2] P).eval x) :
  (∃ x1 x2, x1 ≠ x2 ∧ P.eval x1 = 0 ∧ P.eval x2 = 0) →
  (∃ f : Fin (P.natDegree) → ℂ,
    (∀ i j, i ≠ j → f i ≠ f j) ∧
    (∀ i, P.eval (f i) = 0)) := by
Problem: putnam_1999_b3
Category: algebra

Let $A=\{(x,y):0\leq x,y<1\}$.  For $(x,y)\in A$, let \[S(x,y) = \sum_{\frac{1}{2}\leq \frac{m}{n}\leq 2} x^m y^n,\] where the sum ranges over all pairs $(m,n)$ of positive integers satisfying the indicated inequalities.  Evaluate \[\lim_{(x,y)\rightarrow (1,1), (x,y)\in A} (1-xy^2)(1-x^2y)S(x,y).\]

Solution: Show that the answer is 3.

Lean 4 formalization:
import Mathlib

open Filter Topology Metric

abbrev putnam_1999_b3_solution : ℝ := sorry
theorem putnam_1999_b3
(A : Set (ℝ × ℝ))
(hA : A = {xy | 0 ≤ xy.1 ∧ xy.1 < 1 ∧ 0 ≤ xy.2 ∧ xy.2 < 1})
(S : ℝ → ℝ → ℝ)
(hS : S = fun x y => ∑' m : ℕ, ∑' n : ℕ, if (m > 0 ∧ n > 0 ∧ (1 : ℝ)/2 ≤ (m : ℝ)/n ∧ (m : ℝ)/n ≤ 2) then x^m * y^n else 0)
: Tendsto (fun xy : (ℝ × ℝ) => (1 - xy.1 * xy.2^2) * (1 - xy.1^2 * xy.2) * (S xy.1 xy.2)) (𝓝[A] ⟨1,1⟩) (𝓝 putnam_1999_b3_solution) := by
Problem: putnam_1999_b4
Category: analysis

Let $f$ be a real function with a continuous third derivative such that $f(x), f'(x), f''(x), f'''(x)$ are positive for all $x$.  Suppose that $f'''(x)\leq f(x)$ for all $x$.  Show that $f'(x)<2f(x)$ for all $x$.


Lean 4 formalization:
import Mathlib

open Filter Topology Metric

theorem putnam_1999_b4
(f : ℝ → ℝ)
(hf : ContDiff ℝ 3 f)
(hpos: ∀ n ≤ 3, ∀ x : ℝ, iteratedDeriv n f x > 0)
(hle : ∀ x : ℝ, iteratedDeriv 3 f x ≤ f x)
: ∀ x : ℝ, deriv f x < 2 * (f x) := by
Problem: putnam_1999_b5
Category: linear_algebra

For an integer $n\geq 3$, let $\theta=2\pi/n$.  Evaluate the determinant of the $n\times n$ matrix $I+A$, where $I$ is the $n\times n$ identity matrix and $A=(a_{jk})$ has entries $a_{jk}=\cos(j\theta+k\theta)$ for all $j,k$.

Solution: Show that the answer is $(1 - n^2)/4$.

Lean 4 formalization:
import Mathlib

open Filter Topology Metric

noncomputable abbrev putnam_1999_b5_solution : ℕ → ℝ := sorry
theorem putnam_1999_b5
  (n : ℕ)
  (hn : n ≥ 3)
  (theta : ℝ)
  (htheta : theta = 2 * Real.pi / n)
  (A : Matrix (Fin n) (Fin n) ℝ)
  (hA : A = fun j k => Real.cos ((j.1 + 1) * theta + (k.1 + 1) * theta)) :
  (1 + A).det = putnam_1999_b5_solution n := by
Problem: putnam_1999_b6
Category: number_theory

Let $S$ be a finite set of integers, each greater than 1.  Suppose that for each integer $n$ there is some $s\in S$ such that $\gcd(s,n)=1$ or $\gcd(s,n)=s$.  Show that there exist $s,t\in S$ such that $\gcd(s,t)$ is prime.


Lean 4 formalization:
import Mathlib

open Filter Topology Metric

theorem putnam_1999_b6
  (S : Finset ℤ)
  (hSgt : ∀ s, s ∈ S → s > 1)
  (hSgcd : ∀ n, ∃ s ∈ S, Int.gcd s n = 1 ∨ Int.gcd s n = s) :
  ∃ᵉ (s ∈ S) (t ∈ S), Prime (Int.gcd s t) := by
Problem: putnam_2000_a1
Category: analysis

Let $A$ be a positive real number. What are the possible values of $\sum_{j=0}^\infty x_j^2$, given that $x_0,x_1,\ldots$ are positive numbers for which $\sum_{j=0}^\infty x_j=A$?

Solution: Show that the possible values comprise the interval $(0,A^2)$.

Lean 4 formalization:
import Mathlib

open Topology Filter

abbrev putnam_2000_a1_solution : ℝ → Set ℝ := sorry
theorem putnam_2000_a1
(A : ℝ)
(Apos : A > 0)
: {S : ℝ |
    ∃ x : ℕ → ℝ,
      (∀ j : ℕ, x j > 0) ∧
      (∑' j : ℕ, x j) = A ∧
      (∑' j : ℕ, (x j) ^ 2) = S}
  = putnam_2000_a1_solution A := by
Problem: putnam_2000_a2
Category: number_theory

Prove that there exist infinitely many integers $n$ such that $n,n+1,n+2$ are each the sum of the squares of two integers.


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_2000_a2 :
  ∀ n : ℕ,
    ∃ N : ℤ,
      ∃ i : Fin 6 → ℕ,
        N > n ∧
        N = (i 0)^2 + (i 1)^2 ∧
        N + 1 = (i 2)^2 + (i 3)^2 ∧
        N + 2 = (i 4)^2 + (i 5)^2 := by
Problem: putnam_2000_a4
Category: analysis

Show that the improper integral $\lim_{B \to \infty} \int_0^B \sin(x)\sin(x^2)\,dx$ converges.


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_2000_a4
: ∃ y : ℝ, Tendsto (fun B : ℝ => ∫ x in Set.Ioo 0 B, Real.sin x * Real.sin (x ^ 2)) atTop (𝓝 y) := by
Problem: putnam_2000_a5
Category: algebra

Three distinct points with integer coordinates lie in the plane on a circle of radius $r>0$. Show that two of these points are separated by a distance of at least $r^{1/3}$.


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_2000_a5
  (r : ℝ)
  (z : EuclideanSpace ℝ (Fin 2))
  (p : Fin 3 → (EuclideanSpace ℝ (Fin 2)))
  (rpos : r > 0)
  (pdiff : ∀ n m, (n ≠ m) → (p n ≠ p m))
  (pint : ∀ n i, p n i = round (p n i))
  (pcirc : ∀ n, p n ∈ Metric.sphere z r) :
  ∃ n m, (n ≠ m) ∧ (dist (p n) (p m) ≥ r ^ ((1 : ℝ) / 3)) := by
Problem: putnam_2000_a6
Category: algebra

Let $f(x)$ be a polynomial with integer coefficients. Define a sequence $a_0,a_1,\ldots$ of integers such that $a_0=0$ and $a_{n+1}=f(a_n)$ for all $n\geq 0$. Prove that if there exists a positive integer $m$ for which $a_m=0$ then either $a_1=0$ or $a_2=0$.


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_2000_a6
(f : Polynomial ℤ)
(a : ℕ → ℤ)
(ha0 : a 0 = 0)
(ha : ∀ n : ℕ, a (n + 1) = f.eval (a n))
: ((∃ m > 0, a m = 0) → (a 1 = 0 ∨ a 2 = 0)) := by
Problem: putnam_2000_b1
Category: algebra

Let $a_j,b_j,c_j$ be integers for $1\leq j\leq N$. Assume for each $j$, at least one of $a_j,b_j,c_j$ is odd. Show that there exist integers $r$, $s$, $t$ such that $ra_j+sb_j+tc_j$ is odd for at least $4N/7$ values of $j$, $1\leq j\leq N$.


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_2000_b1
(N : ℕ)
(a b c : Fin N → ℤ)
(Nge1 : N ≥ 1)
(hodd : ∀ j : Fin N, Odd (a j) ∨ Odd (b j) ∨ Odd (c j))
: (∃ r s t : ℤ, {j : Fin N | Odd (r * a j + s * b j + t * c j)}.ncard ≥ (4 * N : ℝ) / 7) := by
Problem: putnam_2000_b2
Category: number_theory, algebra

Prove that the expression
\[
\frac{gcd(m,n)}{n}\binom{n}{m}
\]
is an integer for all pairs of integers $n\geq m\geq 1$.


Lean 4 formalization:
import Mathlib

open Topology Filter Nat

theorem putnam_2000_b2
: (∀ m n : ℕ, m ≥ 1 → n ≥ m → n ∣ Nat.gcd m n * Nat.choose n m) := by
Problem: putnam_2000_b3
Category: analysis

Let $f(t)=\sum_{j=1}^N a_j \sin(2\pi jt)$, where each $a_j$ is real and $a_N$ is not equal to $0$. Let $N_k$ denote the number of zeroes (including multiplicities) of $\frac{d^k f}{dt^k}$. Prove that
\[
N_0\leq N_1\leq N_2\leq \cdots \mbox{ and } \lim_{k\to\infty} N_k = 2N.
\]


Lean 4 formalization:
import Mathlib

open Topology Filter Nat Set Function

theorem putnam_2000_b3
  (N : ℕ) (hN : N > 0)
  (a : Icc 1 N → ℝ)
  (f : ℝ → ℝ)
  (mult : (ℝ → ℝ) → ℝ → ℕ)
  (M : ℕ → ℕ)
  (haN : a ⟨N, by simp; omega⟩ ≠ 0)
  (hf : ∀ t, f t = ∑ j : Icc 1 N, a j * Real.sin (2 * Real.pi * j * t))
  (hmult : ∀ g : ℝ → ℝ, ∀ t : ℝ, (∃ c : ℕ, iteratedDeriv c g t ≠ 0) → (iteratedDeriv (mult g t) g t ≠ 0 ∧ ∀ k < (mult g t), iteratedDeriv k g t = 0))
  (hM : ∀ k, M k = ∑' t : Ico (0 : ℝ) 1, mult (iteratedDeriv k f) t) :
  ((∀ i j : ℕ, i ≤ j → M i ≤ M j) ∧ Tendsto M atTop (𝓝 (2 * N))) := by
Problem: putnam_2000_b4
Category: analysis

Let $f(x)$ be a continuous function such that $f(2x^2-1)=2xf(x)$ for all $x$.  Show that $f(x)=0$ for $-1\leq x\leq 1$.


Lean 4 formalization:
import Mathlib

open Topology Filter Nat Set Function

theorem putnam_2000_b4
(f : ℝ → ℝ)
(hfcont : Continuous f)
(hf : ∀ x, f (2 * x ^ 2 - 1) = 2 * x * f x)
: ∀ x, x ∈ Icc (-1) 1 → f x = 0 := by
Problem: putnam_2000_b5
Category: algebra

Let $S_0$ be a finite set of positive integers. We define finite sets $S_1,S_2,\ldots$ of positive integers as follows: the integer $a$ is in $S_{n+1}$ if and only if exactly one of $a-1$ or $a$ is in $S_n$. Show that there exist infinitely many integers $N$ for which $S_N=S_0\cup\{N+a: a\in S_0\}$.


Lean 4 formalization:
import Mathlib

open Topology Filter Nat Set Function

theorem putnam_2000_b5
(S : ℕ → Set ℤ)
(hSfin : ∀ n, Set.Finite (S n))
(hSpos : ∀ n, ∀ s ∈ S n, s > 0)
(hSdef : ∀ n, ∀ a, a ∈ S (n + 1) ↔ Xor' (a - 1 ∈ S n) (a ∈ S n))
: (∀ n, ∃ N ≥ n, S N = S 0 ∪ {M : ℤ | M - N ∈ S 0}) := by
Problem: putnam_2001_a1
Category: abstract_algebra

Consider a set $S$ and a binary operation $*$, i.e., for each $a,b\in S$, $a*b\in S$.  Assume $(a*b)*a=b$ for all $a,b\in S$.  Prove that $a*(b*a)=b$ for all $a,b\in S$.


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_2001_a1
(S : Type*)
[Mul S]
(hS : ∀ a b : S, (a * b) * a = b)
: ∀ a b : S, a * (b * a) = b := by
Problem: putnam_2001_a3
Category: algebra

For each integer $m$, consider the polynomial
\[P_m(x)=x^4-(2m+4)x^2+(m-2)^2.\] For what values of $m$ is $P_m(x)$
the product of two non-constant polynomials with integer coefficients?

Solution: $P_m(x)$ factors into two nonconstant polynomials over
the integers if and only if $m$ is either a square or twice a square.

Lean 4 formalization:
import Mathlib

open Topology Filter Polynomial Set

abbrev putnam_2001_a3_solution : Set ℤ := sorry
theorem putnam_2001_a3
(P : ℤ → Polynomial ℤ)
(hP : P = fun m : ℤ => (Polynomial.X)^4 - (Polynomial.C (2*m + 4))*(Polynomial.X)^2 + Polynomial.C ((m - 2)^2))
: {m : ℤ | ∃ a b, P m = a * b ∧
(∃ n ∈ Ici 1, a.coeff n ≠ 0) ∧ (∃ n ∈ Ici 1, b.coeff n ≠ 0)} = putnam_2001_a3_solution := by
Problem: putnam_2001_a5
Category: number_theory

Prove that there are unique positive integers $a$, $n$ such that $a^{n+1}-(a+1)^n=2001$.


Lean 4 formalization:
import Mathlib

open Topology Filter Polynomial Set

theorem putnam_2001_a5
: ∃! an : ℤ × ℕ, let (a, n) := an; a > 0 ∧ n > 0 ∧ a^(n+1) - (a+1)^n = 2001 := by
Problem: putnam_2001_b1
Category: algebra

Let $n$ be an even positive integer. Write the numbers $1,2,\ldots,n^2$ in the squares of an $n \times n$ grid so that the $k$-th row, from left to right, is $(k-1)n+1,(k-1)n+2,\ldots,(k-1)n+n$. Color the squares of the grid so that half of the squares in each row and in each column are red and the other half are black (a checkerboard coloring is one possibility). Prove that for each coloring, the sum of the numbers on the red squares is equal to the sum of the numbers on the black squares.


Lean 4 formalization:
import Mathlib

open Topology Filter Polynomial Set

theorem putnam_2001_b1
  (n : ℕ)
  (hn : n > 0) (hn' : Even n)
  (nums : Fin n → Fin n → ℤ)
  (colors : Fin n → Fin n → Fin 2)
  (hnums : ∀ k l, nums k l = k * n + l + 1)
  (hcolorsrows : ∀ k, (∑ l, (if (colors k l = 0) then 1 else 0)) = n / 2)
  (hcolorscols : ∀ l, (∑ k, (if (colors k l = 0) then 1 else 0)) = n / 2) :
  (∑ k, ∑ l, (if (colors k l = 0) then (nums k l) else 0)) = (∑ k, ∑ l, (if (colors k l = 1) then (nums k l) else 0)) := by
Problem: putnam_2001_b2
Category: algebra

Find all pairs of real numbers $(x,y)$ satisfying the system of equations
\begin{align*}
\frac{1}{x}+\frac{1}{2y}&=(x^2+3y^2)(3x^2+y^2) \\
\frac{1}{x}-\frac{1}{2y}&=2(y^4-x^4).
\end{align*}

Solution: Show that $x=(3^{1/5}+1)/2$ and $y=(3^{1/5}-1)/2$ is the unique solution satisfying the given equations.

Lean 4 formalization:
import Mathlib

open Topology Filter Polynomial Set

abbrev putnam_2001_b2_solution : Set (ℝ × ℝ) := sorry
theorem putnam_2001_b2
    (x y : ℝ)
    (hx : x ≠ 0)
    (hy : y ≠ 0)
    (eq1 eq2 : Prop)
    (heq1 : eq1 ↔ (1 / x + 1 / (2 * y) = (x ^ 2 + 3 * y ^ 2) * (3 * x ^ 2 + y ^ 2)))
    (heq2 : eq2 ↔ (1 / x - 1 / (2 * y) = 2 * (y ^ 4 - x ^ 4))) :
    eq1 ∧ eq2 ↔ (x, y) ∈ putnam_2001_b2_solution := by
Problem: putnam_2001_b3
Category: analysis

For any positive integer $n$, let $\langle n \rangle$ denote the closest integer to $\sqrt{n}$. Evaluate $\sum_{n=1}^\infty \frac{2^{\langle n \rangle}+2^{-\langle n \rangle}}{2^n}$.

Solution: Show that the sum is $3$.

Lean 4 formalization:
import Mathlib

open Topology Filter Polynomial Set

abbrev putnam_2001_b3_solution : ℝ := sorry
theorem putnam_2001_b3
: ∑' n : Set.Ici 1, ((2 : ℝ) ^ (round (Real.sqrt n)) + (2 : ℝ) ^ (-round (Real.sqrt n))) / 2 ^ (n : ℝ) = putnam_2001_b3_solution := by
Problem: putnam_2001_b4
Category: algebra

Let $S$ denote the set of rational numbers different from $\{-1,0,1\}$.  Define $f:S\rightarrow S$ by $f(x)=x-1/x$. Prove or disprove that \[\bigcap_{n=1}^\infty f^{(n)}(S) = \emptyset,\] where $f^{(n)}$ denotes $f$ composed with itself $n$ times.


Lean 4 formalization:
import Mathlib

open Topology Filter Polynomial Set

abbrev putnam_2001_b4_solution : Prop := sorry
theorem putnam_2001_b4
(S : Set ℚ)
(hS : S = univ \ {-1, 0, 1})
(f : S → S)
(hf : ∀ x : S, f x = x - 1 / (x : ℚ))
: ⋂ n ∈ Ici 1, f^[n] '' univ = ∅ ↔ putnam_2001_b4_solution := by
Problem: putnam_2001_b5
Category: analysis

Let $a$ and $b$ be real numbers in the interval $(0,1/2)$, and let $g$ be a continuous real-valued function such that $g(g(x))=ag(x)+bx$ for all real $x$. Prove that $g(x)=cx$ for some constant $c$.


Lean 4 formalization:
import Mathlib

open Topology Filter Polynomial Set

theorem putnam_2001_b5
(a b : ℝ)
(g : ℝ → ℝ)
(abint : 0 < a ∧ a < 1 / 2 ∧ 0 < b ∧ b < 1 / 2)
(gcont : Continuous g)
(hg : ∀ x : ℝ, g (g x) = a * g x + b * x)
: ∃ c : ℝ, ∀ x : ℝ, g x = c * x := by
Problem: putnam_2001_b6
Category: analysis

Assume that $(a_n)_{n \geq 1}$ is an increasing sequence of positive real numbers such that $\lim a_n/n=0$. Must there exist infinitely many positive integers $n$ such that $a_{n-i}+a_{n+i}<2a_n$ for $i=1,2,\ldots,n-1$?

Solution: Show that the answer is yes, there must exist infinitely many such $n$.

Lean 4 formalization:
import Mathlib

open Topology Filter Polynomial Set

abbrev putnam_2001_b6_solution : Prop := sorry
theorem putnam_2001_b6 :
  (∀ a : ℤ → ℝ,
    (∀ n ≥ 1, a n > 0 ∧ a n < a (n + 1)) →
    (Tendsto (fun n : ℤ => a (n + 1) / (n + 1)) atTop (𝓝 0)) →
    {n : ℤ | n > 0 ∧ (∀ i ∈ Set.Icc 1 (n - 1), a (n - i) + a (n + i) < 2 * a n)}.Infinite)
  ↔ putnam_2001_b6_solution := by
Problem: putnam_2002_a1
Category: analysis, algebra

Let $k$ be a fixed positive integer. The $n$-th derivative of $\frac{1}{x^k-1}$ has the form $\frac{P_n(x)}{(x^k-1)^{n+1}}$ where $P_n(x)$ is a polynomial. Find $P_n(1)$.

Solution: Show that $P_n(1)=(-k)^nn!$ for all $n \geq 0$.

Lean 4 formalization:
import Mathlib

open Nat

abbrev putnam_2002_a1_solution : ℕ → ℕ → ℝ := sorry
theorem putnam_2002_a1
(k : ℕ)
(P : ℕ → Polynomial ℝ)
(kpos : k > 0)
(Pderiv : ∀ n x, iteratedDeriv n (fun x' : ℝ => 1 / (x' ^ k - 1)) x = ((P n).eval x) / ((x ^ k - 1) ^ (n + 1)))
: ∀ n, (P n).eval 1 = putnam_2002_a1_solution k n := by
Problem: putnam_2002_a2
Category: geometry

Given any five points on a sphere, show that some four of them must lie on a closed hemisphere.


Lean 4 formalization:
import Mathlib

open Nat Metric
open scoped InnerProductSpace

theorem putnam_2002_a2
(unit_sphere : Set (EuclideanSpace ℝ (Fin 3)))
(hsphere : unit_sphere = sphere 0 1)
(hemi : EuclideanSpace ℝ (Fin 3) → Set (EuclideanSpace ℝ (Fin 3)))
(hhemi : hemi = fun V ↦ {P : EuclideanSpace ℝ (Fin 3) | ⟪P, V⟫_ℝ ≥ 0})
: (∀ (S : Set (EuclideanSpace ℝ (Fin 3))), S ⊆ unit_sphere ∧ S.encard = 5 → ∃ V : EuclideanSpace ℝ (Fin 3), V ≠ 0 ∧ (S ∩ hemi V).encard ≥ 4) := by
Problem: putnam_2002_a3
Category: algebra

Let $n \geq 2$ be an integer and $T_n$ be the number of non-empty subsets $S$ of $\{1, 2, 3, \dots, n\}$ with the property that the average of the elements of $S$ is an integer. Prove that $T_n - n$ is always even.


Lean 4 formalization:
import Mathlib

open Nat

theorem putnam_2002_a3
(n Tn : ℤ)
(hn : n ≥ 2)
(hTn : Tn = Set.ncard {S : Set ℤ | S ⊆ Set.Icc 1 n ∧ Nonempty S ∧ ∃ k : ℤ, k = ((1 : ℝ) / S.ncard) * (∑' s : S, s.1)})
: Even (Tn - n) := by
Problem: putnam_2002_a5
Category: number_theory, algebra

Define a sequence by $a_0=1$, together with the rules
$a_{2n+1} = a_n$ and $a_{2n+2} = a_n + a_{n+1}$ for each
integer $n \geq 0$. Prove that every positive rational number
appears in the set
\[
\left\{ \frac{a_{n-1}}{a_n}: n \geq 1 \right\} =
\left\{ \frac{1}{1}, \frac{1}{2}, \frac{2}{1}, \frac{1}{3},
\frac{3}{2}, \dots \right\}.
\]


Lean 4 formalization:
import Mathlib

open Nat Set

theorem putnam_2002_a5
(a : ℕ → ℚ)
(ha : a 0 = 1 ∧ ∀ n : ℕ, a (2*n + 1) = a n ∧ a (2*n + 2) = a n + a (n + 1))
: ∀ q : ℚ, q > 0 → q ∈ {a (n - 1) / a n | n ∈ Ici 1} := by
Problem: putnam_2002_a6
Category: analysis, number_theory

Fix an integer $b \geq 2$. Let $f(1) = 1$, $f(2) = 2$, and for each
$n \geq 3$, define $f(n) = n f(d)$, where $d$ is the number of
base-$b$ digits of $n$. For which values of $b$ does
\[
\sum_{n=1}^\infty \frac{1}{f(n)}
\]
converge?

Solution: The sum converges for $b=2$ and diverges for $b \geq 3$.

Lean 4 formalization:
import Mathlib

open Nat Set Topology Filter

abbrev putnam_2002_a6_solution : Set ℕ := sorry
theorem putnam_2002_a6
(f : ℕ → ℕ → ℝ)
(hf : ∀ b : ℕ, f b 1 = 1 ∧ f b 2 = 2 ∧ ∀ n ∈ Ici 3, f b n = n * f b (Nat.digits b n).length)
: {b ∈ Ici 2 | ∃ L : ℝ, Tendsto (fun m : ℕ => ∑ n ∈ Finset.Icc 1 m, 1/(f b n)) atTop (𝓝 L)} = putnam_2002_a6_solution := by
Problem: putnam_2002_b3
Category: algebra

Show that, for all integers $n > 1$,
\[
\frac{1}{2ne} < \frac{1}{e} - \left( 1 - \frac{1}{n} \right)^n
< \frac{1}{ne}.
\]


Lean 4 formalization:
import Mathlib

open Nat Set Topology Filter

theorem putnam_2002_b3
(e : ℝ)
(he : e = Real.exp 1)
(f : ℤ → ℝ)
(hf : f = fun n : ℤ => 1/e - (1 - 1/n)^n)
: ∀ n : ℤ, n > 1 → 1/(2*n*e) < f n ∧ f n < 1/(n*e) := by
Problem: putnam_2002_b5
Category: number_theory

A palindrome in base $b$ is a positive integer whose base-$b$
digits read the same backwards and forwards; for example,
$2002$ is a 4-digit palindrome in base 10. Note that 200 is not
a palindrome in base 10, but it is the 3-digit palindrome
242 in base 9, and 404 in base 7. Prove that there is an integer
which is a 3-digit palindrome in base $b$ for at least 2002
different values of $b$.


Lean 4 formalization:
import Mathlib

open Nat Set Topology Filter

theorem putnam_2002_b5
: ∃ n : ℕ, {b : ℕ | b ≥ 1 ∧ (Nat.digits b n).length = 3 ∧ List.Palindrome (Nat.digits b n)}.ncard ≥ 2002 := by
Problem: putnam_2002_b6
Category: linear_algebra, number_theory, algebra

Let $p$ be a prime number. Prove that the determinant of the matrix
\[
\begin{pmatrix}
x & y & z \\
x^p & y^p & z^p \\
x^{p^2} & y^{p^2} & z^{p^2}
\end{pmatrix}
\]
is congruent modulo $p$ to a product of polynomials of the form
$ax+by+cz$, where $a,b,c$ are integers. (We say two integer
polynomials are congruent modulo $p$ if corresponding coefficients
are congruent modulo $p$.)


Lean 4 formalization:
import Mathlib

open Nat Set Topology Filter Matrix MvPolynomial

theorem putnam_2002_b6
(p : ℕ)
(hp : Nat.Prime p)
(M : Matrix (Fin 3) (Fin 3) (MvPolynomial (Fin 3) ℤ))
(hM : M = fun (r c : Fin 3) => ((X c)^(p^(r : ℕ)) : MvPolynomial (Fin 3) ℤ))
(cong : ℕ → MvPolynomial (Fin 3) ℤ × MvPolynomial (Fin 3) ℤ → Prop)
(hcong : cong = fun p : ℕ => fun (f, g) => ∀ n : Fin 3 →₀ ℕ, Int.ModEq p (f.coeff n) (g.coeff n))
: ∃ S : Finset (MvPolynomial (Fin 3) ℤ), cong p ((det M), (∏ s ∈ S, s)) ∧ ∀ s ∈ S, (∃ a b c : ℤ, s = (C a)*(X 0) + (C b)*(X 1) + (C c)*(X 2)) := by
Problem: putnam_2003_a1
Category: algebra

Let $n$ be a fixed positive integer. How many ways are there to write $n$ as a sum of positive integers, \[ n = a_1 + a_2 + \dots + a_k, \] with $k$ an arbitrary positive integer and $a_1 \leq a_2 \leq \dots \leq a_k \leq a_1 + 1$? For example, with $n = 4$, there are four ways: $4, 2 + 2, 1 + 1 + 2, 1 + 1 + 1 + 1$

Solution: Show that there are $n$ such sums.

Lean 4 formalization:
import Mathlib

open MvPolynomial

abbrev putnam_2003_a1_solution : ℕ → ℕ := sorry
theorem putnam_2003_a1
(n : ℕ) (hn : n > 0)
: Set.encard {a : ℕ → ℤ |
  ∃ k > 0, (∑ i : Fin k, a i = n) ∧
    (∀ i : Fin k, a i > 0) ∧
    (∀ i : Fin (k - 1), a i ≤ a (i + 1)) ∧
    a (k - 1) ≤ a 0 + 1 ∧ (∀ i ≥ k, a i = 0)}
  = putnam_2003_a1_solution n := by