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

Let $a_1,a_2,\dots,a_n$ and $b_1,b_2,\dots,b_n$ be nonnegative real numbers. Show that $(a_1a_2 \cdots a_n)^{1/n}+(b_1b_2 \cdots b_n)^{1/n} \leq [(a_1+b_1)(a_2+b_2) \cdots (a_n+b_n)]^{1/n}$.


Lean 4 formalization:
import Mathlib

open MvPolynomial

theorem putnam_2003_a2
    (n : ℕ)
    (hn : 0 < n)
    (a b : Fin n → ℝ)
    (abnneg : ∀ i, a i ≥ 0 ∧ b i ≥ 0) :
    (∏ i, a i) ^ ((1 : ℝ) / n) +
    (∏ i, b i) ^ ((1 : ℝ) / n) ≤
    (∏ i, (a i + b i)) ^ ((1 : ℝ) / n) := by
Problem: putnam_2003_a3
Category: analysis

Find the minimum value of $|\sin x+\cos x+\tan x+\cot x+\sec x+\csc x|$ for real numbers $x$.

Solution: Show that the minimum is $2\sqrt{2}-1$.

Lean 4 formalization:
import Mathlib

open Set

noncomputable abbrev putnam_2003_a3_solution : ℝ := sorry
theorem putnam_2003_a3
    (f : ℝ → ℝ)
    (hf : ∀ x : ℝ, f x = |Real.sin x + Real.cos x + Real.tan x + 1 / Real.tan x + 1 / Real.cos x + 1 / Real.sin x|) :
    IsLeast (Set.range f) putnam_2003_a3_solution := by
Problem: putnam_2003_a4
Category: algebra

Suppose that $a,b,c,A,B,C$ are real numbers, $a \ne 0$ and $A \ne 0$, such that $|ax^2+bx+c| \leq |Ax^2+Bx+C|$ for all real numbers $x$. Show that $|b^2-4ac| \leq |B^2-4AC|$.


Lean 4 formalization:
import Mathlib

open MvPolynomial

theorem putnam_2003_a4
(a b c A B C : ℝ)
(aAne0 : a ≠ 0 ∧ A ≠ 0)
(hle : ∀ x : ℝ, |a * x ^ 2 + b * x + c| ≤ |A * x ^ 2 + B * x + C|)
: |b ^ 2 - 4 * a * c| ≤ |B ^ 2 - 4 * A * C| := by
Problem: putnam_2003_a5
Category: combinatorics

A Dyck $n$-path is a lattice path of $n$ upsteps $(1,1)$ and $n$ downsteps $(1,-1)$ that starts at the origin $O$ and never dips below the $x$-axis. A return is a maximal sequence of contiguous downsteps that terminates on the $x$-axis. Show that there is a one-to-one correspondence between the Dyck $n$-paths with no return of even length and the Dyck $(n-1)$-paths.


Lean 4 formalization:
import Mathlib

open MvPolynomial Set

theorem putnam_2003_a5
(n : ℕ) (npos : n > 0)
(dyckpath : (m : ℕ) → Set ((Fin (2 * m)) → ℤ))
(hdyckpath : dyckpath = fun m ↦ {p |
      range p ⊆ {-1, 1} ∧ ∑ k, p k = 0 ∧ ∀ j, ∑ k, ite (k ≤ j) (p k) 0 ≥ 0})
(noevenreturn : (m : ℕ) → Set ((Fin (2 * m)) → ℤ))
(hnoevenreturn : noevenreturn = fun m ↦ {p |
      ¬∃ i j, i < j ∧ p i = 1 ∧ (∀ k ∈ Ioc i j, p k = -1) ∧
            Even (j.1 - i.1) ∧ ∑ k, ite (k ≤ j) (p k) 0 = 0})
      : ∃ f : ((Fin (2 * n)) → ℤ) → (Fin (2 * (n - 1)) → ℤ),
            ∀ y ∈ dyckpath (n - 1), ∃! x, x ∈ dyckpath n ∩ noevenreturn n ∧ f x = y := by
Problem: putnam_2003_a6
Category: algebra

For a set $S$ of nonnegative integers, let $r_S(n)$ denote the number of ordered pairs $(s_1,s_2)$ such that $s_1 \in S$, $s_2 \in S$, $s_1 \ne s_2$, and $s_1+s_2=n$. Is it possible to partition the nonnegative integers into two sets $A$ and $B$ in such a way that $r_A(n)=r_B(n)$ for all $n$?

Solution: Show that such a partition is possible.

Lean 4 formalization:
import Mathlib

open MvPolynomial Set

abbrev putnam_2003_a6_solution : Prop := sorry
theorem putnam_2003_a6
(r : Set ℕ → ℕ → ℕ)
(hr : ∀ S n, r S n = ∑' s1 : S, ∑' s2 : S, if (s1 ≠ s2 ∧ s1 + s2 = n) then 1 else 0)
: (∃ A B : Set ℕ, A ∪ B = (Set.univ : Set ℕ) ∧ A ∩ B = ∅ ∧ (∀ n : ℕ, r A n = r B n)) ↔ putnam_2003_a6_solution := by
Problem: putnam_2003_b1
Category: linear_algebra, algebra

Do there exist polynomials $a(x), b(x), c(y), d(y)$ such that \[ 1 + xy + x^2y^2 = a(x)c(y) + b(x)d(y)\] holds identically?

Solution: Show that no such polynomials exist.

Lean 4 formalization:
import Mathlib

open MvPolynomial Set

abbrev putnam_2003_b1_solution : Prop := sorry
theorem putnam_2003_b1
: (∃ a b c d : Polynomial ℝ, (∀ x y : ℝ, 1 + x * y + x ^ 2 * y ^ 2 = a.eval x * c.eval y + b.eval x * d.eval y)) ↔ putnam_2003_b1_solution := by
Problem: putnam_2003_b2
Category: algebra

Let $n$ be a positive integer. Starting with the sequence $$1, \frac{1}{2}, \frac{1}{3}, \dots, \frac{1}{n},$$ form a new sequence of $n-1$ entries $$\frac{3}{4}, \frac{5}{12}, \dots, \frac{2n-1}{2n(n-1)}$$ by taking the averages of two consecutive entries in the first sequence. Repeat the averaging of neighbors on the second sequence to obtain a third sequence of $n-2$ entries, and continue until the final sequence produced consists of a single number $x_n$. Show that $x_n < 2/n$.


Lean 4 formalization:
import Mathlib

open MvPolynomial Set

theorem putnam_2003_b2
  (n : ℕ)
  (hn : n > 0)
  (seq : ℕ → ℕ → ℚ)
  (hinit : ∀ j ∈ Icc 1 n, seq 0 j = 1 / j)
  (havg : ∀ᵉ (k ∈ Icc 1 (n - 1)) (j ∈ Icc 1 (n - k)),
    seq k j = (seq (k - 1) j + seq (k - 1) (j + 1)) / 2) :
  (seq (n - 1) 1 < 2 / n) := by
Problem: putnam_2003_b3
Category: number_theory

Show that for each positive integer $n$, $n!=\prod_{i=1}^n \text{lcm}\{1,2,\dots,\lfloor n/i \rfloor\}$. (Here lcm denotes the least common multiple, and $\lfloor x \rfloor$ denotes the greatest integer $\leq x$.)


Lean 4 formalization:
import Mathlib

open MvPolynomial Set Nat

theorem putnam_2003_b3 (n : ℕ) :
    n ! = ∏ i ∈ Finset.Icc 1 n, ((List.range ⌊n / i⌋₊).map succ).foldl Nat.lcm 1 := by
Problem: putnam_2003_b4
Category: number_theory, algebra

Let $f(z)=az^4+bz^3+cz^2+dz+e=a(z-r_1)(z-r_2)(z-r_3)(z-r_4)$ where $a,b,c,d,e$ are integers, $a \neq 0$. Show that if $r_1+r_2$ is a rational number and $r_1+r_2 \neq r_3+r_4$, then $r_1r_2$ is a rational number.


Lean 4 formalization:
import Mathlib

open MvPolynomial Set Nat

theorem putnam_2003_b4
  (f : ℝ → ℝ)
  (a b c d e : ℤ)
  (r1 r2 r3 r4 : ℝ)
  (ane0 : a ≠ 0)
  (hf1 : ∀ z, f z = a * z ^ 4 + b * z ^ 3 + c * z ^ 2 + d * z + e)
  (hf2 : ∀ z, f z = a * (z - r1) * (z - r2) * (z - r3) * (z - r4)) :
  (¬Irrational (r1 + r2) ∧ r1 + r2 ≠ r3 + r4) → ¬Irrational (r1 * r2) := by
Problem: putnam_2003_b5
Category: geometry

Let $A,B$, and $C$ be equidistant points on the circumference of a circle of unit radius centered at $O$, and let $P$ be any point in the circle's interior. Let $a, b, c$ be the distance from $P$ to $A, B, C$, respectively. Show that there is a triangle with side lengths $a, b, c$, and that the area of this triangle depends only on the distance from $P$ to $O$.


Lean 4 formalization:
import Mathlib

open MvPolynomial Set Nat

theorem putnam_2003_b5
(A B C : EuclideanSpace ℝ (Fin 2))
(hABC : dist 0 A = 1 ∧ dist 0 B = 1 ∧ dist 0 C = 1 ∧ dist A B = dist A C ∧ dist A B = dist B C ∧ dist A B ≠ 0)
: (∃ f : ℝ → ℝ, ∀ P : EuclideanSpace ℝ (Fin 2), dist 0 P < 1 → ∃ X Y Z : EuclideanSpace ℝ (Fin 2),
      dist X Y = dist P A ∧ dist Y Z = dist P B ∧ dist X Z = dist P C ∧
      (MeasureTheory.volume (convexHull ℝ {X, Y, Z})).toReal = f (dist 0 P)) := by
Problem: putnam_2003_b6
Category: analysis

Let  $f(x)$  be  a continuous real-valued function defined on the interval $[0,1]$. Show that \[ \int_0^1 \int_0^1 | f(x) + f(y) |\,dx\,dy \geq \int_0^1 |f(x)|\,dx. \]


Lean 4 formalization:
import Mathlib

open MvPolynomial Set Nat

theorem putnam_2003_b6
(f : ℝ → ℝ)
(hf : Continuous f)
: (∫ x in (0 : ℝ)..1, (∫ y in (0 : ℝ)..1, |f x + f y|)) ≥ (∫ x in (0 : ℝ)..1, |f x|) := by
Problem: putnam_2004_a1
Category: probability

Basketball star Shanille O'Keal's team statistician keeps track of the number, $S(N)$, of successful free throws she has made in her first $N$ attempts of the season. Early in the season, $S(N)$ was less than $80\%$ of $N$, but by the end of the season, $S(N)$ was more than $80\%$ of $N$. Was there necessarily a moment in between when $S(N)$ was exactly $80\%$ of $N$?

Solution: Show that the answer is yes.

Lean 4 formalization:
import Mathlib

open Nat Topology Filter

abbrev putnam_2004_a1_solution : Prop := sorry
theorem putnam_2004_a1
  (S : (ℕ → Fin 2) → ℕ → ℝ)
  (hS : ∀ attempts, ∀ N ≥ 1, S attempts N = (∑ i : Fin N, (attempts i).1) / N) :
  (∀ attempts a b,
    (1 ≤ a ∧ a < b ∧ S attempts a < 0.8 ∧ S attempts b > 0.8) →
      (∃ c : ℕ, a < c ∧ c < b ∧ S attempts c = 0.8))
  ↔ putnam_2004_a1_solution := by
Problem: putnam_2004_a3
Category: linear_algebra

Define a sequence $\{u_n\}_{n=0}^\infty$ by $u_0=u_1=u_2=1$, and thereafter by the condition that $\det \begin{pmatrix}
u_n & u_{n+1} \\
u_{n+2} & u_{n+3}
\end{pmatrix} = n!$ for all $n \geq 0$. Show that $u_n$ is an integer for all $n$. (By convention, $0!=1$.)


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_2004_a3
(u : ℕ → ℝ)
(hubase : u 0 = 1 ∧ u 1 = 1 ∧ u 2 = 1)
(hudet : ∀ n : ℕ, Matrix.det (fun i j : Fin 2 => u (n + i * 2 + j)) = (n)!)
: ∀ n : ℕ, ∃ m : ℤ, u n = m := by
Problem: putnam_2004_a4
Category: algebra

Show that for any positive integer $n$ there is an integer $N$ such that the product $x_1x_2 \cdots x_n$ can be expressed identically in the form $x_1x_2 \cdots x_n=\sum_{i=1}^Nc_i(a_{i1}x_1+a_{i2}x_2+\cdots+a_{in}x_n)^n$ where the $c_i$ are rational numbers and each $a_{ij}$ is one of the numbers $-1,0,1$.


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_2004_a4
  (n : ℕ) (npos : n > 0)
  (x : Fin n → ℝ)
  (avals : ℕ → (ℕ → Fin n → ℝ) → Prop)
  (havals : ∀ N a, avals N a ↔ ∀ (i : Fin N) (j : Fin n), (a i j = -1 ∨ a i j = 0 ∨ a i j = 1)) :
  ∃ (N : ℕ) (c : Fin N → ℚ) (a : ℕ → Fin n → ℝ),
    avals N a ∧
    (∏ i : Fin n, x i) = ∑ i : Fin N, c i * (∑ j : Fin n, a i j * x j) ^ n := by
Problem: putnam_2004_a5
Category: combinatorics

An $m \times n$ checkerboard is colored randomly: each square is independently assigned red or black with probability $1/2$. We say that two squares, $p$ and $q$, are in the same connected monochromatic region if there is a sequence of squares, all of the same color, starting at $p$ and ending at $q$, in which successive squares in the sequence share a common side. Show that the expected number of connected monochromatic regions is greater than $m n / 8$.


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_2004_a5
(m n : ℕ)
(mnpos : Inhabited (Fin m × Fin n))
(adj : (Fin m × Fin n) → (Fin m × Fin n) → Prop)
(connected : (Fin m × Fin n → Prop) → (Fin m × Fin n) → (Fin m × Fin n) → Prop)
(cmr : (Fin m × Fin n → Prop) → ℕ)
(hadj : adj = fun (⟨a, _⟩, ⟨b, _⟩) (⟨c, _⟩, ⟨d, _⟩) ↦ a = c ∧ Nat.dist b d = 1 ∨ b = d ∧ Nat.dist a c = 1)
(hconnected : connected = fun C P Q ↦ ∃ (S : List (Fin m × Fin n)) (hS : S ≠ []),
      S.head hS = P ∧ S.getLast hS = Q ∧ (∃ p : Prop, ∀ i ∈ Finset.range S.length, C S[i]! = p) ∧ (∀ i ∈ Finset.range (S.length - 1), adj S[i]! S[i+1]!))
(hcmr : cmr = fun C ↦ {R : Set (Fin m × Fin n) | ∃ P ∈ R, ∀ Q, Q ∈ R ↔ connected C P Q}.ncard)
: (∑ C : Fin m × Fin n → Prop, cmr C > 2 ^ (m * n) * (m * n / (8 : ℚ))) := by
Problem: putnam_2004_a6
Category: analysis

Suppose that $f(x,y)$ is a continuous real-valued function on the unit square $0 \leq x \leq 1,0 \leq y \leq 1$. Show that $\int_0^1 \left(\int_0^1 f(x,y)dx\right)^2dy+\int_0^1 \left(\int_0^1 f(x,y)dy\right)^2dx \leq \left(\int_0^1 \int_0^1 f(x,y)dx\,dy\right)^2+\int_0^1 \int_0^1 [f(x,y)]^2dx\,dy$.


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_2004_a6
(f : (Set.Icc (0 : ℝ) 1 × Set.Icc (0 : ℝ) 1) → ℝ)
(fcont : Continuous f)
: (∫ y : Set.Icc (0 : ℝ) 1, (∫ x : Set.Icc (0 : ℝ) 1, f (x, y)) ^ 2) + (∫ x : Set.Icc (0 : ℝ) 1, (∫ y : Set.Icc (0 : ℝ) 1, f (x, y)) ^ 2) ≤ (∫ y : Set.Icc (0 : ℝ) 1, (∫ x : Set.Icc (0 : ℝ) 1, f (x, y))) ^ 2 + (∫ y : Set.Icc (0 : ℝ) 1, (∫ x : Set.Icc (0 : ℝ) 1, (f (x, y)) ^ 2)) := by
Problem: putnam_2004_b1
Category: algebra

Let $P(x)=c_nx^n+c_{n-1}x^{n-1}+\cdots+c_0$ be a polynomial with integer coefficients. Suppose that $r$ is a rational number such that $P(r)=0$. Show that the $n$ numbers $c_nr,\,c_nr^2+c_{n-1}r,\,c_nr^3+c_{n-1}r^2+c_{n-2}r,\dots,\,c_nr^n+c_{n-1}r^{n-1}+\cdots+c_1r$ are integers.


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_2004_b1
(n : ℕ)
(P : Polynomial ℤ)
(r : ℚ)
(Pdeg : P.degree = n)
(Preq0 : Polynomial.aeval r P = 0)
: ∀ i ∈ Finset.range n, ∃ m : ℤ, m = ∑ j ∈ Finset.range (i + 1), (P.coeff (n - j) * r ^ (i + 1 - j)) := by
Problem: putnam_2004_b2
Category: algebra

Let $m$ and $n$ be positive integers. Show that $\frac{(m+n)!}{(m+n)^{m+n}}<\frac{m!}{m^m}\frac{n!}{n^n}$.


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_2004_b2
(m n : ℕ)
(mnpos : m > 0 ∧ n > 0)
: ((m + n)! / ((m + n) ^ (m + n) : ℚ)) < (((m)! / (m ^ m : ℚ)) * ((n)! / (n ^ n : ℚ))) := by
Problem: putnam_2004_b4
Category: geometry

Let $n$ be a positive integer, $n \ge 2$, and put $\theta = 2 \pi / n$. Define points $P_k = (k,0)$ in the $xy$-plane, for $k = 1, 2, \dots, n$. Let $R_k$ be the map that rotates the plane counterclockwise by the angle $\theta$ about the point $P_k$. Let $R$ denote the map obtained by applying, in order, $R_1$, then $R_2, \dots$, then $R_n$. For an arbitrary point $(x,y)$, find, and simplify, the coordinates of $R(x,y)$.

Solution: Show that $R(x, y) = (x + n, y)$.

Lean 4 formalization:
import Mathlib

open Nat Topology Filter

abbrev putnam_2004_b4_solution : ℕ → ℂ → ℂ := sorry
theorem putnam_2004_b4
(n : ℕ)
(nge2 : n ≥ 2)
(R Rk : ℕ → ℂ → ℂ)
(hR : R 0 = id ∧ ∀ k : ℕ, R (k + 1) = Rk (k + 1) ∘ R k)
(hRk : Rk = fun (k : ℕ) (Q : ℂ) ↦ k + Complex.exp (Complex.I * 2 * Real.pi / n) * (Q - k))
: (R n = putnam_2004_b4_solution n) := by
Problem: putnam_2004_b5
Category: analysis

Evaluate $\lim_{x \to 1^-} \prod_{n=0}^\infty \left(\frac{1+x^{n+1}}{1+x^n}\right)^{x^n}$.

Solution: Show that the desired limit is $2/e$.

Lean 4 formalization:
import Mathlib

open Nat Topology Filter

abbrev putnam_2004_b5_solution : ℝ := sorry
theorem putnam_2004_b5
    (xprod : ℝ → ℝ)
    (hxprod : ∀ x ∈ Set.Ioo 0 1,
      Tendsto (fun N ↦ ∏ n ∈ Finset.range N, ((1 + x ^ (n + 1)) / (1 + x ^ n)) ^ (x ^ n))
      atTop (𝓝 (xprod x))) :
    Tendsto xprod (𝓝[<] 1) (𝓝 putnam_2004_b5_solution) := by
Problem: putnam_2004_b6
Category: analysis

Let $\mathcal{A}$ be a non-empty set of positive integers, and let $N(x)$ denote the number of elements of $\mathcal{A}$ not exceeding $x$. Let $\mathcal{B}$ denote the set of positive integers $b$ that can be written in the form $b=a-a'$ with $a \in \mathcal{A}$ and $a' \in \mathcal{A}$. Let $b_1<b_2<\cdots$ be the members of $\mathcal{B}$, listed in increasing order. Show that if the sequence $b_{i+1}-b_i$ is unbounded, then $\lim_{x \to\infty} N(x)/x=0$.


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_2004_b6
  (A B : Set ℕ)
  (N : ℝ → ℕ)
  (b : ℕ → ℕ)
  (Anempty : A.Nonempty)
  (Apos : ∀ a ∈ A, a > 0)
  (hN : ∀ x : ℝ, N x = Set.encard {a : A | a ≤ x})
  (hB : B = {b' > 0 | ∃ a ∈ A, ∃ a' ∈ A, b' = a - a'})
  (hbB : Set.range b = B ∧ ∀ i : ℕ, b i < b (i + 1)) :
  (∀ r : ℕ, ∃ i : ℕ, (b (i + 1) - b i) ≥ r) → Tendsto (fun x => N x / x) atTop (𝓝 0) := by
Problem: putnam_2005_a1
Category: number_theory

Show that every positive integer is a sum of one or more numbers of the form $2^r 3^s$, where $r$ and $s$ are nonnegative integers and no summand divides another.


Lean 4 formalization:
import Mathlib

open Nat

theorem putnam_2005_a1
: ∀ n : ℤ, n > 0 → (∃ k : ℕ, ∃ a : Fin k → Fin 2 → ℕ, n = ∑ i : Fin k, 2^(a i 0)*3^(a i 1) ∧
(∀ i j : Fin k, i ≠ j → ¬(2^(a i 0)*3^(a i 1) ∣ 2^(a j 0)*3^(a j 1)))) := by
Problem: putnam_2005_a2
Category: combinatorics

Let $\mathbf{S} = \{(a,b) | a = 1, 2, \dots,n, b = 1,2,3\}$.
A \emph{rook tour} of $\mathbf{S}$ is a polygonal path made up of line segments connecting points $p_1, p_2, \dots, p_{3n}$ in sequence such that
\begin{enumerate}
\item[(i)] $p_i \in \mathbf{S}$,
\item[(ii)] $p_i$ and $p_{i+1}$ are a unit distance apart, for
$1 \leq i <3n$,
\item[(iii)] for each $p \in \mathbf{S}$ there is a unique $i$ such that
$p_i = p$.
\end{enumerate}
How many rook tours are there that begin at $(1,1)$
and end at $(n,1)$?

Solution: Show that the number of rook tours is $0$ if $n = 1$ and $2 ^ {n - 2}$ if $n \geq 2$.

Lean 4 formalization:
import Mathlib

open Nat Set

abbrev putnam_2005_a2_solution : ℕ → ℕ := sorry
theorem putnam_2005_a2
(n : ℕ)
(npos : n > 0)
(S : Set (ℤ × ℤ))
(unit : ℤ × ℤ → ℤ × ℤ → Prop)
(rooktour : (ℕ → ℤ × ℤ) → Prop)
(hS : S = prod (Icc 1 (n : ℤ)) (Icc 1 3))
(hunit : unit = fun (a, b) (c, d) ↦ a = c ∧ |d - b| = 1 ∨ b = d ∧ |c - a| = 1)
(hrooktour : rooktour = fun p ↦ (∀ P ∈ S, ∃! i, i ∈ Icc 1 (3 * n) ∧ p i = P) ∧ (∀ i ∈ Icc 1 (3 * n - 1), unit (p i) (p (i + 1))) ∧ p 0 = 0 ∧ ∀ i > 3 * n, p i = 0)
: ({p : ℕ → ℤ × ℤ | rooktour p ∧ p 1 = (1, 1) ∧ p (3 * n) = ((n : ℤ), 1)}.encard = putnam_2005_a2_solution n) := by
Problem: putnam_2005_a3
Category: analysis, algebra

Let $p(z)$ be a polynomial of degree $n$ all of whose zeros have absolute value $1$ in the complex plane. Put $g(z)=p(z)/z^{n/2}$. Show that all zeros of $g'(z)=0$ have absolute value $1$.


Lean 4 formalization:
import Mathlib

open Nat Set

theorem putnam_2005_a3
    (p : Polynomial ℂ)
    (n : ℕ)
    (hn : 0 < n)
    (g : ℂ → ℂ)
    (pdeg : p.degree = n)
    (pzeros : ∀ z : ℂ, p.eval z = 0 → ‖z‖ = 1)
    (hg : ∀ z : ℂ, g z = (p.eval z) / z ^ ((n : ℂ) / 2))
    (z : ℂ)
    (hz : z ≠ 0 ∧ DifferentiableAt ℂ g z ∧ deriv g z = 0) :
    ‖z‖ = 1 := by
Problem: putnam_2005_a4
Category: linear_algebra

Let $H$ be an $n \times n$ matrix all of whose entries are $\pm 1$ and whose rows are mutually orthogonal. Suppose $H$ has an $a \times b$ submatrix whose entries are all $1$. Show that $ab \leq n$.


Lean 4 formalization:
import Mathlib

open Nat Set

theorem putnam_2005_a4
(n : ℕ)
(H : Matrix (Fin n) (Fin n) ℝ)
(a b : ℕ)
(S : Matrix (Fin a) (Fin b) ℝ)
(npos : n ≥ 1)
(Hentries : ∀ i j : Fin n, H i j = 1 ∨ H i j = -1)
(Hortho : H.HasOrthogonalRows)
(hab : 1 ≤ a ∧ a ≤ n ∧ 1 ≤ b ∧ b ≤ n)
(Ssub : ∃ (rri : Fin a → Fin n) (cri : Fin b → Fin n), rri.Injective ∧ cri.Injective ∧ S = H.submatrix rri cri)
(Sentries : ∀ (i : Fin a) (j : Fin b), S i j = 1)
: a * b ≤ n := by
Problem: putnam_2005_a5
Category: analysis

Evaluate $\int_0^1 \frac{\ln(x+1)}{x^2+1}\,dx$.

Solution: Show that the solution is $\pi / 8 * \log 2$.

Lean 4 formalization:
import Mathlib

open Nat Set

noncomputable abbrev putnam_2005_a5_solution : ℝ := sorry
theorem putnam_2005_a5 :
  ∫ x in (0:ℝ)..1, (Real.log (x+1))/(x^2 + 1) = putnam_2005_a5_solution := by
Problem: putnam_2005_b1
Category: algebra

Find a nonzero polynomial $P(x,y)$ such that $P(\lfloor a \rfloor,\lfloor 2a \rfloor)=0$ for all real numbers $a$. (Note: $\lfloor \nu \rfloor$ is the greatest integer less than or equal to $\nu$.)

Solution: Show that $P(x,y)=(y-2x)(y-2x-1)$ works.

Lean 4 formalization:
import Mathlib

open Nat Set

noncomputable abbrev putnam_2005_b1_solution : MvPolynomial (Fin 2) ℝ := sorry
theorem putnam_2005_b1
: putnam_2005_b1_solution ≠ 0 ∧ ∀ a : ℝ, MvPolynomial.eval (fun n : Fin 2 => if (n = 0) then (Int.floor a : ℝ) else (Int.floor (2 * a))) putnam_2005_b1_solution = 0 := by
Problem: putnam_2005_b2
Category: algebra

Find all positive integers $n,k_1,\dots,k_n$ such that $k_1+\cdots+k_n=5n-4$ and $\frac{1}{k_1}+\cdots+\frac{1}{k_n}=1$.

Solution: Show that the solutions are $n=1$ and $k_1=1$, $n=3$ and $(k_1,k_2,k_3)$ is a permutation of $(2,3,6)$, and $n=4$ and $(k_1,k_2,k_3,k_4)=(4,4,4,4)$.

Lean 4 formalization:
import Mathlib

open Nat Set

abbrev putnam_2005_b2_solution : Set (ℕ × (ℕ → ℤ)) := sorry
theorem putnam_2005_b2
: {((n : ℕ), (k : ℕ → ℤ)) | (n > 0) ∧ (∀ i ∈ Finset.range n, k i > 0) ∧ (∑ i ∈ Finset.range n, k i = 5 * n - 4) ∧ (∑ i : Finset.range n, (1 : ℝ) / (k i) = 1)} = putnam_2005_b2_solution := by
Problem: putnam_2005_b3
Category: analysis

Find all differentiable functions $f:(0,\infty) \to (0,\infty)$ for which there is a positive real number $a$ such that $f'(\frac{a}{x})=\frac{x}{f(x)}$ for all $x>0$.

Solution: Show that the functions are precisely $f(x)=cx^d$ for $c,d>0$ arbitrary except that we must take $c=1$ in case $d=1$.

Lean 4 formalization:
import Mathlib

open Nat Set

abbrev putnam_2005_b3_solution : Set (ℝ → ℝ) := sorry
theorem putnam_2005_b3
    (f : ℝ → ℝ)
    (hf : ∀ x > 0, 0 < f x)
    (hf' : DifferentiableOn ℝ f (Ioi 0)) :
    (∃ a > 0, ∀ x > 0, deriv f (a / x) = x / f x) ↔ f ∈ putnam_2005_b3_solution := by
Problem: putnam_2005_b4
Category: algebra

For positive integers $m$ and $n$, let $f(m,n)$ denote the number of $n$-tuples $(x_1,x_2,\dots,x_n)$ of integers such that $|x_1|+|x_2|+\cdots+|x_n| \leq m$. Show that $f(m,n)=f(n,m)$.


Lean 4 formalization:
import Mathlib

open Nat Set

theorem putnam_2005_b4
(m n : ℤ)
(mnpos : m > 0 ∧ n > 0)
(f : ℤ → ℤ → ℕ)
(hf : ∀ m' > 0, ∀ n' > 0, f m' n' = Set.encard {x : Finset.Icc 1 n' → ℤ | ∑ i : Finset.Icc 1 n', |x i| ≤ m'})
: f m n = f n m := by
Problem: putnam_2005_b5
Category: algebra

Let $P(x_1,\dots,x_n)$ denote a polynomial with real coefficients in the variables $x_1, \dots, x_n$, and suppose that
\[
\left( \frac{\partial^2}{\partial x_1^2} + \cdots + \frac{\partial^2}{\partial x_n^2}\right) P(x_1, \dots,x_n) = 0 \quad \mbox{(identically)}
\]
and that
\[
x_1^2 + \cdots + x_n^2 \mbox{ divides } P(x_1, \dots, x_n).
\]
Show that $P=0$ identically.


Lean 4 formalization:
import Mathlib

open Nat Set

theorem putnam_2005_b5
(n : ℕ)
(npos : n > 0)
(P : MvPolynomial (Fin n) ℝ)
(hderiv : ∑ i : Fin n, (MvPolynomial.pderiv i)^[2] P = 0)
(hsumsq : ∑ i : Fin n, (MvPolynomial.X i) ^ 2 ∣ P)
: (P = 0) := by
Problem: putnam_2005_b6
Category: linear_algebra, algebra

Let $S_n$ denote the set of all permutations of the numbers $1,2,\dots,n$. For $\pi \in S_n$, let $\sigma(\pi)=1$ if $\pi$ is an even permutation and $\sigma(\pi)=-1$ if $\pi$ is an odd permutation. Also, let $\nu(\pi)$ denote the number of fixed points of $\pi$. Show that $\sum_{\pi \in S_n} \frac{\sigma(\pi)}{\nu(\pi)+1}=(-1)^{n+1}\frac{n}{n+1}$.


Lean 4 formalization:
import Mathlib

open Nat Set

theorem putnam_2005_b6
(n : ℕ)
(v : Equiv.Perm (Fin n) → ℕ)
(npos : n ≥ 1)
(hv : ∀ p : Equiv.Perm (Fin n), v p = Set.encard {i : Fin n | p i = i})
: (∑ p : Equiv.Perm (Fin n), (Equiv.Perm.signAux p : ℤ) / (v p + 1 : ℝ)) = (-1) ^ (n + 1) * (n / (n + 1 : ℝ)) := by
Problem: putnam_2006_a1
Category: geometry

Find the volume of the region of points $(x,y,z)$ such that
\[
(x^2 + y^2 + z^2 + 8)^2 \leq 36(x^2 + y^2).
\]

Solution: Show that the volume is $6\pi^2$.

Lean 4 formalization:
import Mathlib

noncomputable abbrev putnam_2006_a1_solution : ℝ := sorry
theorem putnam_2006_a1
: ((MeasureTheory.volume {(x, y, z) : ℝ × ℝ × ℝ | (x ^ 2 + y ^ 2 + z ^ 2 + 8) ^ 2 ≤ 36 * (x ^ 2 + y ^ 2)}).toReal = putnam_2006_a1_solution) := by
Problem: putnam_2006_a3
Category: algebra

Let $1, 2, 3, \dots, 2005, 2006, 2007, 2009, 2012, 2016, \dots$ be a sequence defined by $x_k = k$ for $k=1, 2, \dots, 2006$ and $x_{k+1} = x_k + x_{k-2005}$ for $k \geq 2006$. Show that the sequence has $2005$ consecutive terms each divisible by $2006$.


Lean 4 formalization:
import Mathlib

theorem putnam_2006_a3
(x : ℤ → ℤ)
(hxlo : ∀ k : ℤ, 0 ≤ k ∧ k ≤ 2006 → x k = k)
(hxhi : ∀ k : ℤ, k ≥ 2006 → x (k + 1) = x k + x (k - 2005))
: (∃ i : ℕ, i > 0 ∧ ∀ j : Finset.range 2005, 2006 ∣ x (i + j)) := by
Problem: putnam_2006_a4
Category: algebra

Let $S=\{1,2,\dots,n\}$ for some integer $n>1$. Say a permutation $\pi$ of $S$ has a \emph{local maximum} at $k \in S$ if
\begin{enumerate}
\item[(i)] $\pi(k)>\pi(k+1)$ for $k=1$;
\item[(ii)] $\pi(k-1)<\pi(k)$ and $\pi(k)>\pi(k+1)$ for $1<k<n$;
\item[(iii)] $\pi(k-1)<\pi(k)$ for $k=n$.
\end{enumerate}
(For example, if $n=5$ and $\pi$ takes values at $1,2,3,4,5$ of $2,1,4,5,3$, then $\pi$ has a local maximum of 2 at $k=1$, and a local maximum of 5 at $k=4$.) What is the average number of local maxima of a permutation of $S$, averaging over all permutations of $S$?

Solution: Show that the average number of local maxima is $\frac{n+1}{3}$.

Lean 4 formalization:
import Mathlib

noncomputable abbrev putnam_2006_a4_solution : ℕ → ℝ := sorry
theorem putnam_2006_a4
(n : ℕ)
(pnat : Equiv.Perm (Fin n) → (ℕ → ℕ))
(pcount : Equiv.Perm (Fin n) → ℕ)
(ngt1 : n > 1)
(hpnat : ∀ p : Equiv.Perm (Fin n), ∀ k : Fin n, (pnat p) k = p k)
(hpcount : ∀ p : Equiv.Perm (Fin n), pcount p = {k : Fin n | (k.1 = 0 ∨ (pnat p) (k - 1) < (pnat p) k) ∧ (k = n - 1 ∨ (pnat p) k > (pnat p) (k + 1))}.encard)
: (∑ p : Equiv.Perm (Fin n), pcount p) / {p : Equiv.Perm (Fin n) | true}.ncard = putnam_2006_a4_solution n := by