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

Let $n$ be a positive odd integer and let $\theta$ be a real number such that $\theta/\pi$ is irrational. Set $a_k=\tan(\theta+k\pi/n)$, $k=1,2,\dots,n$. Prove that $\frac{a_1+a_2+\cdots+a_n}{a_1a_2 \cdots a_n}$ is an integer, and determine its value.

Solution: Show that $\frac{a_1+\cdots+a_n}{a_1 \cdots a_n}=\begin{cases} n & n \equiv 1 \pmod{4} \\ -n & n \equiv 3 \pmod{4}. \end{cases}$

Lean 4 formalization:
import Mathlib

abbrev putnam_2006_a5_solution : ℕ → ℤ := sorry
theorem putnam_2006_a5
(n : ℕ)
(theta : ℝ)
(a : Set.Icc 1 n → ℝ)
(nodd : Odd n)
(thetairr : Irrational (theta / Real.pi))
(ha : ∀ k : Set.Icc 1 n, a k = Real.tan (theta + (k * Real.pi) / n))
: (∑ k : Set.Icc 1 n, a k) / (∏ k : Set.Icc 1 n, a k) = putnam_2006_a5_solution n := by
Problem: putnam_2006_b1
Category: geometry

Show that the curve $x^3 + 3xy + y^3 = 1$ contains only one set of three distinct points, $A$, $B$, and $C$, which are vertices of an equilateral triangle, and find its area.

Solution: Prove that the triangle has area $\frac{3 \sqrt 3}{2}$.

Lean 4 formalization:
import Mathlib

noncomputable abbrev putnam_2006_b1_solution : ℝ := sorry
theorem putnam_2006_b1
  (curve : Set (ℝ × ℝ))
  (hcurve : curve = {(x, y) | x ^ 3 + 3 * x * y + y ^ 3 = 1})
  (equilateral : Set (ℝ × ℝ) → Prop)
  (hequilateral : ∀ S, equilateral S ↔ S.encard = 3 ∧
    ∃ d : ℝ, ∀ P ∈ S, ∀ Q ∈ S, P ≠ Q →
    Real.sqrt ((P.1 - Q.1)^2 + (P.2 - Q.2)^2) = d) :
  (∃! S : Set (ℝ × ℝ), S ⊆ curve ∧ equilateral S) ∧
  (∃ S : Set (ℝ × ℝ), S ⊆ curve ∧ equilateral S ∧ (MeasureTheory.volume (convexHull ℝ S)).toReal = putnam_2006_b1_solution) := by
Problem: putnam_2006_b2
Category: analysis

Prove that, for every set $X = \{x_1, x_2, \dots, x_n\}$ of $n$ real numbers, there exists a non-empty subset $S$ of $X$ and an integer $m$ such that
\[
\left| m + \sum_{s \in S} s \right| \leq \frac{1}{n+1}.
\]


Lean 4 formalization:
import Mathlib

theorem putnam_2006_b2
(n : ℕ)
(npos : n > 0)
(X : Finset ℝ)
(hXcard : X.card = n)
: (∃ S ⊆ X, S ≠ ∅ ∧ ∃ m : ℤ, |m + ∑ s ∈ S, s| ≤ 1 / (n + 1)) := by
Problem: putnam_2006_b3
Category: geometry

Let $S$ be a finite set of points in the plane. A linear partition of $S$ is an unordered pair $\{A,B\}$ of subsets of $S$ such that $A \cup B=S$, $A \cap B=\emptyset$, and $A$ and $B$ lie on opposite sides of some straight line disjoint from $S$ ($A$ or $B$ may be empty). Let $L_S$ be the number of linear partitions of $S$. For each positive integer $n$, find the maximum of $L_S$ over all sets $S$ of $n$ points.

Solution: Show that the maximum is $\binom{n}{2}+1$.

Lean 4 formalization:
import Mathlib

abbrev putnam_2006_b3_solution : ℕ → ℕ := sorry
theorem putnam_2006_b3
    (IsLinearPartition : Finset (Fin 2 → ℝ) → Finset (Finset (Fin 2 → ℝ)) → Prop)
    (IsLinearPartition_def : ∀ S AB, IsLinearPartition S AB ↔
      (AB.card = 2 ∧ ∃ A ∈ AB, ∃ B ∈ AB,
        A ≠ B ∧ (A ∪ B = S) ∧ (A ∩ B = ∅) ∧
        (∃ m b : ℝ,
          (∀ p ∈ A, p 1 > m * p 0 + b) ∧
          (∀ p ∈ B, p 1 < m * p 0 + b))))
    (L : Finset (Fin 2 → ℝ) → ℕ)
    (hL : ∀ S, L S = {AB | IsLinearPartition S AB}.encard)
    (n : ℕ) (npos : 0 < n) :
    IsGreatest {L S | (S) (hS : S.card = n)} (putnam_2006_b3_solution n) := by
Problem: putnam_2006_b4
Category: linear_algebra

Let $Z$ denote the set of points in $\mathbb{R}^n$ whose coordinates are $0$ or $1$. (Thus $Z$ has $2^n$ elements, which are the vertices of a unit hypercube in $\mathbb{R}^n$.) Given a vector subspace $V$ of $\mathbb{R}^n$, let $Z(V)$ denote the number of members of $Z$ that lie in $V$. Let $k$ be given, $0 \leq k \leq n$. Find the maximum, over all vector subspaces $V \subseteq \mathbb{R}^n$ of dimension $k$, of the number of points in $V \cap Z$.

Solution: Prove that the maximum is $2^k$.

Lean 4 formalization:
import Mathlib

noncomputable abbrev putnam_2006_b4_solution : ℕ → ℕ := sorry
theorem putnam_2006_b4
    (n k : ℕ)
    (npos : n > 0)
    (hk : k ≤ n)
    (Z : Set (Fin n → ℝ))
    (hZ : Z = {P : Fin n → ℝ | ∀ j : Fin n, P j = 0 ∨ P j = 1}) :
    IsGreatest
      {y | ∃ V : Subspace ℝ (Fin n → ℝ), Module.rank ℝ V = k ∧ (Z ∩ V).ncard = y}
      (putnam_2006_b4_solution k) := by
Problem: putnam_2006_b5
Category: analysis, algebra

For each continuous function $f: [0,1] \to \mathbb{R}$, let $I(f) = \int_0^1 x^2 f(x)\,dx$ and $J(x) = \int_0^1 x \left(f(x)\right)^2\,dx$. Find the maximum value of $I(f) - J(f)$ over all such functions $f$.

Solution: Show that the answer is \frac{1}{16}.

Lean 4 formalization:
import Mathlib

open Set

noncomputable abbrev putnam_2006_b5_solution : ℝ := sorry
theorem putnam_2006_b5
  (I J : (ℝ → ℝ) → ℝ)
  (hI : I = fun f ↦ ∫ x in (0)..1, x ^ 2 * (f x))
  (hJ : J = fun f ↦ ∫ x in (0)..1, x * (f x) ^ 2) :
  IsGreatest
    {y | ∃ f : ℝ → ℝ, ContinuousOn f (Icc 0 1) ∧ I f - J f = y}
    putnam_2006_b5_solution := by
Problem: putnam_2006_b6
Category: analysis

Let $k$ be an integer greater than 1. Suppose $a_0 > 0$, and define \[ a_{n+1} = a_n + \frac{1}{\sqrt[k]{a_n}} \] for $n > 0$. Evaluate \[\lim_{n \to \infty} \frac{a_n^{k+1}}{n^k}.\]

Solution: Show that the solution is $(\frac{k+1}{k})^k$.

Lean 4 formalization:
import Mathlib

open Set Topology Filter

noncomputable abbrev putnam_2006_b6_solution : ℕ → ℝ := sorry
theorem putnam_2006_b6
(k : ℕ)
(hk : k > 1)
(a : ℕ → ℝ)
(ha0 : a 0 > 0)
(ha : ∀ n : ℕ, a (n + 1) = a n + 1/((a n)^((1 : ℝ)/k)))
: Tendsto (fun n => (a n)^(k+1)/(n ^ k)) atTop (𝓝 (putnam_2006_b6_solution k)) := by
Problem: putnam_2007_a1
Category: algebra, geometry

Find all values of $\alpha$ for which the curves $y = \alpha*x^2 + \alpha*x + 1/24$ and $x = \alpha*y^2 + \alpha*y + 1/24$ are tangent to each other.

Solution: Show that the solution is the set \{2/3, 3/2, (13 + \sqrt{601})/12, (13 - \sqrt{601})/12}.

Lean 4 formalization:
import Mathlib

abbrev putnam_2007_a1_solution : Set ℝ := sorry

theorem putnam_2007_a1
    (P : (ℝ → ℝ) → Prop)
    (P_def : ∀ f, P f ↔ ∃ x y, f x = y ∧ f y = x ∧ deriv f x * deriv f y = 1)
    (α : ℝ) :
    P (fun t ↦ α * t ^ 2 + α * t + 1 / 24) ↔ α ∈ putnam_2007_a1_solution := by
Problem: putnam_2007_a2
Category: geometry

Find the least possible area of a convex set in the plane that intersects both branches of the hyperbola $xy=1$ and both branches of the hyperbola $xy=-1$. (A set $S$ in the plane is called \emph{convex} if for any two points in $S$ the line segment connecting them is contained in $S$.)

Solution: Show that the minimum is $4$.

Lean 4 formalization:
import Mathlib

open MeasureTheory

noncomputable abbrev putnam_2007_a2_solution : ENNReal := sorry
theorem putnam_2007_a2 :
  IsLeast
    {y | ∃ S : Set (Fin 2 → ℝ),
      Convex ℝ S ∧
      (∃ p ∈ S, p 0 > 0 ∧ p 1 > 0 ∧ p 0 * p 1 = 1) ∧
      (∃ p ∈ S, p 0 < 0 ∧ p 1 < 0 ∧ p 0 * p 1 = 1) ∧
      (∃ p ∈ S, p 0 < 0 ∧ p 1 > 0 ∧ p 0 * p 1 = -1) ∧
      (∃ p ∈ S, p 0 > 0 ∧ p 1 < 0 ∧ p 0 * p 1 = -1) ∧
    volume S = y} putnam_2007_a2_solution := by
Problem: putnam_2007_a3
Category: combinatorics

Let $k$ be a positive integer. Suppose that the integers $1, 2, 3, \dots, 3k+1$ are written down in random order. What is the probability that at no time during this process, the sum of the integers that have been written up to that time is a positive integer divisible by $3$? Your answer should be in closed form, but may include factorials.

Solution: Prove that the desired probability is $\frac{k!(k+1)!}{(3k+1)(2k)!}$.

Lean 4 formalization:
import Mathlib

open Set
open scoped Nat

abbrev putnam_2007_a3_solution : ℕ → ℚ := sorry
theorem putnam_2007_a3
(k : ℕ)
(kpos : k > 0)
(perms : Set (Fin (3 * k + 1) → ℤ))
(goodperms : Set (Fin (3 * k + 1) → ℤ))
(hgoodperms : goodperms = {f ∈ perms | ¬∃ j : Fin (3 * k + 1), 3 ∣ ∑ i : Fin (3 * k + 1), ite (i ≤ j) (f i) 0})
(hperms : perms = {f : Fin (3 * k + 1) → ℤ | ∀ y ∈ Icc 1 (3 * k + 1), ∃! x : Fin (3 * k + 1), f x = y})
: (goodperms.ncard = perms.ncard * (putnam_2007_a3_solution k)) := by
Problem: putnam_2007_a4
Category: analysis, algebra, number_theory

A \emph{repunit} is a positive integer whose digits in base 10 are all ones. Find all polynomials $f$ with real coefficients such that if $n$ is a repunit, then so is $f(n)$.

Solution: Show that the desired polynomials $f$ are those of the form
\[
f(n) = \frac{1}{9}(10^c (9n+1)^d - 1)
\]
for integers $d \geq 0$ and $c \geq 1-d$.

Lean 4 formalization:
import Mathlib

open Set Nat

abbrev putnam_2007_a4_solution : Set (Polynomial ℝ) := sorry
theorem putnam_2007_a4
(S : Set (Polynomial ℝ))
(repunit : ℝ → Prop)
(hrepunit : ∀ x, repunit x ↔ x > 0 ∧ x = floor x ∧ ∀ d ∈ (digits 10 (floor x)), d = 1)
(hS : ∀ f, f ∈ S ↔ (∀ n : ℝ, repunit n → repunit (f.eval n)))
: (S = putnam_2007_a4_solution) := by
Problem: putnam_2007_a5
Category: abstract_algebra

Suppose that a finite group has exactly $n$ elements of order $p$, where $p$ is a prime. Prove that either $n = 0$ or $p$ divides $n+1$.


Lean 4 formalization:
import Mathlib

open Set Nat

theorem putnam_2007_a5
(G : Type*) [Group G] [Fintype G]
(p n : ℕ)
(hp : Nat.Prime p)
(hn : n = {g : G | orderOf g = p}.encard)
: n = 0 ∨ p ∣ (n + 1) := by
Problem: putnam_2007_b1
Category: algebra

Let $f$ be a nonconstant polynomial with positive integer coefficients. Prove that if $n$ is a positive integer, then $f(n)$ divides $f(f(n) + 1)$ if and only if $n = 1$


Lean 4 formalization:
import Mathlib

open Set Nat

theorem putnam_2007_b1
(f : Polynomial ℤ)
(hf : ∀ n : ℕ, f.coeff n ≥ 0)
(hfnconst : ∃ n : ℕ, n > 0 ∧ f.coeff n > 0)
(n : ℤ)
(hn : n > 0)
: f.eval n ∣ f.eval (f.eval n + 1) ↔ n = 1 := by
Problem: putnam_2007_b2
Category: analysis

Suppose that $f: [0,1] \to \mathbb{R}$ has a continuous derivative and that $\int_0^1 f(x)\,dx = 0$. Prove that for every $\alpha \in (0,1)$,
\[
\left| \int_0^\alpha f(x)\,dx \right| \leq \frac{1}{8} \max_{0 \leq x
\leq 1} |f'(x)|.
\]


Lean 4 formalization:
import Mathlib

open Set Nat Function

theorem putnam_2007_b2
(f : ℝ → ℝ)
(hf : ContDiffOn ℝ 1 f (Icc 0 1))
(hfint : ∫ x in (0)..1, f x = 0)
(max : ℝ)
(heqmax : ∃ x ∈ Icc (0 : ℝ) 1, |deriv f x| = max)
(hmaxub : ∀ x ∈ Icc (0 : ℝ) 1, |deriv f x| ≤ max)
: (∀ α ∈ (Ioo (0 : ℝ) 1), |∫ x in (0)..α, f x| ≤ (1 / 8) * max) := by
Problem: putnam_2007_b3
Category: analysis

Let $x_0 = 1$ and for $n \geq 0$, let $x_{n+1} = 3x_n + \lfloor x_n \sqrt{5} \rfloor$. In particular, $x_1 = 5$, $x_2 = 26$, $x_3 = 136$, $x_4 = 712$. Find a closed-form expression for $x_{2007}$. ($\lfloor a \rfloor$ means the largest integer $\leq a$.)

Solution: Prove that $x_{2007} = \frac{2^{2006}}{\sqrt{5}}(\alpha^{3997}-\alpha^{-3997})$, where $\alpha = \frac{1+\sqrt{5}}{2}$.

Lean 4 formalization:
import Mathlib

open Set Nat Function

noncomputable abbrev putnam_2007_b3_solution : ℝ := sorry
theorem putnam_2007_b3
(x : ℕ → ℝ)
(hx0 : x 0 = 1)
(hx : ∀ n : ℕ, x (n + 1) = 3 * (x n) + ⌊(x n) * Real.sqrt 5⌋)
: (x 2007 = putnam_2007_b3_solution) := by
Problem: putnam_2007_b4
Category: algebra

Let $n$ be a positive integer. Find the number of pairs $P, Q$ of polynomials with real coefficients such that
\[
(P(X))^2 + (Q(X))^2 = X^{2n} + 1
\]
and $\deg P > \deg Q$.

Solution: Show that the number of pairs is $2^{n+1}$.

Lean 4 formalization:
import Mathlib

open Set Nat Function

abbrev putnam_2007_b4_solution : ℕ → ℕ := sorry
theorem putnam_2007_b4
(n : ℕ) (npos : n > 0) :
({(P, Q) : (Polynomial ℝ) × (Polynomial ℝ) | P ^ 2 + Q ^ 2 = Polynomial.X ^ (2 * n) + 1 ∧ P.degree > Q.degree}.ncard = putnam_2007_b4_solution n) := by
Problem: putnam_2007_b5
Category: algebra

Let $k$ be a positive integer. Prove that there exist polynomials $P_0(n), P_1(n), \dots, P_{k-1}(n)$ (which may depend on $k$) such that for any integer $n$,
\[
\left\lfloor \frac{n}{k} \right\rfloor^k = P_0(n) + P_1(n) \left\lfloor
\frac{n}{k} \right\rfloor + \cdots + P_{k-1}(n) \left\lfloor \frac{n}{k}
\right\rfloor^{k-1}.
\]
($\lfloor a \rfloor$ means the largest integer $\leq a$.)


Lean 4 formalization:
import Mathlib

open Set Nat Function

theorem putnam_2007_b5
(k : ℕ) (kpos : k > 0) :
(∃ P : Finset.range k → Polynomial ℝ, ∀ n : ℤ, ⌊(n : ℝ) / k⌋ ^ k = ∑ i : Finset.range k, (P i).eval (n : ℝ) * ⌊(n : ℝ) / k⌋ ^ (i : ℕ)) := by
Problem: putnam_2007_b6
Category: combinatorics, analysis

For each positive integer $n$, let $f(n)$ be the number of ways to make $n!$ cents using an unordered collection of coins, each worth $k!$ cents for some $k$, $1 \leq k \leq n$. Prove that for some constant $C$, independent of $n$,
\[
n^{n^2/2 - Cn} e^{-n^2/4} \leq f(n) \leq n^{n^2/2 + Cn}e^{-n^2/4}.
\]


Lean 4 formalization:
import Mathlib

open Set Nat Function

theorem putnam_2007_b6
(f : ℕ → ℕ)
(hf : f = fun n ↦ {M : Multiset ℕ | M.sum = (n)! ∧ ∀ m ∈ M, ∃ k ∈ Icc 1 n, m = (k)!}.ncard)
: (∃ C : ℝ, ∀ n : ℕ, n ≥ 2 → n ^ (n ^ 2 / 2 - C * n) * Real.exp (-(n ^ 2) / 4) ≤ f n ∧ f n ≤ n ^ (n ^ 2 / 2 + C * n) * Real.exp (-(n ^ 2) / 4)) := by
Problem: putnam_2008_a1
Category: algebra

Let $f:\mathbb{R}^2 \to \mathbb{R}$ be a function such that $f(x,y)+f(y,z)+f(z,x)=0$ for all real numbers $x$, $y$, and $z$. Prove that there exists a function $g:\mathbb{R} \to \mathbb{R}$ such that $f(x,y)=g(x)-g(y)$ for all real numbers $x$ and $y$.


Lean 4 formalization:
import Mathlib

theorem putnam_2008_a1
(f : ℝ → ℝ → ℝ)
(hf : ∀ x y z : ℝ, f x y + f y z + f z x = 0)
: ∃ g : ℝ → ℝ, ∀ x y : ℝ, f x y = g x - g y := by
Problem: putnam_2008_a3
Category: number_theory

Start with a finite sequence $a_1, a_2, \dots, a_n$ of positive integers. If possible, choose two indices $j < k$ such that $a_j$ does not divide $a_k$, and replace $a_j$ and $a_k$ by $\mathrm{gcd}(a_j, a_k)$ and $\mathrm{lcm}(a_j, a_k)$, respectively. Prove that if this process is repeated, it must eventually stop and the final sequence does not depend on the choices made.


Lean 4 formalization:
import Mathlib

theorem putnam_2008_a3
      (n : ℕ) (npos : n > 0)
      (a : Fin n → ℕ)
      (apos : ∀ i : Fin n, a i > 0)
      (cont : (Fin n → ℕ) → Prop)
      (hcont : ∀ s, cont s ↔ ∃ j k : Fin n, j < k ∧ ¬(s j ∣ s k))
      (init trans : (ℕ → Fin n → ℕ) → Prop)
      (hinit : ∀ P, init P ↔ P 0 = a)
      (htrans : ∀ P, trans P ↔ ∀ t : ℕ, cont (P t) →
            ∃ j k : Fin n, j < k ∧ ¬(P t j ∣ P t k) ∧ P (t + 1) j = Nat.gcd (P t j) (P t k) ∧ P (t + 1) k = Nat.lcm (P t j) (P t k) ∧
            ∀ i : Fin n, i ≠ j → i ≠ k → P (t + 1) i = P t i) :
      (∃ f, ∀ P, init P → trans P → ∃ t : ℕ, ¬cont (P t) ∧ P t = f) := by
Problem: putnam_2008_a4
Category: algebra

Define $f : \mathbb{R} \to \mathbb{R} by $f(x) = x$ if $x \leq e$ and $f(x) = x * f(\ln(x))$ if $x > e$. Does $\sum_{n=1}^{\infty} 1/(f(n))$ converge?

Solution: Show that the sum does not converge.

Lean 4 formalization:
import Mathlib

open Filter Topology

abbrev putnam_2008_a4_solution : Prop := sorry
theorem putnam_2008_a4
(f : ℝ → ℝ)
(hf : f = fun x => if x ≤ Real.exp 1 then x else x * (f (Real.log x)))
: (∃ r : ℝ, Tendsto (fun N : ℕ => ∑ n ∈ Finset.range N, 1/(f (n + 1))) atTop (𝓝 r)) ↔ putnam_2008_a4_solution := by
Problem: putnam_2008_a5
Category: algebra, geometry

Let $n \geq 3$ be an integer. Let $f(x)$ and $g(x)$ be polynomials with real coefficients such that the points $(f(1), g(1)), (f(2), g(2)), \dots, (f(n), g(n))$ in $\mathbb{R}^2$ are the vertices of a regular $n$-gon in counterclockwise order. Prove that at least one of $f(x)$ and $g(x)$ has degree greater than or equal to $n-1$.


Lean 4 formalization:
import Mathlib

open Filter Topology Set

theorem putnam_2008_a5
(n : ℕ)
(nge3 : n ≥ 3)
(f g : Polynomial ℝ)
(hfg : ∃ O z : ℂ, z ≠ 0 ∧ ∀ k : ℕ, k ∈ Icc 1 n → (f.eval (k : ℝ)) + Complex.I * (g.eval (k : ℝ)) = O + z * Complex.exp (Complex.I * 2 * Real.pi * k / n))
: (f.natDegree ≥ n - 1 ∨ g.natDegree ≥ n - 1) := by
Problem: putnam_2008_a6
Category: abstract_algebra

Prove that there exists a constant $c>0$ such that in every nontrivial finite group $G$ there exists a sequence of length at most $c \log |G|$ with the property that each element of $G$ equals the product of some subsequence. (The elements of $G$ in the sequence are not required to be distinct. A \emph{subsequence} of a sequence is obtained by selecting some of the terms, not necessarily consecutive, without reordering them; for example, $4, 4, 2$ is a subsequence of $2, 4, 6, 4, 2$, but $2, 2, 4$ is not.)


Lean 4 formalization:
import Mathlib

open Filter Topology Set

theorem putnam_2008_a6
: ∃ c : ℝ, c > 0 ∧ ∀ G [Group G] (fing : Fintype G), fing.card > 1 → ∃ s : List G, s.length ≤ c * Real.log (fing.card : ℝ) ∧ ∀ g : G, ∃ t : List G, t.Sublist s ∧ t.prod = g := by
Problem: putnam_2008_b1
Category: geometry, number_theory

What is the maximum number of rational points that can lie on a circle in $\mathbb{R}^2$ whose center is not a rational point? (A \emph{rational point} is a point both of whose coordinates are rational numbers.)

Solution: Show that the maximum number is $2$.

Lean 4 formalization:
import Mathlib

open Filter Topology Set

abbrev putnam_2008_b1_solution : ℕ := sorry
def is_rational_point (p : Fin 2 → ℝ) : Prop := ∃ (a b : ℚ), a = p 0 ∧ b = p 1
def real_circle (c : EuclideanSpace ℝ (Fin 2)) (r : ℝ) : Set (EuclideanSpace ℝ (Fin 2)) := {p | dist p c = r}
theorem putnam_2008_b1 :
  IsGreatest {n : ℕ | ∃ (c : EuclideanSpace ℝ (Fin 2)) (r : ℝ), ¬ is_rational_point c ∧ (Set.ncard {p : EuclideanSpace ℝ (Fin 2) | p ∈ real_circle c r ∧ is_rational_point p} = n)} putnam_2008_b1_solution := by
Problem: putnam_2008_b2
Category: analysis

Let $F_0(x)=\ln x$. For $n \geq 0$ and $x>0$, let $F_{n+1}(x)=\int_0^x F_n(t)\,dt$. Evaluate $\lim_{n \to \infty} \frac{n!F_n(1)}{\ln n}$.

Solution: Show that the desired limit is $-1$.

Lean 4 formalization:
import Mathlib

open Filter Topology Set Nat

abbrev putnam_2008_b2_solution : ℝ := sorry
theorem putnam_2008_b2
(F : ℕ → ℝ → ℝ)
(hF0 : ∀ x : ℝ, F 0 x = Real.log x)
(hFn : ∀ n : ℕ, ∀ x > 0, F (n + 1) x = ∫ t in Set.Ioo 0 x, F n t)
: Tendsto (fun n : ℕ => ((n)! * F n 1) / Real.log n) atTop (𝓝 putnam_2008_b2_solution) := by
Problem: putnam_2008_b3
Category: geometry

What is the largest possible radius of a circle contained in a $4$-dimensional hypercube of side length $1$?

Solution: Show that the answer is $\frac{\sqrt 2}{2}$.

Lean 4 formalization:
import Mathlib

open Metric Filter Topology Set Nat

noncomputable abbrev putnam_2008_b3_solution : ℝ := sorry
theorem putnam_2008_b3
    (H : Set (EuclideanSpace ℝ (Fin 4)))
    (H_def : H = {P : EuclideanSpace ℝ (Fin 4) | ∀ i : Fin 4, |P i| ≤ 1 / 2})
    (contains : ℝ → Prop)
    (contains_def : ∀ r, contains r ↔
      ∃ᵉ (A : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 4))) (C ∈ A),
        Module.finrank ℝ A.direction = 2 ∧
        sphere C r ∩ A ⊆ H) :
    IsGreatest contains putnam_2008_b3_solution := by
Problem: putnam_2008_b4
Category: algebra, number_theory

Let $p$ be a prime number. Let $h(x)$ be a polynomial with integer coefficients such that $h(0), h(1), \dots, h(p^2-1)$ are distinct modulo $p^2$. Show that $h(0), h(1), \dots, h(p^3-1)$ are distinct modulo $p^3$.


Lean 4 formalization:
import Mathlib

open Filter Topology Set Nat

theorem putnam_2008_b4
(p : ℕ)
(hp : Nat.Prime p)
(h : Polynomial ℤ)
(hh : ∀ i j : Finset.range (p ^ 2), h.eval i ≡ h.eval j [ZMOD p ^ 2] → i = j)
: (∀ i j : Finset.range (p ^ 3), h.eval i ≡ h.eval j [ZMOD p ^ 3] → i = j) := by
Problem: putnam_2008_b5
Category: analysis

Find all continuously differentiable functions f : \mathbb{R} \to \mathbb{R} such that for every rational number $q$, the number $f(q)$ is rational and has the same denominator as $q$.

Solution: Show that the solution is the set of all functions of the form n + x, n - x where n is any integer.

Lean 4 formalization:
import Mathlib

open Filter Topology Set Nat

abbrev putnam_2008_b5_solution : Set (ℝ → ℝ) := sorry
theorem putnam_2008_b5
(fqsat : (ℝ → ℝ) → ℚ → Prop)
(hfqsat : ∀ f q, fqsat f q ↔ ContDiff ℝ 1 f ∧ (∃ p : ℚ, p = f q ∧ p.den = q.den))
: ∀ f : (ℝ → ℝ), (∀ q : ℚ, fqsat f q) ↔ f ∈ putnam_2008_b5_solution := by
Problem: putnam_2008_b6
Category: number_theory

Let $n$ and $k$ be positive integers. Say that a permutation $\sigma$ of $\{1,2,\dots,n\} is $k-limited$ if \|\sigma(i) - i\| \leq k$ for all $i$. Prove that the number of $k-limited$ permutations $\{1,2,\dots,n\}$ is odd if and only if $n \equiv 0$ or $1 (mod 2k+1)$.


Lean 4 formalization:
import Mathlib

open Filter Topology Set Nat

def klimited (k n : ℕ) (s : Equiv.Perm (Fin n)) := ∀ i, |((s i) : ℤ) - i| ≤ k
theorem putnam_2008_b6
(n k : ℕ)
(hnk : n > 0 ∧ k > 0)
: Odd (Set.ncard {s : Equiv.Perm (Fin n) | klimited k n s}) ↔ (n ≡ 0 [MOD 2*k+1] ∨ n ≡ 1 [MOD 2*k+1]) := by
Problem: putnam_2009_a1
Category: geometry, algebra

Let $f$ be a real-valued function on the plane such that for every square $ABCD$ in the plane, $f(A)+f(B)+f(C)+f(D)=0$. Does it follow that $f(P)=0$ for all points $P$ in the plane?

Solution: Prove that $f$ is identically $0$.

Lean 4 formalization:
import Mathlib

open Topology MvPolynomial Filter

abbrev putnam_2009_a1_solution : Prop := sorry
theorem putnam_2009_a1
: ((∀ f : (ℝ × ℝ) → ℝ, (∀ O v : ℝ × ℝ, v ≠ (0, 0) → f (O.1, O.2) + f (O.1 + v.1, O.2 + v.2) + f (O.1 + v.1 - v.2, O.2 + v.2 + v.1) + f (O.1 - v.2, O.2 + v.1) = 0) → ∀ P : ℝ × ℝ, f P = 0) ↔ putnam_2009_a1_solution) := by
Problem: putnam_2009_a2
Category: analysis

Functions $f,g,h$ are differentiable on some open interval around $0$
and satisfy the equations and initial conditions
\begin{gather*}
f' = 2f^2gh+\frac{1}{gh},\quad f(0)=1, \\
g'=fg^2h+\frac{4}{fh}, \quad g(0)=1, \\
h'=3fgh^2+\frac{1}{fg}, \quad h(0)=1.
\end{gather*}
Find an explicit formula for $f(x)$, valid in some open interval around $0$.

Solution: Prove that the formula is
\[
f(x) = 2^{-1/12} \left(\frac{\sin(6x+\pi/4)}{\cos^2(6x+\pi/4)}\right)^{1/6}.
\]

Lean 4 formalization:
import Mathlib

open Topology MvPolynomial Filter Set

noncomputable abbrev putnam_2009_a2_solution : ℝ → ℝ := sorry
theorem putnam_2009_a2
(f g h : ℝ → ℝ)
(a b : ℝ)
(hab : 0 ∈ Ioo a b)
(hdiff : DifferentiableOn ℝ f (Ioo a b) ∧ DifferentiableOn ℝ g (Ioo a b) ∧ DifferentiableOn ℝ h (Ioo a b))
(hf : (∀ x ∈ Ioo a b, deriv f x = 2 * (f x)^2 * (g x) * (h x) + 1 / ((g x) * (h x))) ∧ f 0 = 1)
(hg : (∀ x ∈ Ioo a b, deriv g x = (f x) * (g x)^2 * (h x) + 4 / ((f x) * (h x))) ∧ g 0 = 1)
(hh : (∀ x ∈ Ioo a b, deriv h x = 3 * (f x) * (g x) * (h x)^2 + 1 / ((f x) * (g x))) ∧ h 0 = 1)
: (∃ c d : ℝ, 0 ∈ Ioo c d ∧ ∀ x ∈ Ioo c d, f x = putnam_2009_a2_solution x) := by
Problem: putnam_2009_a3
Category: linear_algebra, analysis

Let $d_n$ be the determinant of the $n \times n$ matrix whose entries, from left to right and then from top to bottom, are $\cos 1, \cos 2, \dots, \cos n^2$. (For example,\[ d_3 = \left|\begin{matrix} \cos 1 & \cos 2 & \cos 3 \\ \cos 4 & \cos 5 & \cos 6 \\  \cos 7 & \cos 8 & \cos 9 \end{matrix} \right|. \]The argument of $\cos$ is always in radians, not degrees.) Evaluate $\lim_{n\to\infty} d_n$.

Solution: Show that the limit is 0.

Lean 4 formalization:
import Mathlib

open Topology MvPolynomial Filter Set

abbrev putnam_2009_a3_solution : ℝ := sorry
theorem putnam_2009_a3
(cos_matrix : (n : ℕ) → Matrix (Fin n) (Fin n) ℝ)
(hM : ∀ n : ℕ, ∀ i j : Fin n, (cos_matrix n) i j = Real.cos (1 + n * i + j))
: Tendsto (fun n => (cos_matrix n).det) atTop (𝓝 putnam_2009_a3_solution) := by
Problem: putnam_2009_a4
Category: number_theory

Let $S$ be a set of rational numbers such that
\begin{enumerate}
\item[(a)] $0 \in S$;
\item[(b)] If $x \in S$ then $x+1\in S$ and $x-1\in S$; and
\item[(c)] If $x\in S$ and $x\not\in\{0,1\}$, then $\frac{1}{x(x-1)}\in S$.
\end{enumerate}
Must $S$ contain all rational numbers?

Solution: Prove that $S$ need not contain all rationals.

Lean 4 formalization:
import Mathlib

open Topology MvPolynomial Filter Set

abbrev putnam_2009_a4_solution : Prop := sorry
theorem putnam_2009_a4
: ((∀ S : Set ℚ, 0 ∈ S → (∀ x ∈ S, x + 1 ∈ S ∧ x - 1 ∈ S) → (∀ x ∈ S, x ∉ ({0, 1} : Set ℚ) → 1 / (x * (x - 1)) ∈ S) → ∀ r : ℚ, r ∈ S) ↔ putnam_2009_a4_solution) := by