ChristianZ97/putnambench-satp-v4.27 huggingface dataset:
Problem: putnam_1975_b3
Category: analysis, algebra

Let $s_k (a_1, a_2, \dots, a_n)$ denote the $k$-th elementary symmetric function; that is, the sum of all $k$-fold products of the $a_i$. For example, $s_1 (a_1, \dots, a_n) = \sum_{i=1}^{n} a_i$, and $s_2 (a_1, a_2, a_3) = a_1a_2 + a_2a_3 + a_1a_3$. Find the supremum $M_k$ (which is never attained) of $$\frac{s_k (a_1, a_2, \dots, a_n)}{(s_1 (a_1, a_2, \dots, a_n))^k}$$ across all $n$-tuples $(a_1, a_2, \dots, a_n)$ of positive real numbers with $n \ge k$.

Solution: The supremum $M_k$ is $\frac{1}{k!}$.

Lean 4 formalization:
import Mathlib

open Polynomial Real Complex Matrix Filter Topology Multiset

noncomputable abbrev putnam_1975_b3_solution : ℕ → ℝ := sorry
theorem putnam_1975_b3
: ∀ k : ℕ, k > 0 → (∀ a : Multiset ℝ, (∀ i ∈ a, i > 0) ∧ card a ≥ k →
(esymm a k)/(esymm a 1)^k ≤ putnam_1975_b3_solution k) ∧
∀ M : ℝ, M < putnam_1975_b3_solution k → (∃ a : Multiset ℝ, (∀ i ∈ a, i > 0) ∧ card a ≥ k ∧
(esymm a k)/(esymm a 1)^k > M) := by
Problem: putnam_1975_b4
Category: analysis

Let $C = \{(x, y) \in \mathbb{R}^2 : x^2 + y^2 = 1\}$ denote the unit circle. Does there exist $B \subseteq C$ for which $B$ is topologically closed and contains exactly one point from each pair of diametrically opposite points in $C$?

Solution: Such $B$ does not exist.

Lean 4 formalization:
import Mathlib

open Polynomial Real Complex Matrix Filter Topology Multiset

abbrev putnam_1975_b4_solution : Prop := sorry
theorem putnam_1975_b4
(P : ℝ × ℝ → Prop)
(hP : P = fun (x, y) => x^2 + y^2 = 1)
: (∃ B ⊆ setOf P, IsClosed B ∧ ∀ x y : ℝ, P (x, y) → Xor' ((x, y) ∈ B) ((-x, -y) ∈ B)) ↔ putnam_1975_b4_solution := by
Problem: putnam_1975_b5
Category: analysis, algebra

Let $f_0(x) = e^x$ and $f_{n+1}(x) = xf'_n(x)$ for all $n \ge 0$. Prove that $$\sum_{n=0}^{\infty} \frac{f_n(1)}{n!} = e^e.$$


Lean 4 formalization:
import Mathlib

open Polynomial Real Complex Matrix Filter Topology Multiset

theorem putnam_1975_b5
(e : ℝ)
(he : e = Real.exp 1)
(f : ℕ → ℝ → ℝ)
(h0 : ∀ x : ℝ, f 0 x = e^x)
(hf : ∀ n : ℕ, ∀ x : ℝ, f (n + 1) x = x * (deriv (f n) x))
: ∑' n : ℕ, (f n 1)/(Nat.factorial n) = e^e := by
Problem: putnam_1975_b6
Category: analysis

Show that if $s_n = 1 + \frac{1}{2} + \frac{1}{3} + \dots + 1/n, then $n(n+1)^{1/n} < n + s_n$ whenever $n > 1$ and $(n-1)n^{-1/(n-1)} < n - s_n$ whenever $n > 2$.


Lean 4 formalization:
import Mathlib

open Polynomial Real Complex Matrix Filter Topology Multiset

theorem putnam_1975_b6
(s : ℕ → ℝ)
(hs : s = fun (n : ℕ) => ∑ i ∈ Finset.Icc 1 n, 1/(i : ℝ))
: (∀ n : ℕ, n > 1 → n * (n+1 : ℝ)^(1/(n : ℝ)) < n + s n) ∧ (∀ n : ℕ, n > 2 → ((n : ℝ) - 1)*((n : ℝ)^(-1/(n-1 : ℝ))) < n - s n) := by
Problem: putnam_1976_a2
Category: algebra

Let $P(x, y) = x^2y + xy^2$, $Q(x, y) = x^2 + xy + y^2$, $F_n(x, y) = (x + y)^n - x^n - y^n$, and $G_n(x, y) = (x + y)^n + x^n + y^n$. Prove that for all positive integers $n$, either $F_n$ or $G_n$ can be represented as a polynomial in $P$ and $Q$ with integer coefficients.


Lean 4 formalization:
import Mathlib

open MvPolynomial

theorem putnam_1976_a2
    (P Q : MvPolynomial (Fin 2) ℤ)
    (hP : P = X 0 ^ 2 * X 1 + X 0 * X 1 ^ 2)
    (hQ : Q = X 0 ^ 2 + X 0 * X 1 + X 1 ^ 2)
    (F G : ℕ → MvPolynomial (Fin 2) ℤ)
    (hF : ∀ n, F n = (X 0 + X 1) ^ n - X 0 ^ n - X 1 ^ n)
    (hG : ∀ n, G n = (X 0 + X 1) ^ n + X 0 ^ n + X 1 ^ n)
    (n : ℕ)
    (hn : 0 < n) :
    ∃ A : MvPolynomial (Fin 2) ℤ,
      F n = aeval ![P, Q] A ∨
      G n = aeval ![P, Q] A := by
Problem: putnam_1976_a3
Category: number_theory

Find all integer solutions $(p, r, q, s)$ of the equation $|p^r - q^s| = 1$, where $p$ and $q$ are prime and $r$ and $s$ are greater than $1$.

Solution: The only solutions are $(p, r, q, s) = (3, 2, 2, 3)$ and $(p, r, q, s) = (2, 3, 3, 2)$.

Lean 4 formalization:
import Mathlib

abbrev putnam_1976_a3_solution : Set (ℕ × ℕ × ℕ × ℕ) := sorry
theorem putnam_1976_a3
: {(p, r, q, s) : ℕ × ℕ × ℕ × ℕ | Nat.Prime p ∧ Nat.Prime q ∧ r > 1 ∧ s > 1 ∧ |(p^r : ℤ) - q^s| = 1} = putnam_1976_a3_solution := by
Problem: putnam_1976_a4
Category: algebra

Let $r$ be a real root of $P(x) = x^3 + ax^2 + bx - 1$, where $a$ and $b$ are integers and $P$ is irreducible over the rationals. Suppose that $r + 1$ is a root of $x^3 + cx^2 + dx + 1$, where $c$ and $d$ are also integers. Express another root $s$ of $P$ as a function of $r$ that does not depend on the values of $a$, $b$, $c$, or $d$.

Solution: The possible answers are $s = -\frac{1}{r + 1}$ and $s = -\frac{r + 1}{r}$.

Lean 4 formalization:
import Mathlib

open Polynomial

noncomputable abbrev putnam_1976_a4_solution : (ℝ → ℝ) × (ℝ → ℝ) := sorry
theorem putnam_1976_a4
(a b c d : ℤ)
(r : ℝ)
(P Q: Polynomial ℚ)
(hP : P = X^3 + (C (a : ℚ))*X^2 + (C (b : ℚ))*X - (C 1) ∧ aeval r P = 0 ∧ Irreducible P)
(hQ : Q =  X^3 + (C (c : ℚ))*X^2 + (C (d : ℚ))*X + (C 1) ∧ aeval (r + 1) Q = 0)
: ∃ s : ℝ, aeval s P = 0 ∧ (s = putnam_1976_a4_solution.1 r ∨ s = putnam_1976_a4_solution.2 r) := by
Problem: putnam_1976_a6
Category: analysis, algebra

Suppose that $f : \mathbb{R} \to \mathbb{R}$ is a twice continuously differentiable function such that $|f(x)| \le 1$ for all real $x$ and $(f(0))^2 + (f'(0))^2 = 4$. Prove that $f(y) + f''(y) = 0$ for some real number $y$.


Lean 4 formalization:
import Mathlib

open Polynomial

theorem putnam_1976_a6
(f : ℝ → ℝ)
(hfdiff : ContDiff ℝ 2 f)
(hfbd : ∀ x : ℝ, |f x| ≤ 1)
(hf0 : (f 0)^2 + (deriv f 0)^2 = 4)
: ∃ y : ℝ, (f y) + (iteratedDeriv 2 f y) = 0 := by
Problem: putnam_1976_b1
Category: analysis

Find $$\lim_{n \to \infty} \frac{1}{n} \sum_{k=1}^{n}\left(\left\lfloor \frac{2n}{k} \right\rfloor - 2\left\lfloor \frac{n}{k} \right\rfloor\right).$$ Your answer should be in the form $\ln(a) - b$, where $a$ and $b$ are positive integers.

Solution: The limit equals $\ln(4) - 1$, so $a = 4$ and $b = 1$.

Lean 4 formalization:
import Mathlib

open Polynomial Filter Topology

abbrev putnam_1976_b1_solution : ℕ × ℕ := sorry
theorem putnam_1976_b1
: Tendsto (fun n : ℕ => ((1 : ℝ)/n)*∑ k ∈ Finset.Icc (1 : ℤ) n, (Int.floor ((2*n)/k) - 2*Int.floor (n/k))) atTop
(𝓝 (Real.log putnam_1976_b1_solution.1 - putnam_1976_b1_solution.2)) := by
Problem: putnam_1976_b2
Category: abstract_algebra

Let $G$ be a group generated by two elements $A$ and $B$; i.e., every element of $G$ can be expressed as a finite word $A^{n_1}B^{n_2} \cdots A^{n_{k-1}}B^{n_k}$, where the $n_i$ can assume any integer values and $A^0 = B^0 = 1$. Further assume that $A^4 = B^7 = ABA^{-1}B = 1$, but $A^2 \ne 1$ and $B \ne 1$. Find the number of elements of $G$ than can be written as $C^2$ for some $C \in G$ and express each such square as a word in $A$ and $B$.

Solution: There are $8$ such squares: $1$, $A^2$, $B$, $B^2$, $B^3$, $B^4$, $B^5$, and $B^6$.

Lean 4 formalization:
import Mathlib

open Polynomial Filter Topology

abbrev putnam_1976_b2_solution : ℕ × Set (List (ℤ × ℤ)) := sorry
theorem putnam_1976_b2
(G : Type*) [Group G]
(A B : G)
(word : List (ℤ × ℤ) → G)
(hword : word = fun w : List (ℤ × ℤ) => (List.map (fun t : ℤ × ℤ => A^(t.1)*B^(t.2)) w).prod)
(hG : ∀ g : G, ∃ w : List (ℤ × ℤ), g = word w)
(hA : A^4 = 1 ∧ A^2 ≠ 1)
(hB : B^7 = 1 ∧ B ≠ 1)
(h1 : A*B*A^(-(1 : ℤ))*B = 1)
(S : Set G)
(hS : S = {g : G | ∃ C : G, C^2 = g})
: S.ncard = putnam_1976_b2_solution.1 ∧ S = {word w | w ∈ putnam_1976_b2_solution.2} := by
Problem: putnam_1976_b3
Category: probability

Suppose that we have $n$ events $A_1, \dots, A_n$, each of which has probability at least $1 - a$ of occufring, where $a < 1/4$. Further suppose that $A_i$ and $A_j$ are mutually independent if $|i-j| > 1$, although $A_i$ and $A_{i+1}$ may be dependent. Assume as known that the recurrence $u_{k+1} = u_k - au_{k-1}$, $u_0 = 1, u_1 = 1-a$ defines positive real numbers $u_k$ for $k = 0,1,\dots$. Show that the probability of all $A_1, \dots, A_n$ occurring is at least $u_n$.


Lean 4 formalization:
import Mathlib

open Polynomial Filter Topology ProbabilityTheory MeasureTheory

theorem putnam_1976_b3
(Ω : Type*)
[MeasurableSpace Ω]
(μ : Measure Ω)
[IsProbabilityMeasure μ]
(n : ℕ)
(hn : n ≥ 1)
(a : ℝ)
(ha : 0 ≤ a ∧ a < 1/4)
(u : ℕ → ℝ)
(hu01 : u 0 = 1 ∧ u 1 = 1 - a)
(huk : ∀ k ≥ 1, u (k + 1) = u k - a * (u (k-1)))
(hupos : ∀ k : ℕ, u k > 0)
(events : Fin n → Set Ω)
(heventsmeas : ∀ i : Fin n, MeasurableSet (events i))
(heventsprob : ∀ i : Fin n, μ (events i) ≥ ENNReal.ofReal (1 - a))
(heventsindep : ∀ i : Fin n,
  ProbabilityTheory.Indep (MeasurableSpace.generateFrom {events i})
    (MeasurableSpace.generateFrom (Set.image events {j : Fin n | (j : ℤ) < (i : ℤ) - 1})) μ)
: μ (⋂ i : Fin n, events i) ≥ ENNReal.ofReal (u n) := by
Problem: putnam_1976_b5
Category: algebra

Find $$\sum_{k=0}^{n} (-1)^k {n \choose k} (x - k)^n.$$

Solution: The sum equals $n!$.

Lean 4 formalization:
import Mathlib

open Polynomial Filter Topology ProbabilityTheory MeasureTheory

noncomputable abbrev putnam_1976_b5_solution : ℕ → Polynomial ℤ := sorry
theorem putnam_1976_b5
: ∀ n : ℕ, ∑ k ∈ Finset.range (n + 1), C ((-(1 : ℤ))^k * Nat.choose n k) * (X - (C (k : ℤ)))^n = putnam_1976_b5_solution n := by
Problem: putnam_1976_b6
Category: number_theory

Let $\sigma(N)$ denote the sum of all positive integer divisors of $N$, including $1$ and $N$. Call a positive integer $N$ \textit{quasiperfect} if $\sigma(N) = 2N + 1$. Prove that every quasiperfect number is the square of an odd integer.


Lean 4 formalization:
import Mathlib

open Polynomial Filter Topology ProbabilityTheory MeasureTheory

theorem putnam_1976_b6
(σ : ℕ → ℤ)
(hσ : σ = fun N : ℕ => ∑ d ∈ Nat.divisors N, (d : ℤ))
(quasiperfect : ℕ → Prop)
(quasiperfect_def : ∀ N, quasiperfect N ↔ σ N = 2*N + 1)
: ∀ N : ℕ, quasiperfect N → ∃ m : ℤ, Odd m ∧ m^2 = N := by
Problem: putnam_1977_a1
Category: algebra

Show that if four distinct points of the curve $y = 2x^4 + 7x^3 + 3x - 5$ are collinear, then their average $x$-coordinate is some constant $k$. Find $k$.

Solution: Prove that $k = -\frac{7}{8}$.

Lean 4 formalization:
import Mathlib

noncomputable abbrev putnam_1977_a1_solution : ℝ := sorry
theorem putnam_1977_a1
(y : ℝ → ℝ)
(hy : y = fun x ↦ 2 * x ^ 4 + 7 * x ^ 3 + 3 * x - 5)
(S : Finset ℝ)
(hS : S.card = 4)
: (Collinear ℝ {P : Fin 2 → ℝ | P 0 ∈ S ∧ P 1 = y (P 0)} → (∑ x ∈ S, x) / 4 = putnam_1977_a1_solution) := by
Problem: putnam_1977_a2
Category: algebra

Find all real solutions $(a, b, c, d)$ to the equations $a + b + c = d$, $\frac{1}{a} + \frac{1}{b} + \frac{1}{c} = \frac{1}{d}$.

Solution: Prove that the solutions are $d = a$ and $b = -c$, $d = b$ and $a = -c$, or $d = c$ and $a = -b$, with $a, b, c, d$ nonzero.

Lean 4 formalization:
import Mathlib

abbrev putnam_1977_a2_solution : ℝ → ℝ → ℝ → ℝ → Prop := sorry
theorem putnam_1977_a2 :
    ∀ a b c d : ℝ,
      a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 →
        (putnam_1977_a2_solution a b c d ↔
          (a + b + c = d ∧ 1 / a + 1 / b + 1 / c = 1 / d)) := by
Problem: putnam_1977_a3
Category: algebra

Let $f, g, h$ be functions $\mathbb{R} \to \mathbb{R}$. Find an expression for $h(x)$ in terms of $f$ and $g$ such that $f(x) = \frac{h(x + 1) + h(x - 1)}{2}$ and $g(x) = \frac{h(x + 4) + h(x - 4)}{2}$.

Solution: Prove that $h(x) = g(x) - f(x - 3) + f(x - 1) + f(x + 1) - f(x + 3)$ suffices.

Lean 4 formalization:
import Mathlib

abbrev putnam_1977_a3_solution : (ℝ → ℝ) → (ℝ → ℝ) → (ℝ → ℝ) := sorry
theorem putnam_1977_a3
    (f g h : ℝ → ℝ)
    (hf : ∀ x, f x = (h (x + 1) + h (x - 1)) / 2)
    (hg : ∀ x, g x = (h (x + 4) + h (x - 4)) / 2) :
    h = putnam_1977_a3_solution f g := by
Problem: putnam_1977_a4
Category: algebra, analysis

Find $\sum_{n=0}^{\infty} \frac{x^{2^n}}{1 - x^{2^{n+1}}}$ as a rational function of $x$ for $x \in (0, 1)$.

Solution: Prove that the sum equals $\frac{x}{1 - x}$.

Lean 4 formalization:
import Mathlib

open RingHom Set

noncomputable abbrev putnam_1977_a4_solution : RatFunc ℝ := sorry
theorem putnam_1977_a4 :
    ∀ x ∈ Ioo 0 1,
      putnam_1977_a4_solution.eval (id ℝ) x = ∑' n : ℕ, x ^ 2 ^ n / (1 - x ^ 2 ^ (n + 1)) := by
Problem: putnam_1977_a5
Category: algebra, number_theory

Let $p$ be a prime and $m \geq n$ be non-negative integers. Show that $\binom{pm}{pn} = \binom{m}{n} \pmod p$, where $\binom{m}{n}$ is the binomial coefficient.


Lean 4 formalization:
import Mathlib

open RingHom Set Nat

theorem putnam_1977_a5
(p m n : ℕ)
(hp : Nat.Prime p)
(hmgen : m ≥ n)
: (choose (p * m) (p * n) ≡ choose m n [MOD p]) := by
Problem: putnam_1977_a6
Category: analysis

Let $X$ be the square $[0, 1] \times [0, 1]$, and let $f : X \to \mathbb{R}$ be continuous. If $\int_Y f(x, y) \, dx \, dy = 0$ for all squares $Y$ such that
\begin{itemize}
\item[(1)] $Y \subseteq X$,
\item[(2)] $Y$ has sides parallel to those of $X$,
\item[(3)] at least one of $Y$'s sides is contained in the boundary of $X$,
\end{itemize}
is it true that $f(x, y) = 0$ for all $x, y$?

Solution: Prove that $f(x,y)$ must be identically zero.

Lean 4 formalization:
import Mathlib

open RingHom Set Nat

abbrev putnam_1977_a6_solution : Prop := sorry
theorem putnam_1977_a6
(X : Set (ℝ × ℝ))
(hX : X = Set.prod (Icc 0 1) (Icc 0 1))
(room : (ℝ × ℝ) → ℝ)
(hroom : room = fun (a,b) ↦ min (min a (1 - a)) (min b (1 - b)))
: ((∀ f : (ℝ × ℝ) → ℝ, Continuous f → (∀ P ∈ X, ∫ x in (P.1 - room P)..(P.1 + room P), ∫ y in (P.2 - room P)..(P.2 + room P), f (x, y) = 0) → (∀ P ∈ X, f P = 0)) ↔ putnam_1977_a6_solution) := by
Problem: putnam_1977_b1
Category: algebra, analysis

Find $\prod_{n=2}^{\infty} \frac{(n^3 - 1)}{(n^3 + 1)}$.

Solution: Prove that the product equals $\frac{2}{3}$.

Lean 4 formalization:
import Mathlib

open RingHom Set Nat Filter Topology

noncomputable abbrev putnam_1977_b1_solution : ℝ := sorry
theorem putnam_1977_b1
: Tendsto (fun N ↦ ∏ n ∈ Finset.Icc (2 : ℤ) N, ((n : ℝ) ^ 3 - 1) / (n ^ 3 + 1)) atTop (𝓝 putnam_1977_b1_solution) := by
Problem: putnam_1977_b3
Category: algebra

An ordered triple $(a, b, c)$ of positive irrational numbers with $a + b + c = 1$ is considered $\textit{balanced}$ if all three elements are less than $\frac{1}{2}$. If a triple is not balanced, we can perform a ``balancing act'' $B$ defined by $B(a, b, c) = (f(a), f(b), f(c))$, where $f(x) = 2x - 1$ if $x > 1/2$ and $f(x) = 2x$ otherwise. Will finitely many iterations of this balancing act always eventually produce a balanced triple?

Solution: Not necessarily.

Lean 4 formalization:
import Mathlib

open RingHom Set Nat Filter Topology

abbrev putnam_1977_b3_solution : Prop := sorry
theorem putnam_1977_b3
(P balanced: ℝ × ℝ × ℝ → Prop)
(B : ℝ × ℝ × ℝ → ℝ × ℝ × ℝ)
(hP : P = fun (a, b, c) => Irrational a ∧ Irrational b ∧ Irrational c ∧ a > 0 ∧ b > 0 ∧ c > 0 ∧ a + b + c = 1)
(hbalanced : balanced = fun (a, b, c) => a < 1/2 ∧ b < 1/2 ∧ c < 1/2)
(hB : B = fun (a, b, c) => (ite (a > 1/2) (2*a - 1) (2*a), ite (b > 1/2) (2*b - 1) (2*b), ite (c > 1/2) (2*c - 1) (2*c)))
: (∀ t : ℝ × ℝ × ℝ, P t → ∃ n : ℕ, balanced (B^[n] t)) ↔ putnam_1977_b3_solution := by
Problem: putnam_1977_b5
Category: algebra

If $a_1, a_2, \dots, a_n$ are real numbers with $n > 1$ and $A$ satisfies $$A + \sum_{i = 1}^{n} a_i^2 < \frac{1}{n-1}\left(\sum_{i=1}^{n}a_i\right)^2,$$ prove that $A < 2a_{i}a_{j}$ for all $i, j$ with $1 \le i < j \le n$.


Lean 4 formalization:
import Mathlib

open RingHom Set Nat Filter Topology

theorem putnam_1977_b5
(n : ℕ)
(hn : n > 1)
(a : Fin n → ℝ)
(A : ℝ)
(hA : A + ∑ i : Fin n, (a i)^2 < (1/((n : ℝ) - 1))*(∑ i : Fin n, a i)^2)
: ∀ i j : Fin n, i < j → A < 2*(a i)*(a j) := by
Problem: putnam_1977_b6
Category: abstract_algebra

Let $G$ be a group and $H$ be a subgroup of $G$ with $h$ elements. Suppose that $G$ contains some element $a$ such that $(xa)^3 = 1$ for all $x \in H$ (here $1$ represents the identity element of $G$). Let $P$ be the subset of $G$ containing all products of the form $x_1 a x_2 a \cdots x_n a$ with $n \ge 1$ and $x_i \in H$ for all $i \in \{1, 2, \dots, n\}$. Prove that $P$ is a finite set and contains no more than $3h^2$ elements.


Lean 4 formalization:
import Mathlib

open RingHom Set Nat Filter Topology

theorem putnam_1977_b6
{G : Type*}
[Group G]
(H : Subgroup G)
[Finite H]
(h : ℕ)
(h_def : h = Nat.card H)
(a : G)
(ha : ∀ x : H, (x*a)^3 = 1)
(P : Set G)
(hP : P = {g : G | ∃ xs : List H, (xs.length ≥ 1) ∧ g = (List.map (fun h : H => h*a) xs).prod})
: (Finite P) ∧ (P.ncard ≤ 3*h^2) := by
Problem: putnam_1978_a1
Category: algebra

Let $S = \{1, 4, 7, 10, 13, 16, \dots , 100\}$. Let $T$ be a subset of $20$ elements of $S$. Show that we can find two distinct elements of $T$ with sum $104$.


Lean 4 formalization:
import Mathlib

theorem putnam_1978_a1
(S T : Set ℤ)
(hS : S = {k | ∃ j : ℤ, 0 ≤ j ∧ j ≤ 33 ∧ k = 3 * j + 1})
(hT : T ⊆ S ∧ T.ncard = 20)
: (∃ m ∈ T, ∃ n ∈ T, m ≠ n ∧ m + n = 104) := by
Problem: putnam_1978_a2
Category: linear_algebra

Let $A$ be the real $n \times n$ matrix $(a_{ij})$ where $a_{ij} = a$ for $i < j$, $b \; (\neq a)$ for $i > j$, and $c_i$ for $i = j$. Show that $\det A = \frac{b p(a) - a p(b)}{b - a}$, where $p(x) = \prod_{i=1}^n (c_i - x)$.


Lean 4 formalization:
import Mathlib

theorem putnam_1978_a2
(n : ℕ)
(npos : n > 0)
(a b : ℝ)
(hab : a ≠ b)
(c : Fin n → ℝ)
(A : Matrix (Fin n) (Fin n) ℝ)
(hA : A = fun i j ↦ ite (i < j) a (ite (i > j) b (c i)))
(p : ℝ → ℝ)
(hp : p = fun x ↦ ∏ i : Fin n, (c i - x))
: (A.det = ((b * p a - a * p b) / (b - a))) := by
Problem: putnam_1978_a3
Category: analysis, algebra

Let $p(x) = 2(x^6 + 1) + 4(x^5 + x) + 3(x^4 + x^2) + 5x^3$. For $k$ with $0 < k < 5$, let
\[
I_k = \int_0^{\infty} \frac{x^k}{p(x)} \, dx.
\]
For which $k$ is $I_k$ smallest?

Solution: Show that $I_k$ is smallest for $k = 2$.

Lean 4 formalization:
import Mathlib

open Set Polynomial

abbrev putnam_1978_a3_solution : ℕ := sorry
theorem putnam_1978_a3
    (p : Polynomial ℝ)
    (hp : p = 2 * (X ^ 6 + 1) + 4 * (X ^ 5 + X) + 3 * (X ^ 4 + X ^ 2) + 5 * X ^ 3)
    (I : ℕ → ℝ)
    (hI : I = fun k ↦ ∫ x in Ioi 0, x ^ k / p.eval x) :
    IsLeast {y | ∃ k ∈ Ioo 0 5, I k = y} (I putnam_1978_a3_solution) := by
Problem: putnam_1978_a4
Category: abstract_algebra

A binary operation (represented by multiplication) on $S$ has the property that $(ab)(cd) = ad$ for all $a, b, c, d$. Show that:
\begin{itemize}
\item[(1)] if $ab = c$, then $cc = c$;
\item[(2)] if $ab = c$, then $ad = cd$ for all $d$.
\end{itemize}
Find a set $S$, and such a binary operation, which also satisfies:
\begin{itemize}
\item[(A)] $a a = a$ for all $a$;
\item[(B)] $ab = a \neq b$ for some $a, b$;
\item[(C)] $ab \neq a$ for some $a, b$.
\end{itemize}


Lean 4 formalization:
import Mathlib

open Set

theorem putnam_1978_a4
(bypass : (S : Type) → [inst : Mul S] → Prop)
(hbypass : bypass = fun S [Mul S] ↦ ∀ a b c d : S, (a * b) * (c * d) = a * d)
: ((∀ (S : Type) (_ : Mul S), bypass S → ∀ a b c : S, a * b = c → (c * c = c ∧ ∀ d : S, a * d = c * d))
  ∧ (∃ (S : Type) (_ : Mul S) (_ : Fintype S), bypass S ∧ (∀ a : S, a * a = a) ∧ (∃ a b : S, a * b = a ∧ a ≠ b) ∧ (∃ a b : S, a * b ≠ a))) := by
Problem: putnam_1978_a5
Category: analysis

Let $a_1, a_2, \dots , a_n$ be reals in the interval $(0, \pi)$ with arithmetic mean $\mu$. Show that
\[
\prod_{i=1}^n \left( \frac{\sin a_i}{a_i} \right) \leq \left( \frac{\sin \mu}{\mu} \right)^n.
\]


Lean 4 formalization:
import Mathlib

open Set Real

theorem putnam_1978_a5
(n : ℕ)
(npos : n > 0)
(a : Fin n → ℝ)
(ha : ∀ i : Fin n, a i ∈ Ioo 0 Real.pi)
(μ : ℝ)
(hμ : μ = ∑ i : Fin n, a i / n)
: (∏ i : Fin n, sin (a i) / (a i) ≤ (sin μ / μ) ^ n) := by
Problem: putnam_1978_a6
Category: geometry, combinatorics

Given $n$ distinct points in the plane, prove that fewer than $2n^{3/2}$ pairs of these points are a distance of $1$ apart.


Lean 4 formalization:
import Mathlib

open Set Real

theorem putnam_1978_a6
(S : Finset (EuclideanSpace ℝ (Fin 2)))
(n : ℕ)
(hn : n = S.card)
(npos : n > 0)
: ({pair : Set (EuclideanSpace ℝ (Fin 2)) | ∃ P ∈ S, ∃ Q ∈ S, pair = {P, Q} ∧ dist P Q = 1}.ncard < 2 * (n : ℝ) ^ ((3 : ℝ) / 2)) := by
Problem: putnam_1978_b2
Category: algebra, analysis

Find
\[
\sum_{i=1}^{\infty} \sum_{j=1}^{\infty} \frac{1}{i^2j + 2ij + ij^2}.
\]

Solution: Prove that the sum evaluates to $\frac{7}{4}$.

Lean 4 formalization:
import Mathlib

open Set Real

abbrev putnam_1978_b2_solution : ℚ := sorry
theorem putnam_1978_b2
: (∑' i : ℕ+, ∑' j : ℕ+, (1 : ℚ) / (i ^ 2 * j + 2 * i * j + i * j ^ 2) = putnam_1978_b2_solution) := by
Problem: putnam_1978_b3
Category: algebra, analysis

The polynomials $P_n(x)$ are defined by
\begin{align*}
P_1(x) &= 1 + x, \\
P_2(x) &= 1 + 2x, \\
P_{2n+1}(x) &= P_{2n}(x) + (n + 1) x P_{2n-1}(x), \\
P_{2n+2}(x) &= P_{2n+1}(x) + (n + 1) x P_{2n}(x).
\end{align*}
Let $a_n$ be the largest real root of $P_n(x)$. Prove that $a_n$ is strictly monotonically increasing and tends to zero.


Lean 4 formalization:
import Mathlib

open Set Real Filter Topology Polynomial

theorem putnam_1978_b3
(P : ℕ+ → Polynomial ℝ)
(hP1 : P 1 = 1 + X)
(hP2 : P 2 = 1 + 2 * X)
(hPodd : ∀ n, P (2 * n + 1) = P (2 * n) + C ((n : ℝ) + 1) * X * P (2 * n - 1))
(hPeven : ∀ n, P (2 * n + 2) = P (2 * n + 1) + C ((n : ℝ) + 1) * X * P (2 * n))
(a : ℕ+ → ℝ)
(haroot : ∀ n, (P n).eval (a n) = 0)
(haub : ∀ n, ∀ x, (P n).eval x = 0 → x ≤ a n)
: (StrictMono a ∧ Tendsto a atTop (𝓝 0)) := by
Problem: putnam_1978_b4
Category: algebra

Show that we can find integers $a, b, c, d$ such that $a^2 + b^2 + c^2 + d^2 = abc + abd + acd + bcd$, and the smallest of $a, b, c, d$ is arbitrarily large.


Lean 4 formalization:
import Mathlib

open Set Real Filter Topology Polynomial

theorem putnam_1978_b4 :
  ∀ N : ℝ,
    ∃ a b c d : ℤ,
      a > N ∧ b > N ∧ c > N ∧ d > N ∧
      a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = a * b * c + a * b * d + a * c * d + b * c * d := by
Problem: putnam_1978_b5
Category: algebra

Find the real polynomial $p(x)$ of degree $4$ with largest possible coefficient of $x^4$ such that $p([-1, 1]) \subseteq [0, 1]$.

Solution: Prove that $p(x) = 4x^4 - 4x^2 + 1$.

Lean 4 formalization:
import Mathlib

open Set Real Filter Topology Polynomial

noncomputable abbrev putnam_1978_b5_solution : Polynomial ℝ := sorry
theorem putnam_1978_b5
(S : Set (Polynomial ℝ))
(hS : S = {p : Polynomial ℝ | p.degree = 4 ∧ ∀ x ∈ Icc (-1) 1, p.eval x ∈ Icc 0 1})
: (putnam_1978_b5_solution ∈ S ∧ (∀ p ∈ S, p.coeff 4 ≤ putnam_1978_b5_solution.coeff 4)) := by
Problem: putnam_1978_b6
Category: algebra

Let $a_{ij}$ be real numbers in $[0, 1]$. Show that
\[
\left( \sum_{i=1}^n  \sum_{j=1}^{mi} \frac{a_{ij}}{i} \right) ^2 \leq 2m \sum_{i=1}^n \sum_{j=1}^{mi} a_{ij}.
\]


Lean 4 formalization:
import Mathlib

open Set Real Filter Topology Polynomial

theorem putnam_1978_b6
(a : ℕ → ℕ → ℝ)
(ha : ∀ i j, a i j ∈ Icc 0 1)
(m n : ℕ)
(mnpos : m > 0 ∧ n > 0)
: ((∑ i ∈ Finset.Icc 1 n, ∑ j ∈ Finset.Icc 1 (m * i), a i j / i) ^ 2 ≤ 2 * m * ∑ i ∈ Finset.Icc 1 n, ∑ j ∈ Finset.Icc 1 (m * i), a i j) := by
Problem: putnam_1979_a1
Category: algebra

For which positive integers $n$ and $a_1, a_2, \dots, a_n$ with $\sum_{i = 1}^{n} a_i = 1979$ does $\prod_{i = 1}^{n} a_i$ attain the greatest value?

Solution: $n$ equals $660$; all but one of the $a_i$ equal $3$ and the remaining $a_i$ equals $2$.

Lean 4 formalization:
import Mathlib

abbrev putnam_1979_a1_solution : Multiset ℕ := sorry
theorem putnam_1979_a1
    (P : Multiset ℕ → Prop)
    (hP : ∀ a, P a ↔ Multiset.card a > 0 ∧ (∀ i ∈ a, i > 0) ∧ a.sum = 1979) :
    P putnam_1979_a1_solution ∧ ∀ a : Multiset ℕ, P a → putnam_1979_a1_solution.prod ≥ a.prod := by
Problem: putnam_1979_a2
Category: analysis, algebra

For which real numbers $k$ does there exist a continuous function $f : \mathbb{R} \to \mathbb{R}$ such that $f(f(x)) = kx^9$ for all real $x$?

Solution: Such a function exists if and only if $k \ge 0$.

Lean 4 formalization:
import Mathlib

abbrev putnam_1979_a2_solution : ℝ → Prop := sorry
theorem putnam_1979_a2
: ∀ k : ℝ, (∃ f : ℝ → ℝ, Continuous f ∧ ∀ x : ℝ, f (f x) = k*x^9) ↔ putnam_1979_a2_solution k := by