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

Suppose that each of $n$ people writes down the numbers $1,2,3$ in random order in one column of a $3 \times n$ matrix, with all orders equally likely and with the orders for different columns independent of each other. Let the row sums $a,b,c$ of the resulting matrix be rearranged (if necessary) so that $a \leq b \leq c$. Show that for some $n \geq 1995$, it is at least four times as likely that both $b=a+1$ and $c=a+2$ as that $a=b=c$.


Lean 4 formalization:
import Mathlib

open Filter Topology Real

theorem putnam_1995_a6
(SM : (n : ℕ) → Set (Matrix (Fin 3) (Fin n) ℤ))
(Srowsums : (n : ℕ) → Matrix (Fin 3) (Fin n) ℤ → Set ℤ)
(sumsprog : (Set ℤ) → Prop)
(hSM : ∀ n, SM n = {M : Matrix (Fin 3) (Fin n) ℤ | ∀ j : Fin n, {M i j | i : Fin 3} = {1, 2, 3}})
(hSrowsums : ∀ n M, Srowsums n M = {∑ j : Fin n, M i j | i : Fin 3})
(hsumsprog : ∀ sums, sumsprog sums ↔ sums.encard = 3 ∧ (∃ a b c : ℤ, {a, b, c} = sums ∧ b = a + 1 ∧ c = a + 2))
: ∃ n ≥ 1995, {M : (SM n) | sumsprog (Srowsums n M)}.encard ≥ 4 * {M : (SM n) | (Srowsums n M).encard = 1}.encard := by
Problem: putnam_1995_b1
Category: combinatorics

For a partition $\pi$ of $\{1, 2, 3, 4, 5, 6, 7, 8, 9\}$, let $\pi(x)$ be the number of elements in the part containing $x$. Prove that for any two partitions $\pi$ and $\pi'$, there are two distinct numbers $x$ and $y$ in $\{1, 2, 3, 4, 5, 6, 7, 8, 9\}$ such that $\pi(x) = \pi(y)$ and $\pi'(x) = \pi'(y)$. [A {\em partition} of a set $S$ is a collection of disjoint subsets (parts) whose union is $S$.]


Lean 4 formalization:
import Mathlib

open Filter Topology Real Nat

theorem putnam_1995_b1
  (Pi : Finpartition (Finset.range 9) → (Finset.range 9) → ℕ)
  (Pi_def : ∀ partition k, Pi partition k = (Exists.choose (Finpartition.exists_mem partition k.2)).card) :
  ∀ Pt1 Pt2,
    ∃ x y : Finset.range 9,
      x ≠ y ∧
      Pi Pt1 x = Pi Pt1 y ∧
      Pi Pt2 x = Pi Pt2 y := by
Problem: putnam_1995_b3
Category: linear_algebra

To each positive integer with $n^{2}$ decimal digits, we associate the determinant of the matrix obtained by writing the digits in order across the rows. For example, for $n=2$, to the integer 8617 we associate $\det \left( \begin{array}{cc} 8 & 6 \ 1 & 7 \end{array} \right) = 50$. Find, as a function of $n$, the sum of all the determinants associated with $n^{2}$-digit integers. (Leading digits are assumed to be nonzero; for example, for $n=2$, there are 9000 determinants.)

Solution: Show that the solution is $45$ if $n = 1$, $45^2*10$ if $n = 2$, and $0$ if $n$ is greater than 2.

Lean 4 formalization:
import Mathlib

open Filter Topology Real Nat

abbrev putnam_1995_b3_solution : ℕ → ℤ := sorry
theorem putnam_1995_b3
(n : ℕ)
(hn : n > 0)
(digits_set : Set (ℕ → ℕ))
(hdigits_set : digits_set = {f | f 0 ≠ 0 ∧ (∀ i : Fin (n ^ 2), f i ≤ 9) ∧ (∀ i ≥ n ^ 2, f i = 0)})
(digits_to_matrix : (ℕ → ℕ) → Matrix (Fin n) (Fin n) ℤ)
(hdigits_to_matrix : digits_to_matrix = fun f => (fun i j => f (i.1 * n + j.1)))
: ∑' f : digits_set, (digits_to_matrix f).det = putnam_1995_b3_solution n := by
Problem: putnam_1995_b4
Category: algebra

Evaluate \[ \sqrt[8]{2207 - \frac{1}{2207-\frac{1}{2207-\dots}}}. \] Express your answer in the form $\frac{a+b\sqrt{c}}{d}$, where $a,b,c,d$ are integers.

Solution: Show that the solution is $(3 + 1*\sqrt{5})/2.

Lean 4 formalization:
import Mathlib

open Filter Topology Real Nat

abbrev putnam_1995_b4_solution : ℤ × ℤ × ℤ × ℤ := sorry
theorem putnam_1995_b4
    (contfrac : ℝ)
    (hcontfrac : contfrac = 2207 - 1 / contfrac)
    (hcontfrac' : 1 < contfrac) :
    let ⟨a, b, c, d⟩ := putnam_1995_b4_solution
    contfrac ^ ((1 : ℝ) / 8) = (a + b * sqrt c) / d := by
Problem: putnam_1995_b6
Category: algebra, number_theory

For a positive real number $\alpha$, define \[ S(\alpha) = \{ \lfloor n\alpha \rfloor : n = 1,2,3,\dots \}. \] Prove that $\{1,2,3,\dots\}$ cannot be expressed as the disjoint union of three sets $S(\alpha), S(\beta)$ and $S(\gamma)$. [As usual, $\lfloor x \rfloor$ is the greatest integer $\leq x$.]


Lean 4 formalization:
import Mathlib

open Filter Topology Real Nat

theorem putnam_1995_b6
  (S : ℝ → Set ℕ)
  (hS : S = fun (α : ℝ) => {x : ℕ | ∃ n : ℕ, n ≥ 1 ∧ x = floor (n * α)}) :
  ¬ ∃ α β γ,
    α > 0 ∧ β > 0 ∧ γ > 0 ∧
    (S α) ∩ (S β) = ∅ ∧ (S β) ∩ (S γ) = ∅ ∧ (S α) ∩ (S γ) = ∅ ∧
    Set.Ici 1 = (S α) ∪ (S β) ∪ (S γ) := by
Problem: putnam_1996_a2
Category: geometry

Let $C_1$ and $C_2$ be circles whose centers are $10$ units apart, and whose radii are $1$ and $3$. Find, with proof, the locus of all points $M$ for which there exist points $X$ on $C_1$ and $Y$ on $C_2$ such that $M$ is the midpoint of the line segment $XY$.

Solution: Let $O_1$ and $O_2$ be the centers of $C_1$ and $C_2$, respectively. Then show that the desired locus is an annulus centered at the midpoint $O$ of $O_1O_2$, with inner radius $1$ and outer radius $2$.

Lean 4 formalization:
import Mathlib

open Metric

abbrev putnam_1996_a2_solution : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → Set (EuclideanSpace ℝ (Fin 2)) := sorry
theorem putnam_1996_a2
(O1 O2 : EuclideanSpace ℝ (Fin 2))
(C1 C2 : Set (EuclideanSpace ℝ (Fin 2)))
(hC1 : C1 = sphere O1 1)
(hC2 : C2 = sphere O2 3)
(hO1O2 : dist O1 O2 = 10)
: {M : EuclideanSpace ℝ (Fin 2) | ∃ X Y, X ∈ C1 ∧ Y ∈ C2 ∧ M = midpoint ℝ X Y} = putnam_1996_a2_solution O1 O2 := by
Problem: putnam_1996_a3
Category: combinatorics

Suppose that each of 20 students has made a choice of anywhere from 0 to 6 courses from a total of 6 courses offered. Prove or disprove: there are 5 students and 2 courses such that all 5 have chosen both courses or all 5 have chosen neither course.

Solution: Show that the solution is that the statement is false.

Lean 4 formalization:
import Mathlib

abbrev putnam_1996_a3_solution : Prop := sorry
theorem putnam_1996_a3 :
    (∀ choices : Fin 20 → Set (Fin 6),
      ∃ (students : Finset (Fin 20)) (courses : Finset (Fin 6)),
        students.card = 5 ∧
        courses.card = 2 ∧
        (↑courses ⊆ ⋂ s ∈ students, choices s ∨ ↑courses ⊆ ⋂ s ∈ students, (choices s)ᶜ))
    ↔ putnam_1996_a3_solution := by
Problem: putnam_1996_a4
Category: algebra

Let $S$ be a set of ordered triples $(a, b, c)$ of distinct elements of a finite set $A$. Suppose that \begin{enumerate} \item $(a,b,c) \in S$ if and only if $(b,c,a) \in S$; \item $(a,b,c) \in S$ if and only if $(c,b,a) \notin S$; \item $(a,b,c)$ and $(c,d,a)$ are both in $S$ if and only if $(b,c,d)$ and $(d,a,b)$ are both in $S$. \end{enumerate} Prove that there exists a one-to-one function $g$ from $A$ to $\R$ such that $g(a) < g(b) < g(c)$ implies $(a,b,c) \in S$.


Lean 4 formalization:
import Mathlib

open Function

theorem putnam_1996_a4
(A : Type*)
[Finite A]
(S : Set (A × A × A))
(hSdistinct : ∀ a b c : A, ⟨a, b, c⟩ ∈ S → a ≠ b ∧ b ≠ c ∧ a ≠ c)
(hS1 : ∀ a b c : A, [a,b,c].Pairwise (· ≠ ·) → (⟨a, b, c⟩ ∈ S ↔ ⟨b, c, a⟩ ∈ S))
(hS2 : ∀ a b c : A, [a,b,c].Pairwise (· ≠ ·) → (⟨a, b, c⟩ ∈ S ↔ ⟨c, b, a⟩ ∉ S))
(hS3 : ∀ a b c d : A, [a,b,c,d].Pairwise (· ≠ ·) → ((⟨a, b, c⟩ ∈ S ∧ ⟨c, d, a⟩ ∈ S) ↔ (⟨b,c,d⟩ ∈ S ∧ ⟨d,a,b⟩ ∈ S)))
: ∃ g : A → ℝ, Injective g ∧ (∀ a b c : A, g a < g b ∧ g b < g c → ⟨a,b,c⟩ ∈ S) := by
Problem: putnam_1996_a5
Category: number_theory

If $p$ is a prime number greater than 3 and $k = \lfloor 2p/3 \rfloor$, prove that the sum \[\binom p1 + \binom p2 + \cdots + \binom pk \] of binomial coefficients is divisible by $p^2$.


Lean 4 formalization:
import Mathlib

open Function

theorem putnam_1996_a5
(p : ℕ)
(hpprime : Prime p)
(hpge3 : p > 3)
(k : ℕ)
(hk : k = Nat.floor (2*p/(3 : ℚ)))
: p^2 ∣ ∑ i ∈ Finset.Icc 1 k, Nat.choose p i := by
Problem: putnam_1996_a6
Category: analysis, algebra

Let $c>0$ be a constant. Give a complete description, with proof, of the set of all continuous functions $f:\mathbb{R} \to \mathbb{R}$ such that $f(x)=f(x^2+c)$ for all $x \in \mathbb{R}$.

Solution: Show that if $c \leq 1/4$ then $f$ must be constant, and if $c>1/4$ then $f$ can be defined on $[0,c]$ as any continuous function with equal values on the endpoints, then extended to $x>c$ by the relation $f(x)=f(x^2+c)$, then extended further to $x<0$ by the relation $f(x)=f(-x)$.

Lean 4 formalization:
import Mathlib

open Function

abbrev putnam_1996_a6_solution : ℝ → Set (ℝ → ℝ) := sorry
theorem putnam_1996_a6
(c : ℝ)
(f : ℝ → ℝ)
(cgt0 : c > 0)
: (Continuous f ∧ ∀ x : ℝ, f x = f (x ^ 2 + c)) ↔ f ∈ putnam_1996_a6_solution c := by
Problem: putnam_1996_b1
Category: algebra

Define a \emph{selfish} set to be a set which has its own cardinality (number of elements) as an element. Find, with proof, the number of subsets of $\{1,2,\ldots,n\}$ which are \emph{minimal} selfish sets, that is, selfish sets none of whose proper subsets is selfish.

Solution: Show that the number of subsets is $F_n$, the $n$th Fibonacci number.

Lean 4 formalization:
import Mathlib

open Function

abbrev putnam_1996_b1_solution : ℕ → ℕ := sorry
theorem putnam_1996_b1
(selfish : Finset ℕ → Prop)
(n : ℕ)
(hselfish : ∀ s : Finset ℕ, selfish s = (s.card ∈ s))
(npos : n ≥ 1)
: {s : Finset ℕ | (s : Set ℕ) ⊆ Set.Icc 1 n ∧ selfish s ∧ (∀ ss : Finset ℕ, ss ⊂ s → ¬selfish ss)}.encard = putnam_1996_b1_solution n := by
Problem: putnam_1996_b2
Category: analysis

Show that for every positive integer $n$, $(\frac{2n-1}{e})^{\frac{2n-1}{2}}<1 \cdot 3 \cdot 5 \cdots (2n-1)<(\frac{2n+1}{e})^{\frac{2n+1}{2}}$.


Lean 4 formalization:
import Mathlib

open Function

theorem putnam_1996_b2
(n : ℕ)
(prododd : ℝ)
(npos : n > 0)
(hprododd : prododd = ∏ i ∈ Finset.range (2 * n), if Odd i then i else 1)
: ((2 * n - 1 : ℝ) / Real.exp 1) ^ ((2 * n - 1 : ℝ) / 2) < prododd ∧ prododd < ((2 * n + 1 : ℝ) / Real.exp 1) ^ ((2 * n + 1 : ℝ) / 2) := by
Problem: putnam_1996_b3
Category: algebra

Given that $\{x_1,x_2,\ldots,x_n\}=\{1,2,\ldots,n\}$, find, with proof, the largest possible value, as a function of $n$ (with $n \geq 2$), of $x_1x_2+x_2x_3+\cdots+x_{n-1}x_n+x_nx_1$.

Solution: Show that the maximum is $(2n^3+3n^2-11n+18)/6$.

Lean 4 formalization:
import Mathlib

open Function

abbrev putnam_1996_b3_solution : ℕ → ℕ := sorry
theorem putnam_1996_b3
  (n : ℕ) (hn : n ≥ 2) :
  IsGreatest
  {k | ∃ x : ℕ → ℤ,
    (x '' (Finset.range n) = Set.Icc (1 : ℤ) n) ∧
    ∑ i : Fin n, x i * x ((i + 1) % n) = k}
  (putnam_1996_b3_solution n) := by
Problem: putnam_1996_b4
Category: linear_algebra

For any square matrix $A$, we can define $\sin A$ by the usual power series: $\sin A=\sum_{n=0}^\infty \frac{(-1)^n}{(2n+1)!}A^{2n+1}$. Prove or disprove: there exists a $2 \times 2$ matrix $A$ with real entries such that $\sin A=\begin{pmatrix} 1 & 1996 \\ 0 & 1 \end{pmatrix}$.

Solution: Show that there does not exist such a matrix $A$.

Lean 4 formalization:
import Mathlib

open Function Nat

abbrev putnam_1996_b4_solution : Prop := sorry
theorem putnam_1996_b4
(matsin : Matrix (Fin 2) (Fin 2) ℝ → Matrix (Fin 2) (Fin 2) ℝ)
(mat1996 : Matrix (Fin 2) (Fin 2) ℝ)
(hmatsin : ∀ A, matsin A = ∑' n : ℕ, ((-(1 : ℝ)) ^ n / (2 * n + 1)!) • A ^ (2 * n + 1))
(hmat1996 : mat1996 0 0 = 1 ∧ mat1996 0 1 = 1996 ∧ mat1996 1 0 = 0 ∧ mat1996 1 1 = 1)
: (∃ A, matsin A = mat1996) ↔ putnam_1996_b4_solution := by
Problem: putnam_1996_b5
Category: algebra

Given a finite string $S$ of symbols $X$ and $O$, we write $\Delta(S)$ for the number of $X$'s in $S$ minus the number of $O$'s. For example, $\Delta(XOOXOOX)=-1$. We call a string $S$ \emph{balanced} if every substring $T$ of (consecutive symbols of) $S$ has $-2 \leq \Delta(T) \leq 2$. Thus, $XOOXOOX$ is not balanced, since it contains the substring $OOXOO$. Find, with proof, the number of balanced strings of length $n$.

Solution: Show that the number of balanced strings of length $n$ is $3 \cdot 2^{n/2}-2$ if $n$ is even, and $2^{(n+1)/2}-2$ if $n$ is odd.

Lean 4 formalization:
import Mathlib

open Function Nat

abbrev putnam_1996_b5_solution : ℕ → ℕ := sorry

theorem putnam_1996_b5
    (n : ℕ)
    (Δ : (Fin n → ℤˣ) → Fin n → Fin n → ℤ)
    (balanced : (Fin n → ℤˣ) → Prop)
    (hΔ : ∀ S, ∀ a b, a ≤ b → Δ S a b = ∑ i ∈ Finset.Icc a b, (S i : ℤ))
    (hbalanced : ∀ S, balanced S ↔ ∀ a b, a ≤ b → |Δ S a b| ≤ 2) :
    {S : Fin n → ℤˣ | balanced S}.ncard = putnam_1996_b5_solution n := by
Problem: putnam_1997_a3
Category: analysis

Evaluate \begin{gather*} \int_0^\infty \left(x-\frac{x^3}{2}+\frac{x^5}{2\cdot 4}-\frac{x^7}{2\cdot 4\cdot 6}+\cdots\right) \\ \left(1+\frac{x^2}{2^2}+\frac{x^4}{2^2\cdot 4^2}+\frac{x^6}{2^2\cdot 4^2 \cdot 6^2}+\cdots\right)\,dx. \end{gather*}

Solution: Show that the solution is $\sqrt{e}$.

Lean 4 formalization:
import Mathlib

open Filter Topology

noncomputable abbrev putnam_1997_a3_solution : ℝ := sorry
theorem putnam_1997_a3
(series1 series2 : ℝ → ℝ)
(hseries1 : series1 = fun x => ∑' n : ℕ, (-1)^n * x^(2*n + 1)/(∏ i : Finset.range n, 2 * ((i : ℝ) + 1)))
(hseries2 : series2 = fun x => ∑' n : ℕ, x^(2*n)/(∏ i : Finset.range n, (2 * ((i : ℝ) + 1))^2))
: Tendsto (fun t => ∫ x in Set.Icc 0 t, series1 x * series2 x) atTop (𝓝 (putnam_1997_a3_solution)) := by
Problem: putnam_1997_a4
Category: abstract_algebra

Let $G$ be a group with identity $e$ and $\phi:G\rightarrow G$ a function such that \[\phi(g_1)\phi(g_2)\phi(g_3)=\phi(h_1)\phi(h_2)\phi(h_3)\] whenever $g_1g_2g_3=e=h_1h_2h_3$. Prove that there exists an element $a\in G$ such that $\psi(x)=a\phi(x)$ is a homomorphism (i.e. $\psi(xy)=\psi(x)\psi(y)$ for all $x,y\in G$).


Lean 4 formalization:
import Mathlib

open Filter Topology

theorem putnam_1997_a4
(G : Type*)
[Group G]
(φ : G → G)
(hφ : ∀ g1 g2 g3 h1 h2 h3 : G, (g1 * g2 * g3 = 1 ∧ h1 * h2 * h3 = 1) → φ g1 * φ g2 * φ g3 = φ h1 * φ h2 * φ h3)
: ∃ a : G, let ψ := fun g => a * φ g; ∀ x y : G, ψ (x * y) = ψ x * ψ y := by
Problem: putnam_1997_a5
Category: number_theory

Let $N_n$ denote the number of ordered $n$-tuples of positive integers $(a_1,a_2,\ldots,a_n)$ such that $1/a_1 + 1/a_2 +\ldots + 1/a_n=1$.  Determine whether $N_{10}$ is even or odd.

Solution: Show that $N_{10}$ is odd.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_1997_a5_solution : Prop := sorry
theorem putnam_1997_a5
(N : (n : ℕ+) → Set (Fin n → ℕ+))
(hN : N = fun (n : ℕ+) => {t : Fin n → ℕ+ | (∑ i : Fin n, (1 : ℝ)/(t i) = 1) })
: Odd (N 10).ncard ↔ putnam_1997_a5_solution := by
Problem: putnam_1997_a6
Category: algebra

For a positive integer $n$ and any real number $c$, define $x_k$ recursively by $x_0=0$, $x_1=1$, and for $k\geq 0$, \[x_{k+2}=\frac{cx_{k+1}-(n-k)x_k}{k+1}.\] Fix $n$ and then take $c$ to be the largest value for which $x_{n+1}=0$. Find $x_k$ in terms of $n$ and $k$, $1\leq k\leq n$.

Solution: Show that the solution is that $x_k = {n - 1 \choose k - 1}$.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_1997_a6_solution : ℤ → ℤ → ℝ := sorry
theorem putnam_1997_a6
  (n : ℤ)
  (hn : n > 0)
  (x : ℝ → (ℤ → ℝ))
  (hx0 : ∀ c, x c 0 = 0)
  (hx1 : ∀ c, x c 1 = 1)
  (hxk : ∀ c, ∀ k ≥ 0, x c (k + 2) = (c*(x c (k + 1)) - (n - k)*(x c k))/(k + 1))
  (S : Set ℝ)
  (hS : S = {c : ℝ | x c (n + 1) = 0}) :
  ∀ k : Set.Icc 1 n, x (sSup S) k = putnam_1997_a6_solution n k := by
Problem: putnam_1997_b1
Category: algebra

Let $\{x\}$ denote the distance between the real number $x$ and the nearest integer.  For each positive integer $n$, evaluate \[F_n=\sum_{m=1}^{6n-1} \min(\{\frac{m}{6n}\},\{\frac{m}{3n}\}).\] (Here $\min(a,b)$ denotes the minimum of $a$ and $b$.)

Solution: Show that the solution is $n$.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_1997_b1_solution : ℕ → ℝ := sorry
noncomputable def dist_to_int : ℝ → ℝ := fun r => |r - round r|
theorem putnam_1997_b1
(F : ℕ → ℝ)
(hF : F = fun (n : ℕ) => ∑ m ∈ Finset.Icc 1 (6 * n - 1), min (dist_to_int (m/(6*n)) ) (dist_to_int (m/(3*n))))
: ∀ n, n > 0 → F n = putnam_1997_b1_solution n := by
Problem: putnam_1997_b2
Category: analysis

Let $f$ be a twice-differentiable real-valued function satisfying \[f(x)+f''(x)=-xg(x)f'(x),\] where $g(x)\geq 0$ for all real $x$.  Prove that $|f(x)|$ is bounded.


Lean 4 formalization:
import Mathlib

open Filter Topology Bornology Set

theorem putnam_1997_b2
(f g : ℝ → ℝ)
(hg : ∀ x : ℝ, g x ≥ 0)
(hfderiv1 : ContDiff ℝ 1 f)
(hfderiv2 : Differentiable ℝ (deriv f))
(hfg : ∀ x : ℝ, f x + iteratedDeriv 2 f x = -x * g x * deriv f x)
: IsBounded (range (fun x => |f x|)) := by
Problem: putnam_1997_b3
Category: number_theory

For each positive integer $n$, write the sum $\sum_{m=1}^n 1/m$ in the form $p_n/q_n$, where $p_n$ and $q_n$ are relatively prime positive integers.  Determine all $n$ such that 5 does not divide $q_n$.

Solution: Show that the solution is the set of natural numbers which are between $1$ and $4$, or between $20$ and $24$, or between $100$ and $104$, or between $120$ and $124$.

Lean 4 formalization:
import Mathlib

open Filter Topology Bornology Set

abbrev putnam_1997_b3_solution : Set ℕ := sorry
theorem putnam_1997_b3
(n : ℕ)
(hn : n > 0)
: n ∈ putnam_1997_b3_solution ↔ ¬5 ∣ (∑ m ∈ Finset.Icc 1 n, 1/m : ℚ).den := by
Problem: putnam_1997_b4
Category: algebra

Let $a_{m,n}$ denote the coefficient of $x^n$ in the expansion of $(1+x+x^2)^m$.  Prove that for all [integers] $k\geq 0$, \[0\leq \sum_{i=0}^{\lfloor \frac{2k}{3}\rfloor} (-1)^i a_{k-i,i}\leq 1.\]


Lean 4 formalization:
import Mathlib

open Filter Topology Bornology Set Polynomial

theorem putnam_1997_b4
    (a : ℕ → ℕ → ℤ)
    (ha : ∀ m n, a m n = coeff ((1 + X + X ^ 2) ^ m) n)
    (k : ℕ) :
    (∑ i ∈ Finset.Iic ⌊2 * (k : ℚ) / 3⌋₊, (-1) ^ i * a (k - i) i) ∈ Icc 0 1 := by
Problem: putnam_1997_b5
Category: number_theory

Prove that for $n\geq 2$, \[\overbrace{2^{2^{\cdots^{2}}}}^{\mbox{$n$ terms}} \equiv \overbrace{2^{2^{\cdots^{2}}}}^{\mbox{$n-1$ terms}} \quad \pmod{n}.\]


Lean 4 formalization:
import Mathlib

def tetration : ℕ → ℕ → ℕ
  | _, 0 => 1
  | b, (m + 1) => b^(tetration b m)
theorem putnam_1997_b5
(n : ℕ)
(hn : n ≥ 2)
: tetration 2 n ≡ tetration 2 (n-1) [MOD n] := by
Problem: putnam_1998_a2
Category: geometry

Let $s$ be any arc of the unit circle lying entirely in the first quadrant. Let $A$ be the area of the region lying below $s$ and above the $x$-axis and let $B$ be the area of the region lying to the right of the $y$-axis and to the left of $s$. Prove that $A+B$ depends only on the arc length, and not on the position, of $s$.


Lean 4 formalization:
import Mathlib

theorem putnam_1998_a2
(quadrant : (EuclideanSpace ℝ (Fin 2)) → Prop)
(isarc : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → Prop)
(hquadrant : ∀ P, quadrant P ↔ P 0 > 0 ∧ P 1 > 0 ∧ dist 0 P = 1)
(hisarc : ∀ P Q, isarc P Q ↔ quadrant P ∧ quadrant Q ∧ P 0 > Q 0)
(arc : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → Set (EuclideanSpace ℝ (Fin 2)))
(harc : arc = fun P Q ↦ {R : EuclideanSpace ℝ (Fin 2) | quadrant R ∧ P 0 > R 0 ∧ R 0 > Q 0})
(A B : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → ℝ)
(hA : A = fun P Q ↦ (MeasureTheory.volume {S : EuclideanSpace ℝ (Fin 2) | ∃ R ∈ arc P Q, R 0 = S 0 ∧ R 1 > S 1 ∧ S 1 > 0}).toReal)
(hB : B = fun P Q ↦ (MeasureTheory.volume {S : EuclideanSpace ℝ (Fin 2) | ∃ R ∈ arc P Q, R 1 = S 1 ∧ R 0 > S 0 ∧ S 0 > 0}).toReal)
: (∃ f : ℝ → ℝ, ∀ P Q : EuclideanSpace ℝ (Fin 2), isarc P Q → A P Q + B P Q = f (InnerProductGeometry.angle P Q)) := by
Problem: putnam_1998_a3
Category: analysis

Let $f$ be a real function on the real line with continuous third derivative.  Prove that there exists a point $a$ such that \[f(a)\cdot f'(a) \cdot f''(a) \cdot f'''(a)\geq 0 .\]


Lean 4 formalization:
import Mathlib

theorem putnam_1998_a3
(f : ℝ → ℝ)
(hf : ContDiff ℝ 3 f)
: ∃ a : ℝ, (f a) * (deriv f a) * (iteratedDeriv 2 f a) * (iteratedDeriv 3 f a) ≥ 0 := by
Problem: putnam_1998_a4
Category: algebra

Let $A_1=0$ and $A_2=1$. For $n>2$, the number $A_n$ is defined by concatenating the decimal expansions of $A_{n-1}$ and $A_{n-2}$ from left to right.  For example $A_3=A_2 A_1=10$, $A_4=A_3 A_2 = 101$, $A_5=A_4 A_3 = 10110$, and so forth.  Determine all $n$ such that $11$ divides $A_n$.

Solution: Show that the solution is those n for which n can be written as 6k+1 for some integer k.

Lean 4 formalization:
import Mathlib

abbrev putnam_1998_a4_solution : Set ℕ := sorry
theorem putnam_1998_a4
    (A : ℕ → List ℕ)
    (hA1 : A 1 = [0])
    (hA2 : A 2 = [1])
    (hA : ∀ n > 0, A (n + 2) = A (n + 1) ++ A n) :
    {n | 1 ≤ n ∧ 11 ∣ Nat.ofDigits 10 (A n).reverse} = putnam_1998_a4_solution := by
Problem: putnam_1998_a5
Category: analysis

Let $\mathcal F$ be a finite collection of open discs in $\mathbb R^2$ whose union contains a set $E\subseteq \mathbb R^2$.  Show that there is a pairwise disjoint subcollection $D_1,\ldots, D_n$ in $\mathcal F$ such that \[E\subseteq \cup_{j=1}^n 3D_j.\] Here, if $D$ is the disc of radius $r$ and center $P$, then $3D$ is the disc of radius $3r$ and center $P$.


Lean 4 formalization:
import Mathlib

open Set Function Metric

theorem putnam_1998_a5
  (k : ℕ)
  (c : Fin k → (EuclideanSpace ℝ (Fin 2)))
  (r : Fin k → ℝ)
  (hr : ∀ i, r i > 0)
  (E : Set (EuclideanSpace ℝ (Fin 2)))
  (hE : E ⊆ ⋃ i, ball (c i) (r i)) :
  ∃ (n : ℕ) (t : Fin n → Fin k),
    (∀ i j, i ≠ j → (ball (c (t i)) (r (t i)) ∩ ball (c (t j)) (r (t j)) = ∅)) ∧
    E ⊆ ⋃ i : Fin n, ball (c (t i)) (3 * (r (t i))) := by
Problem: putnam_1998_a6
Category: geometry

Let $A, B, C$ denote distinct points with integer coordinates in $\mathbb R^2$. Prove that if
\[(|AB|+|BC|)^2<8\cdot [ABC]+1\]
then $A, B, C$ are three vertices of a square. Here $|XY|$ is the length of segment $XY$ and $[ABC]$ is the area of triangle $ABC$.


Lean 4 formalization:
import Mathlib

open Set Function Metric
open scoped InnerProductSpace

theorem putnam_1998_a6
(A B C : EuclideanSpace ℝ (Fin 2))
(hint : ∀ i : Fin 2, ∃ a b c : ℤ, A i = a ∧ B i = b ∧ C i = c)
(htriangle : A ≠ B ∧ A ≠ C ∧ B ≠ C)
(harea : (dist A B + dist B C) ^ 2 < 8 * (MeasureTheory.volume (convexHull ℝ {A, B, C})).toReal + 1)
(threesquare : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → Prop)
(threesquare_def : threesquare = fun P Q R ↦ dist Q P = dist Q R ∧ ⟪P - Q, R - Q⟫_ℝ = 0)
: (threesquare A B C ∨ threesquare B C A ∨ threesquare C A B) := by
Problem: putnam_1998_b1
Category: algebra

Find the minimum value of \[\frac{(x+1/x)^6-(x^6+1/x^6)-2}{(x+1/x)^3+(x^3+1/x^3)}\] for $x>0$.

Solution: Show that the minimum value is 6.

Lean 4 formalization:
import Mathlib

open Set Function Metric

abbrev putnam_1998_b1_solution : ℝ := sorry
theorem putnam_1998_b1
: sInf {((x + 1/x)^6 - (x^6 + 1/x^6) - 2)/((x + 1/x)^3 + (x^3 + 1/x^3)) | x > (0 : ℝ)} = putnam_1998_b1_solution := by
Problem: putnam_1998_b2
Category: geometry, algebra

Given a point $(a,b)$ with $0<b<a$, determine the minimum perimeter of a triangle with one vertex at $(a,b)$, one on the $x$-axis, and one on the line $y=x$.  You may assume that a triangle of minimum perimeter exists.

Solution: Show that the solution is $\sqrt{2a^2 + 2b^2}.

Lean 4 formalization:
import Mathlib

open Set Function Metric

noncomputable abbrev putnam_1998_b2_solution : ℝ → ℝ → ℝ := sorry
theorem putnam_1998_b2
(a b : ℝ)
(hab : 0 < b ∧ b < a)
: sInf {d : ℝ | ∃ (c : ℝ) (x : ℝ), d = Real.sqrt ((a - c)^2 + (b - 0)^2) +  Real.sqrt ((c - x)^2 + (0 - x)^2) + Real.sqrt ((a - x)^2 + (b - x)^2) ∧
  Real.sqrt ((a - c)^2 + (b - 0)^2) + Real.sqrt ((c - x)^2 + (0 - x)^2) > Real.sqrt ((a - x)^2 + (b - x)^2) ∧
  Real.sqrt ((a - c)^2 + (b - 0)^2) + Real.sqrt ((a - x)^2 + (b - x)^2) > Real.sqrt ((c - x)^2 + (0 - x)^2) ∧
  Real.sqrt ((c - x)^2 + (0 - x)^2) + Real.sqrt ((a - x)^2 + (b - x)^2) > Real.sqrt ((a - c)^2 + (b - 0)^2)}
 = putnam_1998_b2_solution a b := by
Problem: putnam_1998_b4
Category: number_theory

Find necessary and sufficient conditions on positive integers $m$ and $n$ so that \[\sum_{i=0}^{mn-1} (-1)^{\lfloor i/m \rfloor +\lfloor i/n\rfloor}=0.\]

Solution: Show that the sum is 0 if and only if the largest powers of $2$ dividing $m$ and $n$ are different.

Lean 4 formalization:
import Mathlib

open Set Function Metric

abbrev putnam_1998_b4_solution : Set (ℕ × ℕ) := sorry
theorem putnam_1998_b4
  (quantity : ℕ → ℕ → ℤ)
  (hquantity : quantity = fun n m => ∑ i ∈ Finset.range (m * n), (-1)^(i/m + i/n))
  (n m : ℕ)
  (hnm : n > 0 ∧ m > 0) :
  quantity n m = 0 ↔ ⟨n, m⟩ ∈ putnam_1998_b4_solution := by