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

Let $S$ be a set of $n$ distinct real numbers. Let $A_S$ be the set of numbers that occur as averages of two distinct elements of $S$. For a given $n \geq 2$, what is the smallest possible number of elements in $A_S$?

Solution: Show that the answer is $2n - 3$.

Lean 4 formalization:
import Mathlib

open Topology Filter Nat Function

abbrev putnam_1992_b1_solution : ℕ → ℤ := sorry
theorem putnam_1992_b1
  (n : ℕ) (hn : n ≥ 2)
  (A : Finset ℝ → Set ℝ)
  (hA : A = fun S ↦ {x | ∃ a ∈ S, ∃ b ∈ S, a ≠ b ∧ (a + b) / 2 = x}) :
  IsLeast {k : ℤ | ∃ S : Finset ℝ, S.card = n ∧ k = (A S).ncard} (putnam_1992_b1_solution n) := by
Problem: putnam_1992_b2
Category: algebra

For nonnegative integers $n$ and $k$, define $Q(n, k)$ to be the coefficient of $x^k$ in the expansion of $(1 + x + x^2 + x^3)^n$. Prove that
\[
Q(n, k) = \sum_{j=0}^k \binom{n}{j} \binom{n}{k-2j},
\]
where $\binom{a}{b}$ is the standard binomial coefficient. (Reminder: For integers $a$ and $b$ with $a \geq 0$, $\binom{a}{b} = \frac{a!}{b!(a-b)!}$ for $0 \leq b \leq a$, with $\binom{a}{b} = 0$ otherwise.)


Lean 4 formalization:
import Mathlib

open Topology Filter Nat Function Polynomial

theorem putnam_1992_b2
    (Q : ℕ → ℕ → ℕ)
    (hQ : Q = fun n k ↦ coeff ((1 + X + X ^ 2 + X ^ 3) ^ n) k)
    (n k : ℕ) :
    Q n k = ∑ j ∈ Finset.Iic k, choose n j * (if 2 * j ≤ k then choose n (k - 2 * j) else 0) := by
Problem: putnam_1992_b3
Category: geometry, analysis

For any pair $(x,y)$ of real numbers, a sequence $(a_n(x,y))_{n \geq 0}$ is defined as follows:
\begin{align*}
a_0(x,y)&=x, \\
a_{n+1}(x,y)&=\frac{(a_n(x,y))^2+y^2}{2},\text{ for $n \geq 0$.}
\end{align*}
Find the area of the region $\{(x,y) \mid (a_n(x,y))_{n \geq 0}\text{ converges}\}$.

Solution: Show that the area is $4+\pi$.

Lean 4 formalization:
import Mathlib

open Topology Filter Nat Function Polynomial

noncomputable abbrev putnam_1992_b3_solution : ℝ := sorry
theorem putnam_1992_b3
  (a : (Fin 2 → ℝ) → (ℕ → ℝ))
  (ha : ∀ p, (a p) 0 = p 0 ∧ (∀ n, (a p) (n + 1) = (((a p) n) ^ 2 + (p 1) ^ 2) / 2)) :
  putnam_1992_b3_solution = (MeasureTheory.volume {p | ∃ L, Tendsto (a p) atTop (𝓝 L)}).toReal := by
Problem: putnam_1992_b4
Category: algebra

Let $p(x)$ be a nonzero polynomial of degree less than $1992$ having no nonconstant factor in common with $x^3 - x$. Let
\[
\frac{d^{1992}}{dx^{1992}} \left( \frac{p(x)}{x^3 - x} \right) = \frac{f(x)}{g(x)}
\]
for polynomials $f(x)$ and $g(x)$. Find the smallest possible degree of $f(x)$.

Solution: Show that the minimum degree is $3984$.

Lean 4 formalization:
import Mathlib

open Topology Filter Nat Function Polynomial

abbrev putnam_1992_b4_solution : ℕ := sorry
theorem putnam_1992_b4
  (IsValid : Polynomial ℝ → Prop)
  (pair : Polynomial ℝ → Polynomial ℝ → Prop)
  (IsValid_def : ∀ p, IsValid p ↔ p ≠ 0 ∧ p.degree < 1992 ∧ IsCoprime p (X ^ 3 - X))
  (hpair : ∀ p f, pair p f ↔ ∃ g : Polynomial ℝ, iteratedDeriv 1992 (fun x ↦ p.eval x / (x ^ 3 - x)) = fun x ↦ f.eval x / g.eval x) :
  IsLeast {k : ℕ | ∃ p f, IsValid p ∧ pair p f ∧ k = f.degree} putnam_1992_b4_solution := by
Problem: putnam_1992_b5
Category: linear_algebra, analysis

Let $D_n$ denote the value of the $(n-1) \times (n-1)$ determinant
\[
\left[
\begin{array}{cccccc}
3 & 1 & 1 & 1 & \cdots & 1 \\
1 & 4 & 1 & 1 & \cdots & 1 \\
1 & 1 & 5 & 1 & \cdots & 1 \\
1 & 1 & 1 & 6 & \cdots & 1 \\
\vdots & \vdots & \vdots & \vdots & \ddots & \vdots \\
1 & 1 & 1 & 1 & \cdots & n+1
\end{array}
\right].
\]
Is the set $\left\{ \frac{D_n}{n!} \right\}_{n \geq 2}$ bounded?

Solution: Prove that the set is not bounded.

Lean 4 formalization:
import Mathlib

open Topology Filter Nat Function Polynomial

abbrev putnam_1992_b5_solution : Prop := sorry
theorem putnam_1992_b5
  (D : ℕ → ℚ)
  (hD : ∀ n, D n = Matrix.det (fun i j : Fin (n - 1) ↦ ite (i = j) ((i : ℕ) + 3 : ℚ) 1)) :
  putnam_1992_b5_solution ↔ (Bornology.IsBounded {x | ∃ n ≥ 2, D n / factorial n = x}) := by
Problem: putnam_1992_b6
Category: linear_algebra

Let $M$ be a set of real $n \times n$ matrices such that
\begin{itemize}
\item[(i)] $I \in M$, where $I$ is the $n \times n$ identity matrix;
\item[(ii)] if $A \in M$ and $B \in M$, then either $AB \in M$ or $-AB \in M$, but not both;
\item[(iii)] if $A \in M$ and $B \in M$, then either $AB = BA$ or $AB = -BA$;
\item[(iv)] if $A \in M$ and $A \neq I$, there is at least one $B \in M$ such that $AB = -BA$.
\end{itemize}
Prove that $M$ contains at most $n^2$ matrices.


Lean 4 formalization:
import Mathlib

open Topology Filter Nat Function Polynomial

theorem putnam_1992_b6
  (n : ℕ)
  (npos : 0 < n)
  (M : Set (Matrix (Fin n) (Fin n) ℝ))
  (h1 : 1 ∈ M)
  (h2 : ∀ A ∈ M, ∀ B ∈ M, Xor' (A * B ∈ M) (-A * B ∈ M))
  (h3 : ∀ A ∈ M, ∀ B ∈ M, (A * B = B * A) ∨ (A * B = -B * A))
  (h4 : ∀ A ∈ M, A ≠ 1 → ∃ B ∈ M, A * B = -B * A) :
  M.encard ≤ n ^ 2 := by
Problem: putnam_1993_a1
Category: analysis, algebra

The horizontal line $y=c$ intersects the curve $y=2x-3x^3$ in the first quadrant as in the figure. Find $c$ so that the areas of the two shaded regions are equal. [Figure not included. The first region is bounded by the $y$-axis, the line $y=c$ and the curve; the other lies under the curve and above the line $y=c$ between their two points of intersection.]

Solution: Show that the area of the two regions are equal when $c=4/9$.

Lean 4 formalization:
import Mathlib

noncomputable abbrev putnam_1993_a1_solution : ℝ := sorry
theorem putnam_1993_a1
: 0 < putnam_1993_a1_solution ∧ putnam_1993_a1_solution < (4 * Real.sqrt 2) / 9 ∧ (∫ x in Set.Ioo 0 ((Real.sqrt 2) / 3), max (putnam_1993_a1_solution - (2 * x - 3 * x ^ 3)) 0) = (∫ x in Set.Ioo 0 ((Real.sqrt 6) / 3), max ((2 * x - 3 * x ^ 3) - putnam_1993_a1_solution) 0) := by
Problem: putnam_1993_a2
Category: algebra

Let $(x_n)_{n \geq 0}$ be a sequence of nonzero real numbers such that $x_n^2-x_{n-1}x_{n+1}=1$ for $n=1,2,3,\dots$. Prove there exists a real number $a$ such that $x_{n+1}=ax_n-x_{n-1}$ for all $n \geq 1$.


Lean 4 formalization:
import Mathlib

theorem putnam_1993_a2
(x : ℕ → ℝ)
(xnonzero : ∀ n : ℕ, x n ≠ 0)
(hx : ∀ n ≥ 1, (x n) ^ 2 - x (n - 1) * x (n + 1) = 1)
: ∃ a : ℝ, ∀ n ≥ 1, x (n + 1) = a * x n - x (n - 1) := by
Problem: putnam_1993_a3
Category: algebra

Let $\mathcal{P}_n$ be the set of subsets of $\{1,2,\dots,n\}$. Let $c(n,m)$ be the number of functions $f:\mathcal{P}_n \to \{1,2,\dots,m\}$ such that $f(A \cap B)=\min\{f(A),f(B)\}$. Prove that $c(n,m)=\sum_{j=1}^m j^n$.


Lean 4 formalization:
import Mathlib

theorem putnam_1993_a3
(c : ℕ → ℕ → ℕ)
(hc : ∀ n ≥ 1, ∀ m ≥ 1, c n m = {f : Finset (Fin n) → Fin m | ∀ A B : Finset (Fin n), f (A ∩ B) = min (f A) (f B)}.encard)
: ∀ n ≥ 1, ∀ m ≥ 1, c n m = ∑' j : Set.Icc 1 m, (j : ℤ) ^ n := by
Problem: putnam_1993_a4
Category: algebra

Let $x_1,x_2,\dots,x_{19}$ be positive integers each of which is less than or equal to $93$. Let $y_1,y_2,\dots,y_{93}$ be positive integers each of which is less than or equal to $19$. Prove that there exists a (nonempty) sum of some $x_i$'s equal to a sum of some $y_j$'s.


Lean 4 formalization:
import Mathlib

theorem putnam_1993_a4
  (x : Fin 19 → ℤ)
  (y : Fin 93 → ℤ)
  (hx : ∀ i, 0 < x i ∧ x i ≤ 93)
  (hy : ∀ j, 0 < y j ∧ y j ≤ 19) :
  ∃ (is : Finset (Fin 19)) (js : Finset (Fin 93)),
    is ≠ ∅ ∧ (∑ i : is, x i) = (∑ j : js, y j) := by
Problem: putnam_1993_a5
Category: analysis

Show that $\int_{-100}^{-10} (\frac{x^2-x}{x^3-3x+1})^2\,dx+\int_{\frac{1}{101}}^{\frac{1}{11}} (\frac{x^2-x}{x^3-3x+1})^2\,dx+\int_{\frac{101}{100}}^{\frac{11}{10}} (\frac{x^2-x}{x^3-3x+1})^2\,dx$ is a rational number.


Lean 4 formalization:
import Mathlib

theorem putnam_1993_a5
: ¬Irrational ((∫ x in Set.Ioo (-100) (-10), (((x ^ 2 - x) / (x ^ 3 - 3 * x + 1)) ^ 2)) + (∫ x in Set.Ioo (1 / 101) (1 / 11), (((x ^ 2 - x) / (x ^ 3 - 3 * x + 1)) ^ 2)) + (∫ x in Set.Ioo (101 / 100) (11 / 10), (((x ^ 2 - x) / (x ^ 3 - 3 * x + 1)) ^ 2))) := by
Problem: putnam_1993_a6
Category: algebra

The infinite sequence of $2$'s and $3$'s $2,3,3,2,3,3,3,2,3,3,3,2,3,3,2,3,3,3,2,3,3,3,2,3,3,3,2,3,3,2,3,3,3,2,\dots$ has the property that, if one forms a second sequence that records the number of $3$'s between successive $2$'s, the result is identical to the given sequence. Show that there exists a real number $r$ such that, for any $n$, the $n$th term of the sequence is $2$ if and only if $n=1+\lfloor rm \rfloor$ for some nonnegative integer $m$. (Note: $\lfloor x \rfloor$ denotes the largest integer less than or equal to $x$.)


Lean 4 formalization:
import Mathlib

theorem putnam_1993_a6
(seq : ℕ → ℤ)
(hseq23 : ∀ n, seq n = 2 ∨ seq n = 3)
(hseq2inds : ∀ n, seq n = 2 ↔ (∃ N : ℕ, n = ∑ i : Fin N, (seq i + 1)))
: ∃ r : ℝ, ∀ n, seq n = 2 ↔ (∃ m : ℤ, n + 1 = 1 + Int.floor (r * m)) := by
Problem: putnam_1993_b1
Category: algebra

Find the smallest positive integer $n$ such that for every integer $m$ with $0<m<1993$, there exists an integer $k$ for which $\frac{m}{1993}<\frac{k}{n}<\frac{m+1}{1994}$.

Solution: Show that the smallest positive integer $n$ satisfying the condition is $n=3987$.

Lean 4 formalization:
import Mathlib

abbrev putnam_1993_b1_solution : ℕ := sorry
theorem putnam_1993_b1 :
    IsLeast
    {n : ℕ | 0 < n ∧
      ∀ m ∈ Set.Ioo (0 : ℤ) (1993), ∃ k : ℤ,
      (m / 1993 < (k : ℝ) / n) ∧ ((k : ℝ) / n < (m + 1) / 1994) }
    putnam_1993_b1_solution := by
Problem: putnam_1993_b3
Category: probability, number_theory, geometry

Two real numbers $x$ and $y$ are chosen at random in the interval $(0,1)$ with respect to the uniform distribution. What is the probability that the closest integer to $x/y$ is even? Express the answer in the form $r+s\pi$, where $r$ and $s$ are rational numbers.

Solution: Show that the limit is $(5-\pi)/4$. That is, $r=5/4$ and $s=-1/4$.

Lean 4 formalization:
import Mathlib

abbrev putnam_1993_b3_solution : ℚ × ℚ := sorry
theorem putnam_1993_b3 :
  let (r, s) := putnam_1993_b3_solution;
  (MeasureTheory.volume
    {p : Fin 2 → ℝ | 0 < p ∧ p < 1 ∧ Even (round (p 0 / p 1))}
  ).toReal
  = r + s * Real.pi := by
Problem: putnam_1993_b4
Category: analysis

The function $K(x,y)$ is positive and continuous for $0 \leq x \leq 1,0 \leq y \leq 1$, and the functions $f(x)$ and $g(x)$ are positive and continuous for $0 \leq x \leq 1$. Suppose that for all $x$, $0 \leq x \leq 1$, $\int_0^1 f(y)K(x,y)\,dy=g(x)$ and $\int_0^1 g(y)K(x,y)\,dy=f(x)$. Show that $f(x)=g(x)$ for $0 \leq x \leq 1$.


Lean 4 formalization:
import Mathlib

theorem putnam_1993_b4
(K : ℝ × ℝ → ℝ)
(f g : ℝ → ℝ)
(Kpos : ∀ x y : Set.Icc (0 : ℝ) 1, K (x, y) > 0)
(Kcont : ContinuousOn K {(x, y) : ℝ × ℝ | x ∈ Set.Icc 0 1 ∧ y ∈ Set.Icc 0 1})
(fgpos : ∀ x : Set.Icc (0 : ℝ) 1, f x > 0 ∧ g x > 0)
(fgcont : ContinuousOn f (Set.Icc 0 1) ∧ ContinuousOn g (Set.Icc 0 1))
(fgint : ∀ x : Set.Icc (0 : ℝ) 1, (∫ y in Set.Ioo 0 1, f y * K (x, y)) = g x ∧ (∫ y in Set.Ioo 0 1, g y * K (x, y)) = f x)
: ∀ x : Set.Icc (0 : ℝ) 1, f x = g x := by
Problem: putnam_1993_b5
Category: geometry, number_theory, linear_algebra

Show there do not exist four points in the Euclidean plane such that the pairwise distances between the points are all odd integers.


Lean 4 formalization:
import Mathlib

theorem putnam_1993_b5:
  ¬∃ p : Fin 4 → (EuclideanSpace ℝ (Fin 2)),
    ∀ i j, i ≠ j →
      (∃ n : ℤ, dist (p i) (p j) = n ∧ Odd n) := by
Problem: putnam_1993_b6
Category: algebra

Let $S$ be a set of three, not necessarily distinct, positive integers. Show that one can transform $S$ into a set containing $0$ by a finite number of applications of the following rule: Select two of the three integers, say $x$ and $y$, where $x \leq y$ and replace them with $2x$ and $y-x$.


Lean 4 formalization:
import Mathlib

theorem putnam_1993_b6
(S : Fin 3 → ℕ)
(f : Fin 3 → Fin 3 → (Fin 3 → ℕ) → (Fin 3 → ℕ))
(Spos : ∀ i : Fin 3, S i > 0)
(hf : ∀ i j k : Fin 3, (i ≠ j ∧ i ≠ k ∧ j ≠ k) → ∀ S' : Fin 3 → ℕ, if S' i ≤ S' j then ((f i j S') i = 2 * S' i ∧ (f i j S') j = S' j - S' i ∧ (f i j S') k = S' k) else (f i j S' = S'))
: ∃ (Ss : ℕ → (Fin 3 → ℕ)) (N : ℕ), Ss 0 = S ∧ (∃ i : Fin 3, Ss N i = 0) ∧ (∀ n : Fin N, ∃ i j : Fin 3, i ≠ j ∧ f i j (Ss n) = Ss ((n : ℕ) + 1)) := by
Problem: putnam_1994_a1
Category: analysis

Suppose that a sequence $a_1,a_2,a_3,\dots$ satisfies $0<a_n \leq a_{2n}+a_{2n+1}$ for all $n \geq 1$. Prove that the series $\sum_{n=1}^\infty a_n$ diverges.


Lean 4 formalization:
import Mathlib

open Filter Topology

theorem putnam_1994_a1
    (a : ℕ → ℝ)
    (ha : ∀ n ≥ 1, 0 < a n ∧ a n ≤ a (2 * n) + a (2 * n + 1)) :
    Tendsto (fun N : ℕ => ∑ n : Set.Icc 1 N, a n) atTop atTop := by
Problem: putnam_1994_a3
Category: geometry

Show that if the points of an isosceles right triangle of side length $1$ are each colored with one of four colors, then there must be two points of the same color which are at least a distance $2-\sqrt{2}$ apart.


Lean 4 formalization:
import Mathlib

open Filter Topology

theorem putnam_1994_a3
(T : Set (EuclideanSpace ℝ (Fin 2)))
(hT : T = convexHull ℝ {!₂[0,0], !₂[1,0], !₂[0,1]})
(Tcolors : T → Fin 4)
: ∃ p q : T, Tcolors p = Tcolors q ∧ dist p.1 q.1 ≥ 2 - Real.sqrt 2 := by
Problem: putnam_1994_a4
Category: linear_algebra

Let $A$ and $B$ be $2 \times 2$ matrices with integer entries such that $A$, $A+B$, $A+2B$, $A+3B$, and $A+4B$ are all invertible matrices whose inverses have integer entries. Show that $A+5B$ is invertible and that its inverse has integer entries.


Lean 4 formalization:
import Mathlib

open Filter Topology

theorem putnam_1994_a4
  (A B : Matrix (Fin 2) (Fin 2) ℤ)
  (ABinv : Nonempty (Invertible A) ∧
    Nonempty (Invertible (A + B)) ∧
    Nonempty (Invertible (A + 2 * B)) ∧
    Nonempty (Invertible (A + 3 * B)) ∧
    Nonempty (Invertible (A + 4 * B)))
  : Nonempty (Invertible (A + 5 * B)) := by
Problem: putnam_1994_a5
Category: analysis

Let $(r_n)_{n \geq 0}$ be a sequence of positive real numbers such that $\lim_{n \to \infty} r_n=0$. Let $S$ be the set of numbers representable as a sum $r_{i_1}+r_{i_2}+\cdots+r_{i_{1994}}$, with $i_1<i_2<\cdots<i_{1994}$. Show that every nonempty interval $(a,b)$ contains a nonempty subinterval $(c,d)$ that does not intersect $S$.


Lean 4 formalization:
import Mathlib

open Filter Topology

theorem putnam_1994_a5
  (r : ℕ → ℝ)
  (S : Set ℝ)
  (rpos : ∀ n, r n > 0)
  (rlim : Tendsto r atTop (𝓝 0))
  (hS : S = {x | ∃ i : Fin 1994 → ℕ, (∀ j k : Fin 1994, j < k → i j < i k) ∧ (x = ∑ j : Fin 1994, r (i j))}) :
  ∀ a b : ℝ, a < b → (∃ c d : ℝ, a ≤ c ∧ c < d ∧ d ≤ b ∧ (Set.Ioo c d) ∩ S = ∅) := by
Problem: putnam_1994_a6
Category: algebra

Let $f_1,\dots,f_{10}$ be bijections of the set of integers such that for each integer $n$, there is some composition $f_{i_1} \circ f_{i_2} \circ \cdots \circ f_{i_m}$ of these functions (allowing repetitions) which maps 0 to $n$. Consider the set of $1024$ functions $\mathcal{F}=\{f_1^{e_1} \circ f_2^{e_2} \circ \cdots \circ f_{10}^{e_{10}}\}$, $e_i=0$ or $1$ for $1 \leq i \leq 10$. ($f_i^0$ is the identity function and $f_i^1=f_i$.) Show that if $A$ is any nonempty finite set of integers, then at most $512$ of the functions in $\mathcal{F}$ map $A$ to itself.


Lean 4 formalization:
import Mathlib

open Classical Filter Topology

theorem putnam_1994_a6
(f : Fin 10 → Equiv.Perm ℤ)
(mijcomp : ℕ → (ℕ → Fin 10) → ℕ → (ℤ → ℤ))
(F : Finset (ℤ → ℤ))
(hf: ∀ n : ℤ, ∃ m : ℕ, ∃ i : ℕ → Fin 10, m ≥ 1 ∧ (mijcomp m i 0) 0 = n)
(hmijcomp : ∀ m ≥ 1, ∀ (i : ℕ → Fin 10) (j : Fin m), mijcomp m i j = if (j = m - 1) then (f (i j) : ℤ → ℤ) else (f (i j) ∘ mijcomp m i (j + 1)))
(hF : F = {g : ℤ → ℤ | ∃ e : Fin 10 → Fin 2, g = (f 0)^[e 0] ∘ (f 1)^[e 1] ∘ (f 2)^[e 2] ∘ (f 3)^[e 3] ∘ (f 4)^[e 4] ∘ (f 5)^[e 5] ∘ (f 6)^[e 6] ∘ (f 7)^[e 7] ∘ (f 8)^[e 8] ∘ (f 9)^[e 9]})
: ∀ A : Finset ℤ, A.Nonempty → {g ∈ F | g '' A = A}.card ≤ 512 := by
Problem: putnam_1994_b1
Category: algebra

Find all positive integers $n$ that are within $250$ of exactly $15$ perfect squares.

Solution: Show that an integer $n$ is within $250$ of exactly $15$ perfect squares if and only if either $315 \leq n \leq 325$ or $332 \leq n \leq 350$.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_1994_b1_solution : Set ℤ := sorry
theorem putnam_1994_b1
    (n : ℤ) :
    n ∈ putnam_1994_b1_solution ↔
    (0 < n ∧ {m : ℕ | |n - m ^ 2| ≤ 250}.encard = 15) := by
Problem: putnam_1994_b2
Category: geometry, algebra

For which real numbers $c$ is there a straight line that intersects the curve $x^4+9x^3+cx^2+9x+4$ in four distinct points?

Solution: Show that there exists such a line if and only if $c<243/8$.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_1994_b2_solution : Set ℝ := sorry
theorem putnam_1994_b2
  (c : ℝ) :
  (∃ m b : ℝ,
    {x : ℝ | m * x + b = x ^ 4 + 9 * x ^ 3 + c * x ^ 2 + 9 * x + 4}.encard = 4)
  ↔ c ∈ putnam_1994_b2_solution := by
Problem: putnam_1994_b3
Category: analysis

Find the set of all real numbers $k$ with the following property: For any positive, differentiable function $f$ that satisfies $f'(x)>f(x)$ for all $x$, there is some number $N$ such that $f(x)>e^{kx}$ for all $x>N$.

Solution: Show that the desired set is $(-\infty,1)$.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_1994_b3_solution : Set ℝ := sorry
theorem putnam_1994_b3 :
    {k | ∀ f (hf : (∀ x, 0 < f x ∧ f x < deriv f x) ∧ Differentiable ℝ f),
      ∃ N, ∀ x > N, Real.exp (k * x) < f x} = putnam_1994_b3_solution := by
Problem: putnam_1994_b4
Category: linear_algebra, number_theory, analysis

For $n \geq 1$, let $d_n$ be the greatest common divisor of the entries of $A^n-I$, where $A=\begin{pmatrix} 3 & 2 \\ 4 & 3 \end{pmatrix}$ and $I=\begin{pmatrix} 1 & 0 \\ 0 & 1 \end{pmatrix}$. Show that $\lim_{n \to \infty} d_n=\infty$.


Lean 4 formalization:
import Mathlib

open Filter Topology

theorem putnam_1994_b4
(matgcd : Matrix (Fin 2) (Fin 2) ℤ → ℤ)
(A : Matrix (Fin 2) (Fin 2) ℤ)
(d : ℕ → ℤ)
(hmatgcd : ∀ M, matgcd M = Int.gcd (Int.gcd (Int.gcd (M 0 0) (M 0 1)) (M 1 0)) (M 1 1))
(hA : A 0 0 = 3 ∧ A 0 1 = 2 ∧ A 1 0 = 4 ∧ A 1 1 = 3)
(hd : ∀ n ≥ 1, d n = matgcd (A ^ n - 1))
: Tendsto d atTop atTop := by
Problem: putnam_1994_b5
Category: algebra

For any real number $\alpha$, define the function $f_\alpha(x)=\lfloor \alpha x \rfloor$. Let $n$ be a positive integer. Show that there exists an $\alpha$ such that for $1 \leq k \leq n$, $f_\alpha^k(n^2)=n^2-k=f_{\alpha^k}(n^2)$.


Lean 4 formalization:
import Mathlib

open Filter Topology

theorem putnam_1994_b5
  (n : ℕ) (hn : n > 0)
  (f : ℝ → ℤ → ℤ)
  (hf : ∀ (α : ℝ) (x : ℤ), f α x = Int.floor (α * x)) :
  ∃ α : ℝ,
    ∀ k ∈ Set.Icc 1 n,
      ((f α)^[k] (n ^ 2) = n ^ 2 - k) ∧
      (f (α ^ k) (n ^ 2) = n ^ 2 - k) := by
Problem: putnam_1994_b6
Category: number_theory

For any integer $a$, set $n_a=101a-100 \cdot 2^a$. Show that for $0 \leq a,b,c,d \leq 99$, $n_a+n_b \equiv n_c+n_d \pmod{10100}$ implies $\{a,b\}=\{c,d\}$.


Lean 4 formalization:
import Mathlib

open Filter Topology

theorem putnam_1994_b6
(n : ℕ → ℤ)
(hn : ∀ a : ℕ, n a = 101 * a - 100 * 2 ^ a)
: ∀ a b c d : Set.Icc 0 99, (n a + n b ≡ n c + n d [ZMOD 10100]) → (({a, b} : Set (Set.Icc 0 99)) = {c, d}) := by
Problem: putnam_1995_a1
Category: algebra

Let $S$ be a set of real numbers which is closed under multiplication (that is, if $a$ and $b$ are in $S$, then so is $ab$). Let $T$ and $U$ be disjoint subsets of $S$ whose union is $S$. Given that the product of any {\em three} (not necessarily distinct) elements of $T$ is in $T$ and that the product of any three elements of $U$ is in $U$, show that at least one of the two subsets $T,U$ is closed under multiplication.


Lean 4 formalization:
import Mathlib

theorem putnam_1995_a1
(S : Set ℝ)
(hS : ∀ a ∈ S, ∀ b ∈ S, a * b ∈ S)
(T U : Set ℝ)
(hsub : T ⊆ S ∧ U ⊆ S)
(hunion : T ∪ U = S)
(hdisj : T ∩ U = ∅)
(hT3 : ∀ a ∈ T, ∀ b ∈ T, ∀ c ∈ T, a * b * c ∈ T)
(hU3 : ∀ a ∈ U, ∀ b ∈ U, ∀ c ∈ U, a * b * c ∈ U)
: (∀ a ∈ T, ∀ b ∈ T, a * b ∈ T) ∨ (∀ a ∈ U, ∀ b ∈ U, a * b ∈ U) := by
Problem: putnam_1995_a2
Category: analysis

For what pairs $(a,b)$ of positive real numbers does the improper integral \[ \int_{b}^{\infty} \left( \sqrt{\sqrt{x+a}-\sqrt{x}} - \sqrt{\sqrt{x}-\sqrt{x-b}} \right)\,dx \] converge?

Solution: Show that the solution is those pairs $(a,b)$ where $a = b$.

Lean 4 formalization:
import Mathlib

open Filter Topology Real

abbrev putnam_1995_a2_solution : Set (ℝ × ℝ) := sorry
theorem putnam_1995_a2
(habconv : (ℝ × ℝ) → Prop)
(habconv_def : habconv = fun ⟨a,b⟩ =>
∃ limit : ℝ, Tendsto (fun t : ℝ => ∫ x in (Set.Icc b t), (sqrt (sqrt (x + a) - sqrt x) - sqrt (sqrt x - sqrt (x - b)))) atTop (𝓝 limit))
: ∀ ab : ℝ × ℝ, ab.1 > 0 ∧ ab.2 > 0 → (habconv ab ↔ ab ∈ putnam_1995_a2_solution) := by
Problem: putnam_1995_a3
Category: number_theory

The number $d_{1}d_{2}\dots d_{9}$ has nine (not necessarily distinct) decimal digits. The number $e_{1}e_{2}\dots e_{9}$ is such that each of the nine 9-digit numbers formed by replacing just one of the digits $d_{i}$ is $d_{1}d_{2}\dots d_{9}$ by the corresponding digit $e_{i}$ ($1 \leq i \leq 9$) is divisible by 7. The number $f_{1}f_{2}\dots f_{9}$ is related to $e_{1}e_{2}\dots e_{9}$ is the same way: that is, each of the nine numbers formed by replacing one of the $e_{i}$ by the corresponding $f_{i}$ is divisible by 7. Show that, for each $i$, $d_{i}-f_{i}$ is divisible by 7. [For example, if $d_{1}d_{2}\dots d_{9} = 199501996$, then $e_{6}$ may be 2 or 9, since $199502996$ and $199509996$ are multiples of 7.]


Lean 4 formalization:
import Mathlib

open Filter Topology Real

theorem putnam_1995_a3
(relation : (Fin 9 → ℤ) → (Fin 9 → ℤ) → Prop)
(digits_to_num : (Fin 9 → ℤ) → ℤ)
(hdigits_to_num : digits_to_num = fun dig => ∑ i : Fin 9, (dig i) * 10^i.1)
(hrelation : ∀ d e : (Fin 9 → ℤ), relation d e ↔ (∀ i : Fin 9, d i < 10 ∧ d i ≥ 0 ∧ e i < 10 ∧ e i ≥ 0) ∧ (∀ i : Fin 9, 7 ∣ (digits_to_num (fun j : Fin 9 => if j = i then e j else d j))))
: ∀ d e f : (Fin 9 → ℤ), ((relation d e) ∧ (relation e f)) → (∀ i : Fin 9, 7 ∣ d i - f i) := by
Problem: putnam_1995_a4
Category: combinatorics

Suppose we have a necklace of $n$ beads. Each bead is labeled with an integer and the sum of all these labels is $n-1$. Prove that we can cut the necklace to form a string whose consecutive labels $x_{1},x\_{2},\dots,x_{n}$ satisfy \[\sum_{i=1}^{k} x_{i} \leq k-1 \qquad \mbox{for} \quad k=1,2,\dots,n.\]


Lean 4 formalization:
import Mathlib

open Filter Topology Real

theorem putnam_1995_a4
(n : ℕ)
(hn : n > 0)
(necklace : Fin n → ℤ)
(hnecklacesum : ∑ i : Fin n, necklace i = n - 1)
: ∃ cut, ∀ k, ∑ i : {j : Fin n | j.1 ≤ k}, necklace (cut + i) ≤ k := by
Problem: putnam_1995_a5
Category: linear_algebra, analysis

Let $x_{1},x_{2},\dots,x_{n}$ be differentiable (real-valued) functions of a single variable $f$ which satisfy \begin{align*} \frac{dx_{1}}{dt} &= a_{11}x_{1} + a_{12}x_{2} + \cdots + a_{1n}x_{n} \ \frac{dx_{2}}{dt} &= a_{21}x_{1} + a_{22}x_{2} + \cdots + a_{2n}x_{n} \ \vdots && \vdots \ \frac{dx_{n}}{dt} &= a_{n1}x_{1} + a_{n2}x_{2} + \cdots + a_{nn}x_{n} \end{align*} for some constants $a_{ij}>0$. Suppose that for all $i$, $x_{i}(t) \to 0$ as $t \to \infty$. Are the functions $x_{1},x_{2},\dots,x_{n}$ necessarily linearly dependent?

Solution: Show that the answer is yes, the functions must be linearly dependent.

Lean 4 formalization:
import Mathlib

open Filter Topology Real

abbrev putnam_1995_a5_solution : Prop := sorry
theorem putnam_1995_a5 :
  putnam_1995_a5_solution ↔
  (∀ (n : ℕ) (x : Fin n → (ℝ → ℝ)) (a : Fin n → Fin n → ℝ),
    (0 < n) →
    (∀ i, Differentiable ℝ (x i)) →
    (∀ i j, a i j > 0) →
    (∀ t i, (deriv (x i)) t = ∑ j : Fin n, (a i j) * ((x j) t)) →
    (∀ i, Tendsto (x i) atTop (𝓝 0)) →
    ¬(∀ b : Fin n → ℝ, (∀ t : ℝ, ∑ i : Fin n, (b i) * ((x i) t) = 0) →
      (∀ i, b i = 0))) := by