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

Let $a_1, a_2, \dots, a_n$ be real numbers, and let $b_1, b_2, \dots, b_n$ be distinct positive integers. Suppose that there is a polynomial $f(x)$ satisfying the identity
\[
(1-x)^n f(x) = 1 + \sum_{i=1}^n a_i x^{b_i}.
\]
Find a simple expression (not involving any sums) for $f(1)$ in terms of $b_1, b_2, \dots, b_n$ and $n$ (but independent of $a_1, a_2, \dots, a_n$).

Solution: Show that $f(1) = b_1 b_2 \dots b_n / n!$.

Lean 4 formalization:
import Mathlib

open  Real Equiv

noncomputable abbrev putnam_1986_a6_solution : (ℕ → ℕ) → ℕ → ℝ := sorry
theorem putnam_1986_a6
(n : ℕ)
(npos : n > 0)
(a : ℕ → ℝ)
(b : ℕ → ℕ)
(bpos : ∀ i ∈ Finset.Icc 1 n, b i > 0)
(binj : ∀ i ∈ Finset.Icc 1 n, ∀ j ∈ Finset.Icc 1 n, b i = b j → i = j)
(f : Polynomial ℝ)
(hf : ∀ x : ℝ, (1 - x) ^ n * f.eval x = 1 + ∑ i : Finset.Icc 1 n, (a i) * x ^ (b i))
: (f.eval 1 = putnam_1986_a6_solution b n) := by
Problem: putnam_1986_b1
Category: geometry, algebra

Inscribe a rectangle of base $b$ and height $h$ and an isosceles triangle of base $b$ (against a corresponding side of the rectangle and pointed in the other direction) in a circle of radius one. For what value of $h$ do the rectangle and triangle have the same area?

Solution: Show that the only such value of $h$ is $2/5$.

Lean 4 formalization:
import Mathlib

open  Real Equiv

noncomputable abbrev putnam_1986_b1_solution : ℝ := sorry
theorem putnam_1986_b1
(b h : ℝ)
(hbh : b > 0 ∧ h > 0 ∧ b ^ 2 + h ^ 2 = 2 ^ 2)
(areaeq : b * h = 0.5 * b * (1 - h / 2))
: h = putnam_1986_b1_solution := by
Problem: putnam_1986_b2
Category: algebra

Prove that there are only a finite number of possibilities for the ordered triple $T=(x-y,y-z,z-x)$, where $x,y,z$ are complex numbers satisfying the simultaneous equations
\[
x(x-1)+2yz = y(y-1)+2zx = z(z-1)+2xy,
\]
and list all such triples $T$.

Solution: Show that the possibilities for $T$ are $(0, 0, 0), \, (0, -1, 1), \, (1, 0, -1), \, (-1, 1, 0)$.

Lean 4 formalization:
import Mathlib

open  Real Equiv

noncomputable abbrev putnam_1986_b2_solution : Finset (ℂ × ℂ × ℂ) := sorry
theorem putnam_1986_b2
: ({T : ℂ × ℂ × ℂ | ∃ x y z : ℂ, T = (x - y, y - z, z - x) ∧ x * (x - 1) + 2 * y * z = y * (y - 1) + 2 * z * x ∧ y * (y - 1) + 2 * z * x = z * (z - 1) + 2 * x * y} = putnam_1986_b2_solution) := by
Problem: putnam_1986_b3
Category: number_theory, algebra

Let $\Gamma$ consist of all polynomials in $x$ with integer coefficients. For $f$ and $g$ in $\Gamma$ and $m$ a positive integer, let $f \equiv g \pmod{m}$ mean that every coefficient of $f-g$ is an integral multiple of $m$. Let $n$ and $p$ be positive integers with $p$ prime. Given that $f,g,h,r$ and $s$ are in $\Gamma$ with $rf+sg\equiv 1 \pmod{p}$ and $fg \equiv h \pmod{p}$, prove that there exist $F$ and $G$ in $\Gamma$ with $F \equiv f \pmod{p}$, $G \equiv g \pmod{p}$, and $FG \equiv h \pmod{p^n}$.


Lean 4 formalization:
import Mathlib

open  Real Equiv Polynomial

theorem putnam_1986_b3
    (n p : ℕ)
    (nppos : n > 0 ∧ p > 0)
    (pprime : Nat.Prime p)
    (cong : Polynomial ℤ → Polynomial ℤ → ℤ → Prop)
    (hcong : ∀ f g m, cong f g m ↔ ∀ i : ℕ, m ∣ (f - g).coeff i)
    (f g h r s : Polynomial ℤ)
    (hcoprime : cong (r * f + s * g) 1 p)
    (hprod : cong (f * g) h p)
    : (∃ F G : Polynomial ℤ, cong F f p ∧ cong G g p ∧ cong (F * G) h (p ^ n)) := by
Problem: putnam_1986_b4
Category: analysis

For a positive real number $r$, let $G(r)$ be the minimum value of $|r - \sqrt{m^2+2n^2}|$ for all integers $m$ and $n$. Prove or disprove the assertion that $\lim_{r\to \infty}G(r)$ exists and equals $0$.

Solution: Show that the limit exists and equals $0$.

Lean 4 formalization:
import Mathlib

open  Real Equiv Polynomial Filter Topology

abbrev putnam_1986_b4_solution : Prop := sorry
theorem putnam_1986_b4
(G : ℝ → ℝ)
(hGeq : ∀ r : ℝ, ∃ m n : ℤ, G r = |r - sqrt (m ^ 2 + 2 * n ^ 2)|)
(hGlb : ∀ r : ℝ, ∀ m n : ℤ, G r ≤ |r - sqrt (m ^ 2 + 2 * n ^ 2)|)
: (Tendsto G atTop (𝓝 0) ↔ putnam_1986_b4_solution) := by
Problem: putnam_1986_b5
Category: algebra

Let $f(x,y,z) = x^2+y^2+z^2+xyz$. Let $p(x,y,z), q(x,y,z)$, $r(x,y,z)$ be polynomials with real coefficients satisfying
\[
f(p(x,y,z), q(x,y,z), r(x,y,z)) = f(x,y,z).
\]
Prove or disprove the assertion that the sequence $p,q,r$ consists of some permutation of $\pm x, \pm y, \pm z$, where the number of minus signs is $0$ or $2$.

Solution: Prove that the assertion is false.

Lean 4 formalization:
import Mathlib

open  Real Equiv Polynomial Filter Topology MvPolynomial

abbrev putnam_1986_b5_solution : Prop := sorry
theorem putnam_1986_b5
    (f : MvPolynomial (Fin 3) ℝ)
    (perms : Set (Set (MvPolynomial (Fin 3) ℝ)))
    (hf : f = (X 0) ^ 2 + (X 1) ^ 2 + (X 2) ^ 2 + (X 0) * (X 1) * (X 2))
    (hperms : perms = {{X 0, X 1, X 2}, {X 0, -X 1, -X 2}, {-X 0, X 1, -X 2}, {-X 0, -X 1, X 2}}) :
    putnam_1986_b5_solution ↔ (∀ pqr : Fin 3 → MvPolynomial (Fin 3) ℝ,
      (∀ xyz : Fin 3 → ℝ, MvPolynomial.eval (fun i ↦ MvPolynomial.eval xyz (pqr i)) f = MvPolynomial.eval xyz f) →
      ({pqr 0, pqr 1, pqr 2} ∈ perms)) := by
Problem: putnam_1986_b6
Category: linear_algebra

Suppose $A,B,C,D$ are $n \times n$ matrices with entries in a field $F$, satisfying the conditions that $AB^T$ and $CD^T$ are symmetric and $AD^T - BC^T = I$. Here $I$ is the $n \times n$ identity matrix, and if $M$ is an $n \times n$ matrix, $M^T$ is its transpose. Prove that $A^T D - C^T B = I$.


Lean 4 formalization:
import Mathlib

open  Real Equiv Polynomial Filter Topology MvPolynomial Matrix

theorem putnam_1986_b6
(n : ℕ)
(npos : n > 0)
(F : Type*) [Field F]
(A B C D : Matrix (Fin n) (Fin n) F)
(hsymm : IsSymm (A * Bᵀ) ∧ IsSymm (C * Dᵀ))
(hid : A * Dᵀ - B * Cᵀ = 1)
: (Aᵀ * D - Cᵀ * B = 1) := by
Problem: putnam_1987_a1
Category: algebra

Curves $A$, $B$, $C$, and $D$ are defined in the plane as follows:
\begin{align*}
A&=\left\{ (x,y):x^2-y^2=\frac{x}{x^2+y^2} \right\}, \\
B&=\left\{ (x,y):2xy+\frac{y}{x^2+y^2}=3 \right\}, \\
C&=\left\{ (x,y):x^3-3xy^2+3y=1 \right\}, \\
D&=\left\{ (x,y):3x^2y-3x-y^3=0 \right\}.
\end{align*}
Prove that $A \cap B=C \cap D$.


Lean 4 formalization:
import Mathlib

theorem putnam_1987_a1
(A B C D : Set (ℝ × ℝ))
(hA : A = {(x, y) : ℝ × ℝ | x ^ 2 + y ^ 2 ≠ 0 ∧ x ^ 2 - y ^ 2 = x / (x ^ 2 + y ^ 2)})
(hB : B = {(x, y) : ℝ × ℝ | x ^ 2 + y ^ 2 ≠ 0 ∧ 2 * x * y + y / (x ^ 2 + y ^ 2) = 3})
(hC : C = {(x, y) : ℝ × ℝ | x ^ 3 - 3 * x * y ^ 2 + 3 * y = 1})
(hD : D = {(x, y) : ℝ × ℝ | 3 * x ^ 2 * y - 3 * x - y ^ 3 = 0})
: A ∩ B = C ∩ D := by
Problem: putnam_1987_a2
Category: algebra

The sequence of digits $123456789101112131415161718192021 \dots$ is obtained by writing the positive integers in order. If the $10^n$-th digit in this sequence occurs in the part of the sequence in which the $m$-digit numbers are placed, define $f(n)$ to be $m$. For example, $f(2)=2$ because the $100$th digit enters the sequence in the placement of the two-digit integer $55$. Find, with proof, $f(1987)$.

Solution: Show that the value of $f(1987)$ is $1984$.

Lean 4 formalization:
import Mathlib

abbrev putnam_1987_a2_solution : ℕ := sorry
theorem putnam_1987_a2
    (seqind seqsize f : ℕ → ℕ)
    (hseqind : seqind 1 = 1 ∧ ∀ i ≥ 2, seqind i = seqind (i - 1) + (Nat.digits 10 (i - 1)).length)
    (hseqsize : ∀ i ≥ 1, ∀ j : Fin ((Nat.digits 10 i).length), seqsize (seqind i + j) = (Nat.digits 10 i).length)
    (hf : ∀ n : ℕ, f n = seqsize (10 ^ n)) :
    f 1987 = putnam_1987_a2_solution := by
Problem: putnam_1987_a4
Category: algebra

Let $P$ be a polynomial, with real coefficients, in three variables and $F$ be a function of two variables such that
\[
P(ux, uy, uz) = u^2 F(y-x,z-x) \quad \mbox{for all real $x,y,z,u$},
\]
and such that $P(1,0,0)=4$, $P(0,1,0)=5$, and $P(0,0,1)=6$. Also let $A,B,C$ be complex numbers with $P(A,B,C)=0$ and $|B-A|=10$. Find $|C-A|$.

Solution: Prove that $|C - A| = \frac{5}{3}\sqrt{30}$.

Lean 4 formalization:
import Mathlib

open MvPolynomial Real

noncomputable abbrev putnam_1987_a4_solution : ℂ := sorry
theorem putnam_1987_a4
(P : MvPolynomial (Fin 3) ℂ)
(hPreal : ∀ i : Fin 3 →₀ ℕ, (coeff i P).im = 0)
(F : ℝ → ℝ → ℝ)
(vars : ℂ → ℂ → ℂ → (Fin 3 → ℂ))
(hvars : vars = fun a b c ↦ fun i ↦ ite (i = 0) a (ite (i = 1) b c))
(h : ∀ x y z u : ℝ, eval (vars (u * x) (u * y) (u * z)) P = u ^ 2 * F (y - x) (z - x))
(hPval : eval (vars 1 0 0) P = 4 ∧ eval (vars 0 1 0) P = 5 ∧ eval (vars 0 0 1) P = 6)
(A B C : ℂ)
(hPABC : eval (vars A B C) P = 0)
(habs : ‖B - A‖ = 10)
: (‖C - A‖ = putnam_1987_a4_solution) := by
Problem: putnam_1987_a5
Category: analysis

Let $\vec{G}(x,y)=\left(\frac{-y}{x^2+4y^2},\frac{x}{x^2+4y^2},0\right)$. Prove or disprove that there is a vector-valued function $\vec{F}(x,y,z)=(M(x,y,z),N(x,y,z),P(x,y,z))$ with the following properties:
\begin{enumerate}
\item[(i)] $M$, $N$, $P$ have continuous partial derivatives for all $(x,y,z) \neq (0,0,0)$;
\item[(ii)] $\text{Curl}\,\vec{F}=\vec{0}$ for all $(x,y,z) \neq (0,0,0)$;
\item[(iii)] $\vec{F}(x,y,0)=\vec{G}(x,y)$.
\end{enumerate}

Solution: Show that there is no such $\vec{F}$.

Lean 4 formalization:
import Mathlib

abbrev putnam_1987_a5_solution : Prop := sorry
theorem putnam_1987_a5
    (curl : ((Fin 3 → ℝ) → (Fin 3 → ℝ)) → ((Fin 3 → ℝ) → (Fin 3 → ℝ)))
    (curl_def : ∀ f x, curl f x = ![
      fderiv ℝ f x (Pi.single 1 1) 2 - fderiv ℝ f x (Pi.single 2 1) 1,
      fderiv ℝ f x (Pi.single 2 1) 0 - fderiv ℝ f x (Pi.single 0 1) 2,
      fderiv ℝ f x (Pi.single 0 1) 1 - fderiv ℝ f x (Pi.single 1 1) 0])
    (G : (Fin 2 → ℝ) → (Fin 3 → ℝ))
    (G_def : ∀ x y, G ![x, y] = ![(-y / (x ^ 2 + 4 * y ^ 2)), (x / (x ^ 2 + 4 * y ^ 2)), 0]) :
    (∃ F : (Fin 3 → ℝ) → (Fin 3 → ℝ),
      ContDiffOn ℝ 1 F {v | v ≠ ![0,0,0]} ∧
      (∀ x, x ≠ 0 → curl F x = 0) ∧
      ∀ x y, F ![x, y, 0] = G ![x, y]) ↔ putnam_1987_a5_solution := by
Problem: putnam_1987_a6
Category: algebra, analysis

For each positive integer $n$, let $a(n)$ be the number of zeroes in the base $3$ representation of $n$. For which positive real numbers $x$ does the series
\[
\sum_{n=1}^\infty \frac{x^{a(n)}}{n^3}
\]
converge?

Solution: Show that for positive $x$, the series converges if and only if $x < 25$.

Lean 4 formalization:
import Mathlib

open MvPolynomial Real Nat

abbrev putnam_1987_a6_solution : Set ℝ := sorry
theorem putnam_1987_a6
(a : ℕ → ℕ)
(ha : a = fun n ↦ {i | (digits 3 n).get i = 0}.ncard)
: ({x : ℝ | x > 0 ∧ Summable (fun n ↦ x ^ (a n) / (n ^ 3))} = putnam_1987_a6_solution) := by
Problem: putnam_1987_b1
Category: analysis

Evaluate
\[
\int_2^4 \frac{\sqrt{\ln(9-x)}\,dx}{\sqrt{\ln(9-x)}+\sqrt{\ln(x+3)}}.
\]

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

Lean 4 formalization:
import Mathlib

open MvPolynomial Real Nat

abbrev putnam_1987_b1_solution : ℝ := sorry
theorem putnam_1987_b1
: (∫ x in (2)..4, sqrt (log (9 - x)) / (sqrt (log (9 - x)) + sqrt (log (x + 3))) = putnam_1987_b1_solution) := by
Problem: putnam_1987_b2
Category: algebra

Let $r, s$ and $t$ be integers with $0 \leq r$, $0 \leq s$ and $r+s \leq t$. Prove that
\[
\frac{\binom s0}{\binom tr}
+ \frac{\binom s1}{\binom{t}{r+1}} + \cdots
+ \frac{\binom ss}{\binom{t}{r+s}}
= \frac{t+1}{(t+1-s)\binom{t-s}{r}}.
\]


Lean 4 formalization:
import Mathlib

open MvPolynomial Real Nat

theorem putnam_1987_b2
(r s t : ℕ)
(hsum : r + s ≤ t)
: (∑ i : Finset.range (s + 1), (choose s i : ℚ) / (choose t (r + i)) = ((t + 1) : ℚ) / ((t + 1 - s) * choose (t - s) r)) := by
Problem: putnam_1987_b3
Category: abstract_algebra

Let $F$ be a field in which $1+1 \neq 0$. Show that the set of solutions to the equation $x^2+y^2=1$ with $x$ and $y$ in $F$ is given by $(x,y)=(1,0)$ and $(x,y)=\left(\frac{r^2-1}{r^2+1},\frac{2r}{r^2+1}\right)$, where $r$ runs through the elements of $F$ such that $r^2 \neq -1$.


Lean 4 formalization:
import Mathlib

open MvPolynomial Real Nat

theorem putnam_1987_b3
(F : Type*) [Field F]
(hF : (1 : F) + 1 ≠ 0)
: {(x, y) : F × F | x ^ 2 + y ^ 2 = 1} = {(1, 0)} ∪ {((r ^ 2 - 1) / (r ^ 2 + 1), (2 * r) / (r ^ 2 + 1)) | r ∈ {r' : F | r' ^ 2 ≠ -1}} := by
Problem: putnam_1987_b4
Category: analysis

Let $(x_1,y_1) = (0.8, 0.6)$ and let $x_{n+1} = x_n \cos y_n - y_n \sin y_n$ and $y_{n+1}= x_n \sin y_n + y_n \cos y_n$ for $n=1,2,3,\dots$. For each of $\lim_{n\to \infty} x_n$ and $\lim_{n \to \infty} y_n$, prove that the limit exists and find it or prove that the limit does not exist.

Solution: Show that $\lim_{n \to \infty} x_n = -1$ and $\lim_{n \to \infty} y_n = 0$.

Lean 4 formalization:
import Mathlib

open MvPolynomial Real Nat Filter Topology

abbrev putnam_1987_b4_solution : Prop × ℝ × Prop × ℝ := sorry
theorem putnam_1987_b4
    (x y : ℕ → ℝ)
    (hxy1 : (x 1, y 1) = (0.8, 0.6))
    (hx : ∀ n ≥ 1, x (n + 1) = (x n) * cos (y n) - (y n) * sin (y n))
    (hy : ∀ n ≥ 1, y (n + 1) = (x n) * sin (y n) + (y n) * cos (y n)) :
    let (existsx, limx, existsy, limy) := putnam_1987_b4_solution
    ((∃ c : ℝ, Tendsto x atTop (𝓝 c)) → existsx) ∧
    (existsx → Tendsto x atTop (𝓝 limx)) ∧
    ((∃ c : ℝ, Tendsto y atTop (𝓝 c)) → existsy) ∧
    (existsy → Tendsto y atTop (𝓝 limy)) := by
Problem: putnam_1987_b5
Category: linear_algebra

Let $O_n$ be the $n$-dimensional vector $(0,0,\cdots, 0)$. Let $M$ be a $2n \times n$ matrix of complex numbers such that whenever $(z_1, z_2, \dots, z_{2n})M = O_n$, with complex $z_i$, not all zero, then at least one of the $z_i$ is not real. Prove that for arbitrary real numbers $r_1, r_2, \dots, r_{2n}$, there are complex numbers $w_1, w_2, \dots, w_n$ such that
\[
\mathrm{re}\left[ M \left( \begin{array}{c} w_1 \\ \vdots \\ w_n \end{array} \right) \right] = \left( \begin{array}{c} r_1 \\ \vdots \\ r_{2n} \end{array} \right).
\]
(Note: if $C$ is a matrix of complex numbers, $\mathrm{re}(C)$ is the matrix whose entries are the real parts of the entries of $C$.)


Lean 4 formalization:
import Mathlib

open MvPolynomial Real Nat Filter Topology

theorem putnam_1987_b5
(n : ℕ)
(npos : n > 0)
(M : Matrix (Fin (2 * n)) (Fin n) ℂ)
(hM : ∀ z : Matrix (Fin 1) (Fin (2 * n)) ℂ, z * M = 0 → (¬∀ i : Fin (2 * n), z 0 i = 0) → ∃ i : Fin (2 * n), (z 0 i).im ≠ 0)
: (∀ r : Matrix (Fin (2 * n)) (Fin 1) ℝ, ∃ w : Matrix (Fin n) (Fin 1) ℂ, ∀ i : (Fin (2 * n)), ((M * w) i 0).re = r i 0) := by
Problem: putnam_1987_b6
Category: abstract_algebra

Let $F$ be the field of $p^2$ elements, where $p$ is an odd prime. Suppose $S$ is a set of $(p^2-1)/2$ distinct nonzero elements of $F$ with the property that for each $a\neq 0$ in $F$, exactly one of $a$ and $-a$ is in $S$. Let $N$ be the number of elements in the intersection $S \cap \{2a: a \in S\}$. Prove that $N$ is even.


Lean 4 formalization:
import Mathlib

open MvPolynomial Real Nat Filter Topology

theorem putnam_1987_b6
    (p : ℕ)
    (F : Type*) [Field F] [Fintype F]
    (S : Set F)
    (hp : Odd p ∧ Nat.Prime p)
    (Fcard : Fintype.card F = p ^ 2)
    (Snz : ∀ x ∈ S, x ≠ 0)
    (Scard : S.ncard = ((p : ℤ) ^ 2 - 1) / 2)
    (hS : ∀ a : F, a ≠ 0 → Xor' (a ∈ S) (-a ∈ S)) :
    (Even ((S ∩ {x | ∃ a ∈ S, x = 2 * a}).ncard)) := by
Problem: putnam_1988_a1
Category: geometry

Let $R$ be the region consisting of the points $(x,y)$ of the cartesian plane satisfying both $|x|-|y| \leq 1$ and $|y| \leq 1$. Find the area of $R$.

Solution: Show that the area of $R$ is $6$.

Lean 4 formalization:
import Mathlib

open MeasureTheory

abbrev putnam_1988_a1_solution : ℝ := sorry
theorem putnam_1988_a1
    (R : Set (Fin 2 → ℝ))
    (hR : R = {p | |p 0| - |p 1| ≤ 1 ∧ |p 1| ≤ 1}) :
    (volume R).toReal = putnam_1988_a1_solution := by
Problem: putnam_1988_a2
Category: analysis

A not uncommon calculus mistake is to believe that the product rule for derivatives says that $(fg)' = f'g'$. If $f(x)=e^{x^2}$, determine, with proof, whether there exists an open interval $(a,b)$ and a nonzero function $g$ defined on $(a,b)$ such that this wrong product rule is true for $x$ in $(a,b)$.

Solution: Show that such $(a,b)$ and $g$ exist.

Lean 4 formalization:
import Mathlib

open Set

abbrev putnam_1988_a2_solution : Prop := sorry
theorem putnam_1988_a2
    (f : ℝ → ℝ)
    (hf : f = fun x ↦ Real.exp (x ^ 2)) :
    putnam_1988_a2_solution ↔
    (∃ a b : ℝ,
      a < b ∧
      ∃ g : ℝ → ℝ,
        (∃ x ∈ Ioo a b, g x ≠ 0) ∧
        DifferentiableOn ℝ g (Ioo a b) ∧
        ∀ x ∈ Ioo a b, deriv (fun y ↦ f y * g y) x = (deriv f x) * (deriv g x)) := by
Problem: putnam_1988_a3
Category: analysis

Determine, with proof, the set of real numbers $x$ for which
\[
\sum_{n=1}^\infty \left( \frac{1}{n} \csc \frac{1}{n} - 1 \right)^x
\]
converges.

Solution: Show that the series converges if and only if $x > \frac{1}{2}$.

Lean 4 formalization:
import Mathlib

open Set Filter Topology

abbrev putnam_1988_a3_solution : Set ℝ := sorry
theorem putnam_1988_a3
: {x : ℝ | ∃ L : ℝ, Tendsto (fun t ↦ ∑ n ∈ Finset.Icc (1 : ℕ) t, (((1 / n) / Real.sin (1 / n) - 1) ^ x)) atTop (𝓝 L)} = putnam_1988_a3_solution := by
Problem: putnam_1988_a4
Category: geometry, combinatorics

\begin{enumerate}
\item[(a)] If every point of the plane is painted one of three colors, do there necessarily exist two points of the same color exactly one inch apart?
\item[(b)] What if ``three'' is replaced by ``nine''?
\end{enumerate}

Solution: Prove that the points must exist with three colors, but not necessarily with nine.

Lean 4 formalization:
import Mathlib

open Set Filter Topology

abbrev putnam_1988_a4_solution : Prop × Prop := sorry
theorem putnam_1988_a4
    (p : ℕ → Prop)
    (hp : ∀ n, p n ↔
      ∀ color : (EuclideanSpace ℝ (Fin 2)) → Fin n,
        ∃ p q : EuclideanSpace ℝ (Fin 2),
          color p = color q ∧ dist p q = 1) :
    (let (a, b) := putnam_1988_a4_solution; (p 3 ↔ a) ∧ (p 9 ↔ b)) := by
Problem: putnam_1988_a5
Category: analysis

Prove that there exists a \emph{unique} function $f$ from the set $\mathrm{R}^+$ of positive real numbers to $\mathrm{R}^+$ such that
\[
f(f(x)) = 6x-f(x)
\]
and
\[
f(x)>0
\]
for all $x>0$.


Lean 4 formalization:
import Mathlib

open Set Filter Topology

theorem putnam_1988_a5
: (∃ f : ℝ → ℝ, (∀ x > 0, f (f x) = 6 * x - f x ∧ f x > 0) ∧ (∀ g : ℝ → ℝ, (∀ x > 0, g (g x) = 6 * x - g x ∧ g x > 0) → (∀ x > 0, f x = g x))) := by
Problem: putnam_1988_a6
Category: linear_algebra

If a linear transformation $A$ on an $n$-dimensional vector space has $n+1$ eigenvectors such that any $n$ of them are linearly independent, does it follow that $A$ is a scalar multiple of the identity? Prove your answer.

Solution: Show that the answer is yes, $A$ must be a scalar multiple of the identity.

Lean 4 formalization:
import Mathlib

open Set Filter Topology

abbrev putnam_1988_a6_solution : Prop := sorry
theorem putnam_1988_a6
: (∀ (F V : Type*) (_ : Field F) (_ : AddCommGroup V) (_ : Module F V) (_ : FiniteDimensional F V) (n : ℕ) (A : Module.End F V) (evecs : Set V), (n = Module.finrank F V ∧ evecs ⊆ {v : V | ∃ f : F, A.HasEigenvector f v} ∧ evecs.encard = n + 1 ∧ (∀ sevecs : Fin n → V, (Set.range sevecs ⊆ evecs ∧ (Set.range sevecs).encard = n) → LinearIndependent F sevecs)) → (∃ c : F, A = c • LinearMap.id)) ↔ putnam_1988_a6_solution := by
Problem: putnam_1988_b1
Category: number_theory, algebra

A \emph{composite} (positive integer) is a product $ab$ with $a$ and $b$ not necessarily distinct integers in $\{2,3,4,\dots\}$. Show that every composite is expressible as $xy+xz+yz+1$, with $x,y,z$ positive integers.


Lean 4 formalization:
import Mathlib

open Set Filter Topology

theorem putnam_1988_b1
: ∀ a ≥ 2, ∀ b ≥ 2, ∃ x y z : ℤ, x > 0 ∧ y > 0 ∧ z > 0 ∧ a * b = x * y + x * z + y * z + 1 := by
Problem: putnam_1988_b2
Category: algebra

Prove or disprove: If $x$ and $y$ are real numbers with $y \geq 0$ and $y(y+1) \leq (x+1)^2$, then $y(y-1) \leq x^2$.

Solution: Show that this is true.

Lean 4 formalization:
import Mathlib

open Set Filter Topology

abbrev putnam_1988_b2_solution : Prop := sorry
theorem putnam_1988_b2
: (∀ x y : ℝ, (y ≥ 0 ∧ y * (y + 1) ≤ (x + 1) ^ 2) → (y * (y - 1) ≤ x ^ 2)) ↔ putnam_1988_b2_solution := by
Problem: putnam_1988_b3
Category: algebra

For every $n$ in the set $N=\{1,2,\dots\}$ of positive integers, let $r_n$ be the minimum value of $|c-d \sqrt{3}|$ for all nonnegative integers $c$ and $d$ with $c+d=n$. Find, with proof, the smallest positive real number $g$ with $r_n \leq g$ for all $n \in N$.

Solution: Show that the smallest such $g$ is $(1+\sqrt{3})/2$.

Lean 4 formalization:
import Mathlib

open Set Filter Topology

noncomputable abbrev putnam_1988_b3_solution : ℝ := sorry
theorem putnam_1988_b3
    (r : ℤ → ℝ)
    (hr : ∀ n ≥ 1,
      (∃ c d : ℤ,
        (c ≥ 0 ∧ d ≥ 0) ∧
        c + d = n ∧ r n = |c - d * Real.sqrt 3|) ∧
        (∀ c d : ℤ, (c ≥ 0 ∧ d ≥ 0 ∧ c + d = n) → |c - d * Real.sqrt 3| ≥ r n))
    : IsLeast {g : ℝ | g > 0 ∧ (∀ n : ℤ, n ≥ 1 → r n ≤ g)} putnam_1988_b3_solution := by
Problem: putnam_1988_b4
Category: analysis

Prove that if $\sum_{n=1}^\infty a_n$ is a convergent series of positive real numbers, then so is $\sum_{n=1}^\infty (a_n)^{n/(n+1)}$.


Lean 4 formalization:
import Mathlib

open Set Filter Topology

theorem putnam_1988_b4
    (a : ℕ → ℝ)
    (IsPosConv : (ℕ → ℝ) → Prop)
    (IsPosConv_def : ∀ a' : ℕ → ℝ, IsPosConv a' ↔
      (∀ n ≥ 1, a' n > 0) ∧
      (∃ s : ℝ, Tendsto (fun N : ℕ => ∑ n : Set.Icc 1 N, a' n) atTop (𝓝 s))) :
    (IsPosConv a) → IsPosConv (fun n : ℕ => (a n) ^ ((n : ℝ) / (n + 1))) := by
Problem: putnam_1988_b5
Category: linear_algebra

For positive integers $n$, let $M_n$ be the $2n+1$ by $2n+1$ skew-symmetric matrix for which each entry in the first $n$ subdiagonals below the main diagonal is $1$ and each of the remaining entries below the main diagonal is $-1$. Find, with proof, the rank of $M_n$. (According to one definition, the rank of a matrix is the largest $k$ such that there is a $k \times k$ submatrix with nonzero determinant.) One may note that
\begin{align*}
M_1&=\begin{pmatrix} 0 & -1 & 1 \\ 1 & 0 & -1 \\ -1 & 1 & 0 \end{pmatrix} \\
M_2&=\begin{pmatrix} 0 & -1 & -1 & 1 & 1 \\ 1 & 0 & -1 & -1 & 1 \\ 1 & 1 & 0 & -1 & -1 \\ -1 & 1 & 1 & 0 & -1 \\ -1 & -1 & 1 & 1 & 0 \end{pmatrix}.
\end{align*}

Solution: Show that the rank of $M_n$ equals $2n$.

Lean 4 formalization:
import Mathlib

open Set Filter Topology

abbrev putnam_1988_b5_solution : ℕ → ℕ := sorry
theorem putnam_1988_b5
    (n : ℕ) (hn : n > 0)
    (Mn : Matrix (Fin (2 * n + 1)) (Fin (2 * n + 1)) ℝ)
    (Mnskewsymm : ∀ i j, Mn i j = -(Mn j i))
    (hMn1 : ∀ i j, (1 ≤ (i.1 : ℤ) - j.1 ∧ (i.1 : ℤ) - j.1 ≤ n) → Mn i j = 1)
    (hMnn1 : ∀ i j, (i.1 : ℤ) - j.1 > n → Mn i j = -1) :
    Mn.rank = putnam_1988_b5_solution n := by
Problem: putnam_1988_b6
Category: number_theory, algebra

Prove that there exist an infinite number of ordered pairs $(a,b)$ of integers such that for every positive integer $t$, the number $at+b$ is a triangular number if and only if $t$ is a triangular number. (The triangular numbers are the $t_n=n(n+1)/2$ with $n$ in $\{0,1,2,\dots\}$.)


Lean 4 formalization:
import Mathlib

open Set Filter Topology

theorem putnam_1988_b6
(trinums : Set ℤ)
(htrinums : trinums = {t : ℤ | ∃ n : ℤ, t ≥ 0 ∧ t = (n * (n + 1)) / 2})
: {(a, b) : ℤ × ℤ | ∀ t > 0, (a * t + b) ∈ trinums ↔ t ∈ trinums}.encard = ⊤ := by
Problem: putnam_1989_a1
Category: algebra, number_theory

How many primes among the positive integers, written as usual in base $10$, are alternating $1$'s and $0$'s, beginning and ending with $1$?

Solution: Show that there is only one such prime.

Lean 4 formalization:
import Mathlib

abbrev putnam_1989_a1_solution : ℕ∞ := sorry
theorem putnam_1989_a1
    (pdigalt : List ℕ → Prop)
    (hpdigalt : ∀ l, pdigalt l ↔ Odd l.length ∧ (∀ i, l.get i = if Even (i : ℕ) then 1 else 0)) :
    {p : ℕ | p.Prime ∧ pdigalt (Nat.digits 10 p)}.encard = putnam_1989_a1_solution := by
Problem: putnam_1989_a2
Category: analysis

Evaluate $\int_0^a \int_0^b e^{\max\{b^2x^2,a^2y^2\}}\,dy\,dx$ where $a$ and $b$ are positive.

Solution: Show that the value of the integral is $(e^{a^2b^2}-1)/(ab)$.

Lean 4 formalization:
import Mathlib

noncomputable abbrev putnam_1989_a2_solution : ℝ → ℝ → ℝ := sorry
theorem putnam_1989_a2
(a b : ℝ)
(abpos : a > 0 ∧ b > 0)
: ∫ x in Set.Ioo 0 a, ∫ y in Set.Ioo 0 b, Real.exp (max (b ^ 2 * x ^ 2) (a ^ 2 * y ^ 2)) = putnam_1989_a2_solution a b := by