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

Find all polynomials of the form $\sum_{0}^{n} a_{i} x^{n-i}$ with $n \ge 1$ and $a_i = \pm 1$ for all $0 \le i \le n$ whose roots are all real.

Solution: The set of such polynomials is $$\{\pm (x - 1), \pm (x + 1), \pm (x^2 + x - 1), \pm (x^2 - x - 1), \pm (x^3 + x^2 - x - 1), \pm (x^3 - x^2 - x + 1)\}.$$

Lean 4 formalization:
import Mathlib

open Finset Polynomial

abbrev putnam_1968_a6_solution : Set ℂ[X] := sorry
theorem putnam_1968_a6
: {P : ℂ[X] | P.natDegree ≥ 1 ∧ (∀ k ∈ Set.Icc 0 P.natDegree, P.coeff k = 1 ∨ P.coeff k = -1) ∧
∀ z : ℂ, P.eval z = 0 → ∃ r : ℝ, r = z} = putnam_1968_a6_solution := by
Problem: putnam_1968_b1
Category: probability

The random variables $X, Y$ can each take a finite number of integer values. They are not necessarily independent. Express $\mathrm{prob}(\min(X, Y) = k)$ in terms of $p_1 = \mathrm{prob}(X = k)$, $p_2 = \mathrm{prob}(Y = k)$ and $p_3 = \mathrm{prob(max(X, Y) = k)$.

Solution: $\mathrm{prob}(\min(X, Y) = k) = p_1 + p_2 - p_3.$

Lean 4 formalization:
import Mathlib

open MeasureTheory
open scoped ProbabilityTheory

abbrev putnam_1968_b1_solution : ℝ → ℝ → ℝ → ℝ := sorry
theorem putnam_1968_b1
    {Ω : Type*}
    [MeasureSpace Ω]
    [IsProbabilityMeasure (ℙ : Measure Ω)]
    (X Y : Ω → ℤ)
    (hX : Measurable X)
    (hY : Measurable Y)
    (hX' : Set.Finite (X '' Set.univ))
    (hY' : Set.Finite (Y '' Set.univ))
    (k : ℤ) :
    (ℙ {ω : Ω | min (X ω) (Y ω) = k}).toReal =
      putnam_1968_b1_solution (ℙ (X⁻¹' {k})).toReal (ℙ (Y⁻¹' {k})).toReal
      (ℙ {ω : Ω | max (X ω) (Y ω) = k}).toReal := by
Problem: putnam_1968_b2
Category: abstract_algebra

Let $G$ be a finite group (with a multiplicative operation), and $A$ be a subset of $G$ that contains more than half of $G$'s elements. Prove that every element of $G$ can be expressed as the product of two elements of $A$.


Lean 4 formalization:
import Mathlib

open Finset Polynomial

theorem putnam_1968_b2
{G : Type*}
[Group G]
(hG : Finite G)
(A : Set G)
(hA : A.ncard > (Nat.card G : ℚ)/2)
: ∀ g : G, ∃ x ∈ A, ∃ y ∈ A, g = x * y := by
Problem: putnam_1968_b4
Category: analysis

Suppose that $f : \mathbb{R} \to \mathbb{R}$ is continuous on $(-\infty, \infty)$ and that $\int_{-\infty}^{\infty} f(x) dx$ exists. Prove that $$\int_{-\infty}^{\infty} f\left(x - \frac{1}{x}\right) dx = \int_{-\infty}^{\infty} f(x) dx.$$


Lean 4 formalization:
import Mathlib

open Finset Polynomial Topology Filter Metric

theorem putnam_1968_b4
(f : ℝ → ℝ)
(hf : Continuous f ∧ ∃ r : ℝ, Tendsto (fun y => ∫ x in ball 0 y, f x) atTop (𝓝 r))
: ∃ r : ℝ, Tendsto (fun y => ∫ x in (ball 0 y \ ball 0 (1 / y)), f (x - 1/x)) atTop (𝓝 r) ∧ Tendsto (fun y => ∫ x in ball 0 y, f x) atTop (𝓝 r) := by
Problem: putnam_1968_b5
Category: linear_algebra, number_theory, combinatorics

Let $p$ be a prime number. Find the number of distinct $2 \times 2$ matrices $$\begin{pmatrix} a & b \\ c & d \end{pmatrix}$$ such that $a, b, c, d \in \{0, 1, ..., p - 1\}$, $a + d \equiv 1 \pmod p$, and $ad - bc \equiv 0 \pmod p$.

Solution: There are $p^2 + p$ such matrices.

Lean 4 formalization:
import Mathlib

open Finset Polynomial Topology Filter Metric

abbrev putnam_1968_b5_solution : ℕ → ℕ := sorry
theorem putnam_1968_b5
(p : ℕ)
(hp : Prime p)
: {M : Matrix (Fin 2) (Fin 2) (ZMod p) | M 0 0 + M 1 1 = 1 ∧ M 0 0 * M 1 1 - M 0 1 * M 1 0 = 0}.ncard = putnam_1968_b5_solution p := by
Problem: putnam_1968_b6
Category: analysis

Prove that no sequence $\{K_n\}_{n=0}^{\infty}$ of compact (closed and bounded) sets of rational numbers has the property that every compact set of rational numbers is contained by at least one $K_n$.


Lean 4 formalization:
import Mathlib

open Finset Polynomial Topology Filter Metric

theorem putnam_1968_b6
: ¬∃ K : ℕ → Set ℚ, (∀ n : ℕ, IsCompact (K n)) ∧ (∀ S : Set ℚ, IsCompact S → ∃ n : ℕ, S ⊆ K n) := by
Problem: putnam_1969_a1
Category: algebra, set_theory

What are the possible ranges (across all real inputs $x$ and $y$) of a polynomial $f(x, y)$ with real coefficients?

Solution: Show that the possibles ranges are a single point, any half-open or half-closed semi-infinite interval, or all real numbers.

Lean 4 formalization:
import Mathlib

open Matrix Filter Topology Set Nat

abbrev putnam_1969_a1_solution : Set (Set ℝ) := sorry
theorem putnam_1969_a1
: {{z : ℝ | ∃ x : Fin 2 → ℝ, MvPolynomial.eval x f = z} | f : MvPolynomial (Fin 2) ℝ} = putnam_1969_a1_solution := by
Problem: putnam_1969_a2
Category: linear_algebra

Let $D_n$ be the determinant of the $n$ by $n$ matrix whose value in the $i$th row and $j$th column is $|i-j|$. Show that $D_n = (-1)^{n-1} * (n-1) * (2^{n-2}).$


Lean 4 formalization:
import Mathlib

open Matrix Filter Topology Set Nat

theorem putnam_1969_a2
(D : (n : ℕ) → Matrix (Fin n) (Fin n) ℝ)
(hD : D = fun (n : ℕ) => λ (i : Fin n) (j : Fin n) => |(i : ℝ) - (j : ℝ)| )
: ∀ n, n ≥ 2 → (D n).det = (-1)^((n : ℤ)-1) * ((n : ℤ)-1) * 2^((n : ℤ)-2) := by
Problem: putnam_1969_a4
Category: analysis

Show that $\int_0^1 x^x dx = \sum_{n=1}^{\infty} (-1)^{n+1}n^{-n}$.


Lean 4 formalization:
import Mathlib

open Matrix Filter Topology Set Nat

theorem putnam_1969_a4
: Tendsto (fun n => ∑ i ∈ Finset.Icc (1 : ℤ) n, (-1)^(i+1)*(i : ℝ)^(-i)) atTop (𝓝 (∫ x in Ioo (0 : ℝ) 1, x^x)) := by
Problem: putnam_1969_a5
Category: analysis

Consider the system of differential equations $$\frac{dx}{dt} = -2y + u(t), \frac{dy}{dt} = -2x + u(t)$$ for some continuous function $u(t)$. Prove that, if $x(0) \ne y(0)$, the solution will never pass through $(0, 0)$ regardless of the choice of $u(t)$, and if $x(0) = y(0)$, a suitable $u(t)$ can be chosen for any $T > 0$ so that $(x(T), y(T)) = (0, 0)$.


Lean 4 formalization:
import Mathlib

open Matrix Filter Topology Set Nat

theorem putnam_1969_a5
    (x0 y0 t : ℝ)
    (ht : 0 < t) :
    x0 = y0 ↔ ∃ x y u : ℝ → ℝ,
      Differentiable ℝ x ∧
      Differentiable ℝ y ∧
      Continuous u ∧
      deriv x = - 2 • y + u ∧
      deriv y = - 2 • x + u ∧
      x 0 = x0 ∧
      y 0 = y0 ∧
      x t = 0 ∧
      y t = 0 := by
Problem: putnam_1969_a6
Category: analysis

Let $(x_n)$ be a sequence, and let $y_n = x_{n-1} + 2*x_n$ for $n \geq 2$. Suppose that $(y_n)$ converges, then prove that $(x_n)$ converges.


Lean 4 formalization:
import Mathlib

open Matrix Filter Topology Set Nat

theorem putnam_1969_a6
(x : ℕ → ℝ)
(y : ℕ → ℝ)
(hy1 : ∀ n ≥ 2, y n = x (n-1) + 2 * (x n))
(hy2 : ∃ c : ℝ, Tendsto y atTop (𝓝 c))
: ∃ C : ℝ, Tendsto x atTop (𝓝 C) := by
Problem: putnam_1969_b1
Category: number_theory

Let $n$ be a positive integer such that $n+1$ is divisible by $24$. Prove that the sum of all the divisors of $n$ is divisible by $24$.


Lean 4 formalization:
import Mathlib

open Matrix Filter Topology Set Nat

theorem putnam_1969_b1
(n : ℕ)
(hnpos : n > 0)
(hn : 24 ∣ n + 1)
: 24 ∣ ∑ d ∈ divisors n, d := by
Problem: putnam_1969_b2
Category: abstract_algebra

Show that a finite group can not be the union of two of its proper subgroups. Does the statement remain true if 'two' is replaced by 'three'?

Solution: Show that the statement is no longer true if 'two' is replaced by 'three'.

Lean 4 formalization:
import Mathlib

open Matrix Filter Topology Set Nat

abbrev putnam_1969_b2_solution : Prop := sorry
theorem putnam_1969_b2
    (P : ℕ → Prop)
    (P_def : ∀ n, P n ↔ ∀ (G : Type) [Group G] [Finite G],
      ∀ H : Fin n → Subgroup G, (∀ i, H i < ⊤) → ⋃ i, (H i : Set G) < ⊤) :
    P 2 ∧ (P 3 ↔ putnam_1969_b2_solution) := by
Problem: putnam_1969_b3
Category: analysis

Suppose $T$ is a sequence which satisfies $T_n * T_{n+1} = n$ whenever $n \geq 1$, and also $\lim_{n \to \infty} \frac{T_n}{T_{n+1}} = 1. Show that $\pi * T_1^2 = 2$.


Lean 4 formalization:
import Mathlib

open Matrix Filter Topology Set Nat

theorem putnam_1969_b3
(T : ℕ → ℝ)
(hT1 : ∀ n : ℕ, n ≥ 1 → (T n) * (T (n + 1)) = n)
(hT2 : Tendsto (fun n => (T n)/(T (n + 1))) atTop (𝓝 1))
: Real.pi * (T 1)^2 = 2 := by
Problem: putnam_1969_b4
Category: geometry

$Γ$ is a plane curve of length 1. Show that we can find a closed rectangle of area 1/4 which covers $Γ$.


Lean 4 formalization:
import Mathlib

open scoped Real EuclideanGeometry

theorem putnam_1969_b4
    (Γ : ℝ → EuclideanSpace ℝ (Fin 2))
    --Note: the problem doesn't say what regularity conditions we should impose on `Γ` - hopefully continuity is enough.
    (Γ_cts : ContinuousOn Γ (Set.Icc 0 1))
    (hΓ : eVariationOn Γ (Set.Icc 0 1) = 1) :
    letI : Module.Oriented ℝ (EuclideanSpace ℝ (Fin 2)) (Fin 2) := ⟨Module.Basis.orientation <| PiLp.basisFun 2 ℝ (Fin 2)⟩
    letI : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 2) := ⟨finrank_euclideanSpace_fin⟩
    ∃ (a b c d : EuclideanSpace ℝ (Fin 2)), Γ '' (Set.Icc 0 1) ⊆
      convexHull ℝ {a, b, c, d} ∧ dist a b * dist b c = 1/4 ∧
      --`abcd` is a rectangle
      letI π_div_2 := Real.Angle.coe <| π / 2
      (∡ a b c = π_div_2 ∧ ∡ b c d = π_div_2 ∧ ∡ c d a = π_div_2 ∧ ∡ d a b = π_div_2) := by
Problem: putnam_1969_b5
Category: analysis

Let $a_1 < a_2 < a_3 < \dots$ be an increasing sequence of positive integers. Assume that the sequences $\sum_{i = 1}^{\infty} 1/(a n)$ is convergent. For any number $x$, let $k(x)$ be the number of $a_n$'s which do not exceed $x$. Show that $\lim_{x \to \infty} k(x)/x = 0$.


Lean 4 formalization:
import Mathlib

open Matrix Filter Topology Set Nat

theorem putnam_1969_b5
(a : ℕ → ℝ)
(ha : StrictMono a ∧ (∀ x : ℕ, a x > 0))
(hinvasum : ∃ C : ℝ, Tendsto (fun n => ∑ i : Fin n, 1/(a i)) atTop (𝓝 C))
(k : ℝ → ℕ)
(hk : k = fun x => {n | a n ≤ x}.ncard)
: Tendsto (fun t => (k t)/t) atTop (𝓝 0) := by
Problem: putnam_1969_b6
Category: linear_algebra

Let $A$ be a $3 \times 2$ matrix and $B$ be a $2 \times 3$ matrix such that $$AB =
\begin{pmatrix}
8 & 2 & -2 \\
2 & 5 & 4 \\
-2 & 4 & 5
\end{pmatrix}.
$$ Prove that $$BA =
\begin{pmatrix}
9 & 0 \\
0 & 9
\end{pmatrix}.$$


Lean 4 formalization:
import Mathlib

open Matrix Filter Topology Set Nat

theorem putnam_1969_b6
(A : Matrix (Fin 3) (Fin 2) ℝ)
(B : Matrix (Fin 2) (Fin 3) ℝ)
(p : Fin 3 → Fin 3 → ℝ)
(hp : p 0 0 = 8 ∧ p 0 1 = 2 ∧ p 0 2 = -2 ∧
p 1 0 = 2 ∧ p 1 1 = 5 ∧ p 1 2 = 4 ∧
p 2 0 = -2 ∧ p 2 1 = 4 ∧ p 2 2 = 5)
(hAB : A * B = Matrix.of p)
: B * A = 9 * (1 : Matrix (Fin 2) (Fin 2) ℝ) := by
Problem: putnam_1970_a1
Category: analysis

Prove that, for all $a > 0$ and $b > 0$, the power series of $e^{ax} \cos (bx)$ with respect to $x$ has either zero or infinitely many zero coefficients.


Lean 4 formalization:
import Mathlib

open Metric Set EuclideanGeometry

theorem putnam_1970_a1
(a b : ℝ)
(ha : a > 0)
(hb : b > 0)
(f : ℝ → ℝ)
(f_def : f = fun x : ℝ => Real.exp (a*x) * Real.cos (b*x))
(p : ℕ → ℝ)
(hp : ∃ c : ℝ, c > 0 ∧ ∀ x ∈ ball 0 c, ∑' n : ℕ, (p n)*x^n = f x)
(S : Set ℕ)
(S_def : S = {n : ℕ | p n = 0})
: S = ∅ ∨ ¬Finite S := by
Problem: putnam_1970_a2
Category: analysis, algebra

Let $A$, $B$, $C$, $D$, $E$, $F$, and $G$ be real numbers satisfying $B^2 - 4AC < 0$. Prove that there exists some $\delta > 0$ such that no points $(x, y)$ in the punctured disk $0 < x^2 + y^2 < \delta$ satisfy $$Ax^2 + Bxy + Cy^2 + Dx^3 + Ex^2y + Fxy^2 + Gy^3 = 0.$$


Lean 4 formalization:
import Mathlib

open Metric Set EuclideanGeometry

theorem putnam_1970_a2
(A B C D E F G : ℝ)
(hle : B^2 - 4*A*C < 0)
: ∃ δ > 0, ¬∃ x y : ℝ, x^2 + y^2 ∈ Set.Ioo 0 (δ^2) ∧
A*x^2 + B*x*y + C*y^2 + D*x^3 + E*x^2*y + F*x*y^2 + G*y^3 = 0 := by
Problem: putnam_1970_a3
Category: number_theory

Find the length of the longest possible sequence of equal nonzero digits (in base 10) in which a perfect square can terminate. Also, find the smallest square that attains this length.

Solution: The maximum attainable length is $3$; the smallest such square is $38^2 = 1444$.

Lean 4 formalization:
import Mathlib

open Metric Set EuclideanGeometry

abbrev putnam_1970_a3_solution : ℕ × ℕ := sorry
theorem putnam_1970_a3
(L : ℕ → ℕ)
(hL : ∀ n : ℕ, L n ≤ (Nat.digits 10 n).length ∧
(∀ k : ℕ, k < L n → (Nat.digits 10 n)[k]! = (Nat.digits 10 n)[0]!) ∧
(L n ≠ (Nat.digits 10 n).length → (Nat.digits 10 n)[L n]! ≠ (Nat.digits 10 n)[0]!))
: (∃ n : ℕ, (Nat.digits 10 (n^2))[0]! ≠ 0 ∧ L (n^2) = putnam_1970_a3_solution.1) ∧
(∀ n : ℕ, (Nat.digits 10 (n^2))[0]! ≠ 0 → L (n^2) ≤ putnam_1970_a3_solution.1) ∧
(∃ m : ℕ, m^2 = putnam_1970_a3_solution.2) ∧
L (putnam_1970_a3_solution.2) = putnam_1970_a3_solution.1 ∧
(Nat.digits 10 putnam_1970_a3_solution.2)[0]! ≠ 0 ∧
∀ n : ℕ, (Nat.digits 10 (n^2))[0]! ≠ 0 ∧ L (n^2) = putnam_1970_a3_solution.1 → n^2 ≥ putnam_1970_a3_solution.2 := by
Problem: putnam_1970_a4
Category: analysis

Suppose $(x_n)$ is a sequence such that $\lim_{n \to \infty} (x_n - x_{n-2} = 0$. Prove that $\lim_{n \to \infty} \frac{x_n - x_{n-1}}{n} = 0$.


Lean 4 formalization:
import Mathlib

open Metric Set EuclideanGeometry Filter Topology

theorem putnam_1970_a4
(x : ℕ → ℝ)
(hxlim : Tendsto (fun n => x (n+2) - x n) atTop (𝓝 0))
: Tendsto (fun n => (x (n+1) - x (n))/(n+1)) atTop (𝓝 0) := by
Problem: putnam_1970_b1
Category: analysis

Evaluate the infinite product $\lim_{n \to \infty} \frac{1}{n^4} \prod_{i = 1}^{2n} (n^2 + i^2)^{1/n}$.

Solution: Show that the solution is $e^{2 \log(5) - 4 + 2 arctan(2)}$.

Lean 4 formalization:
import Mathlib

open Metric Set EuclideanGeometry Filter Topology

noncomputable abbrev putnam_1970_b1_solution : ℝ := sorry
theorem putnam_1970_b1
: Tendsto (fun n => 1/(n^4) * ∏ i ∈ Finset.Icc (1 : ℤ) (2*n), ((n^2 + i^2) : ℝ)^((1 : ℝ)/n)) atTop (𝓝 putnam_1970_b1_solution) := by
Problem: putnam_1970_b2
Category: analysis, algebra

Let $H$ be a polynomial of degree at most $3$ and $T$ be a positive real number. Show that the average value of $H(t)$ over the interval $[-T, T]$ equals the average of $H\left(-\frac{T}{\sqrt{3}}\right)$ and $H\left(\frac{T}{\sqrt{3}}\right)$.


Lean 4 formalization:
import Mathlib

open Metric Set EuclideanGeometry Filter Topology

theorem putnam_1970_b2
(T : ℝ)
(H : Polynomial ℝ)
(hT : T > 0)
(hH : H.degree ≤ 3)
: (H.eval (-T / Real.sqrt 3) + H.eval (T / Real.sqrt 3))/2 = ⨍ t in Set.Icc (-T) T, H.eval t := by
Problem: putnam_1970_b3
Category: analysis

A closed subset $S$ of $\mathbb{R}^2$ lies in $a < x < b$. Show that its projection on the y-axis is closed.


Lean 4 formalization:
import Mathlib

open Metric Set EuclideanGeometry Filter Topology

theorem putnam_1970_b3
(S : Set (ℝ × ℝ))
(a b : ℝ)
(hab : a < b)
(hS : ∀ s ∈ S, s.1 ∈ Ioo a b)
(hSclosed : IsClosed S)
: IsClosed {y | ∃ x : ℝ, ⟨x,y⟩ ∈ S} := by
Problem: putnam_1970_b4
Category: analysis

Let $x : \mathbb{R} \to \mathbb{R}$ be a twice differentiable function satisfying $x(1) - x(0) = 1$, $x'(0) = x'(1) = 0$, and $|x'(t)| \le \frac{3}{2}$ for all $t \in (0, 1)$. Prove that there exists some $t \in [0, 1]$ such that $|x''(t)| \ge \frac{9}{2}$.


Lean 4 formalization:
import Mathlib

open Metric Set EuclideanGeometry Filter Topology

theorem putnam_1970_b4
(x : ℝ → ℝ)
(hdiff : DifferentiableOn ℝ x (Set.Icc 0 1) ∧ DifferentiableOn ℝ (deriv x) (Set.Icc 0 1))
(hx : x 1 - x 0 = 1)
(hv : deriv x 0 = 0 ∧ deriv x 1 = 0)
(hs : ∀ t ∈ Set.Ioo 0 1, |deriv x t| ≤ 3/2)
: ∃ t ∈ Set.Icc 0 1, |(deriv (deriv x)) t| ≥ 9/2 := by
Problem: putnam_1970_b5
Category: analysis

Let $u_n$ denote the function $u_n(x) = -n$ if $x \leq -n$, $x$ if $-n < x \leq n$, and $n$ otherwise. Let $F$ be a function on the reals. Show that $F$ is continuous if and only if $u_n \circ F$ is continuous for all natural numbers $n$.


Lean 4 formalization:
import Mathlib

open Metric Set EuclideanGeometry Filter Topology

theorem putnam_1970_b5
(ramp : ℤ → (ℝ → ℝ))
(ramp_def : ramp = fun (n : ℤ) => (fun (x : ℝ) => if x ≤ -n then (-n : ℝ) else (if -n < x ∧ x ≤ n then x else (n : ℝ))))
(F : ℝ → ℝ)
: Continuous F ↔ (∀ n : ℕ, Continuous ((ramp n) ∘ F)) := by
Problem: putnam_1970_b6
Category: geometry

Prove that if a quadrilateral with side lengths $a$, $b$, $c$, and $d$ and area $\sqrt{abcd}$ can be circumscribed to a circle (i.e., a circle can be inscribed in it), then it must be cyclic (i.e., it can be inscribed in a circle).


Lean 4 formalization:
import Mathlib

open Metric Set EuclideanGeometry Filter Topology

theorem putnam_1970_b6
(L : ZMod 4 → (EuclideanSpace ℝ (Fin 2)))
(S : Set (EuclideanSpace ℝ (Fin 2)))
(S_def : S = {L i | i : ZMod 4})
(hSquad : S.ncard = 4 ∧ ∀ s ⊆ S, s.ncard = 3 → ¬ Collinear ℝ s)
(hlens : dist (L 0) (L 1) > 0 ∧ dist (L 1) (L 2) > 0 ∧ dist (L 2) (L 3) > 0 ∧ dist (L 3) (L 0) > 0)
(horder : ∀ i : ZMod 4, segment ℝ (L i) (L (i + 1)) ∩ interior (convexHull ℝ S) = ∅)
(hcircum : ∃ (O: EuclideanSpace ℝ (Fin 2)) (r : ℝ), O ∈ convexHull ℝ S ∧ r > 0 ∧ ∀ i : ZMod 4,
∃! I : EuclideanSpace ℝ (Fin 2), Collinear ℝ {I, L i, L (i + 1)} ∧ dist O I = r)
(harea : (MeasureTheory.volume (convexHull ℝ S)).toReal =
Real.sqrt (dist (L 0) (L 1) * dist (L 1) (L 2) * dist (L 2) (L 3) * dist (L 3) (L 0)))
: Cospherical S := by
Problem: putnam_1971_a1
Category: geometry, combinatorics

Let $S$ be a set of $9$ lattice points (points with integer coordinates) in $3$-dimensional Euclidean space. Prove that there exists a lattice point along the interior of some line segment that joins two distinct points in $S$.


Lean 4 formalization:
import Mathlib

open Set

theorem putnam_1971_a1
(S : Set (ℤ × ℤ × ℤ))
(hS : S.ncard = 9)
(L : (ℤ × ℤ × ℤ) × (ℤ × ℤ × ℤ) → Set (ℝ × ℝ × ℝ))
(hL : L = fun ((a, b, c), (d, e, f)) =>
{(t*a + (1-t)*d, t*b + (1-t)*e, t*c + (1-t)*f) | t ∈ Ioo (0 : ℝ) 1})
: ∃ x y z : ℤ, ∃ P Q : ℤ × ℤ × ℤ, P ∈ S ∧ Q ∈ S ∧ P ≠ Q ∧ ((x : ℝ), (y : ℝ), (z : ℝ)) ∈ L (P, Q) := by
Problem: putnam_1971_a2
Category: algebra

Determine all polynomials $P(x)$ such that $P(x^2 + 1) = (P(x))^2 + 1$ and $P(0) = 0$.

Solution: Show that the only such polynomial is the identity function.

Lean 4 formalization:
import Mathlib

open Set

abbrev putnam_1971_a2_solution : Set (Polynomial ℝ) := sorry
theorem putnam_1971_a2
    (P : Polynomial ℝ) :
    (P.eval 0 = 0 ∧ (∀ x : ℝ, P.eval (x^2 + 1) = (P.eval x)^2 + 1)) ↔ P ∈ putnam_1971_a2_solution := by
Problem: putnam_1971_a3
Category: geometry

The three vertices of a triangle of sides $a,b,c$ are lattice points and lie on a circle of radius $R$. Show that $abc \geq 2R$.


Lean 4 formalization:
import Mathlib

open Set

theorem putnam_1971_a3
    (a b c : ℝ × ℝ)
    (R : ℝ)
    (habclattice : a.1 = round a.1 ∧ a.2 = round a.2 ∧ b.1 = round b.1 ∧ b.2 = round b.2 ∧ c.1 = round c.1 ∧ c.2 = round c.2)
    (habcneq : a ≠ b ∧ a ≠ c ∧ b ≠ c)
    (hR : R > 0)
    (hcircle : ∃ C : ℝ × ℝ,
      √((a.1 - C.1)^2 + (a.2 - C.2)^2) = R ∧
      √((b.1 - C.1)^2 + (b.2 - C.2)^2) = R ∧
      √((c.1 - C.1)^2 + (c.2 - C.2)^2) = R) :
    (√((a.1 - b.1)^2 + (a.2 - b.2)^2)) * (√((a.1 - c.1)^2 + (a.2 - c.2)^2)) * (√((b.1 - c.1)^2 + (b.2 - c.2)^2)) ≥ 2 * R := by
Problem: putnam_1971_a4
Category: analysis

Show that for $\epsilon \in (0,1)$, the expression $(x + y)^n (x^2 - 2-\epsilon)xy + y^2)$ is a polynomial with positive coefficients for $n$ sufficiently large, where $n$ is an integer. 


Lean 4 formalization:
import Mathlib

open Set MvPolynomial

theorem putnam_1971_a4
(ε : ℝ)
(hε : 0 < ε ∧ ε < 1)
(P : ℕ → ℝ → MvPolynomial (Fin 2) ℝ)
(hP : P = fun (n : ℕ) (δ : ℝ) => (MvPolynomial.X 0 + MvPolynomial.X 1)^n * ((MvPolynomial.X 0)^2 - (MvPolynomial.C (2 - δ))*(MvPolynomial.X 0)*(MvPolynomial.X 1) + (MvPolynomial.X 1)^2))
: ∃ N : ℕ, ∀ n ≥ N, ∀ i : Fin 2 →₀ ℕ, MvPolynomial.coeff i (P n ε) ≥ 0 := by
Problem: putnam_1971_a5
Category: number_theory

After each play of a certain game of solitaire, the player receives either $a$ or $b$ points, where $a$ and $b$ are positive integers with $a > b$; scores accumulate from play to play. If there are $35$ unattainable scores, one of which is $58$, find $a$ and $b$.

Solution: Show that the solution is $a = 11$ and $b = 8$.

Lean 4 formalization:
import Mathlib

open Set MvPolynomial

abbrev putnam_1971_a5_solution : ℤ × ℤ := sorry
theorem putnam_1971_a5
    (a b : ℤ)
    (hab : a > 0 ∧ b > 0 ∧ a > b)
    (pab : ℤ → ℤ → Prop)
    (hpab : ∀ x y, pab x y ↔
      {s : ℕ | ¬∃ m n : ℕ, m*x + n*y = s}.ncard = 35 ∧
      ¬∃ m n : ℕ, m*x + n*y = 58) :
    pab a b ↔ a = putnam_1971_a5_solution.1 ∧ b = putnam_1971_a5_solution.2 := by
Problem: putnam_1971_a6
Category: number_theory

Let $c$ be a real number such that $n^c$ is an integer for every positive integer $n$. Show that $c$ is a non-negative integer.


Lean 4 formalization:
import Mathlib

open Set MvPolynomial

theorem putnam_1971_a6
(c : ℝ)
(hc : ∀ n : ℤ, n > 0 → ∃ m : ℤ, (n : ℝ)^c = m)
: ∃ m : ℤ, m ≥ 0 ∧ c = m := by
Problem: putnam_1971_b1
Category: abstract_algebra

Let $S$ be a set and let $\cdot$ be a binary operation on $S$ satisfying the two following laws: (1) for all $x$ in $S$, $x = x \cdot x$, (2) for all $x,y,z$ in $S$, $(x \cdot y) \cdot z) = (y \cdot z) \cdot x$. Show that $\cdot$ is associative and commutative. 


Lean 4 formalization:
import Mathlib

open Set MvPolynomial

theorem putnam_1971_b1
(S : Type*) [Mul S]
(hself : ∀ x : S, x * x = x)
(h2 : ∀ x y z : S, (x * y) * z = (y * z) * x)
: (∀ x y z : S, (x * y) * z = x * (y * z)) ∧ (∀ x y : S, x * y = y * x) := by
Problem: putnam_1971_b2
Category: algebra

Find all functions $F : \mathbb{R} \setminus \{0, 1\} \to \mathbb{R}$ that satisfy $F(x) + F\left(\frac{x - 1}{x}\right) = 1 + x$ for all $x \in \mathbb{R} \setminus \{0, 1\}$.

Solution: The only such function is $F(x) = \frac{x^3 - x^2 - 1}{2x(x - 1)}$.

Lean 4 formalization:
import Mathlib

open Set MvPolynomial

abbrev putnam_1971_b2_solution : Set (ℝ → ℝ) := sorry
theorem putnam_1971_b2
(S : Set ℝ)
(hS : S = univ \ {0, 1})
(P : (ℝ → ℝ) → Prop)
(hP : P = fun (F : ℝ → ℝ) => ∀ x ∈ S, F x + F ((x - 1)/x) = 1 + x)
: (∀ F ∈ putnam_1971_b2_solution, P F) ∧ ∀ f : ℝ → ℝ, P f → ∃ F ∈ putnam_1971_b2_solution, (∀ x ∈ S, f x = F x) := by
Problem: putnam_1971_b3
Category: algebra

If two cars travel around a track at constant speeds of one lap per hour, starting from the same point but at different times, prove that the total amount of time for which the first car has completed exactly twice as many laps as the second is exactly $1$ hour.


Lean 4 formalization:
import Mathlib

open Set MvPolynomial

theorem putnam_1971_b3
(T : ℝ)
(hT : T > 0)
: MeasureTheory.volume {t : ℝ | t ≥ T ∧ Nat.floor t = 2 * (Nat.floor (t - T))} = 1 := by
Problem: putnam_1971_b6
Category: number_theory

Let $\delta(x) be the greatest odd divisor of the positive integer $x$. Show that $|\sum_{n = 1}^x \delta(n)/n - 2x/3| < 1$ for all positive integers $x$.


Lean 4 formalization:
import Mathlib

open Set MvPolynomial

theorem putnam_1971_b6
(δ : ℤ → ℤ)
(hδ : δ = fun n => sSup {t | Odd t ∧ t ∣ n})
: ∀ x : ℤ, x > 0 → |∑ i ∈ Finset.Icc 1 x, (δ i)/(i : ℚ) - 2*x/3| < 1 := by
Problem: putnam_1972_a1
Category: algebra

Show that there are no four consecutive binomial coefficients ${n \choose r}, {n \choose (r+1)}, {n \choose (r+2)}, {n \choose (r+3)}$ where $n,r$ are positive integers and $r+3 \leq n$, which are in arithmetic progression.


Lean 4 formalization:
import Mathlib

open EuclideanGeometry Filter Topology Set

theorem putnam_1972_a1
    (n : ℕ) (hn : n > 0)
    (fourAP : ℤ → ℤ → ℤ → ℤ → Prop)
    (hfourAP : ∀ n1 n2 n3 n4, fourAP n1 n2 n3 n4 ↔ n4-n3 = n3-n2 ∧ n3-n2 = n2-n1) :
    ¬ ∃ r : ℕ, r > 0 ∧ r + 3 ≤ n ∧ fourAP (n.choose r) (n.choose (r+1)) (n.choose (r+2)) (n.choose (r+3)) := by
Problem: putnam_1972_a2
Category: abstract_algebra

Let $S$ be a set and $\cdot$ be a binary operation on $S$ satisfying: (1) for all $x,y$ in $S$, $x \cdot (x \cdot y) = y$ (2) for all $x,y$ in $S$, $(y \cdot x) \cdot x = y$. Show that $\cdot$ is commutative but not necessarily associative.


Lean 4 formalization:
import Mathlib

open EuclideanGeometry Filter Topology Set

theorem putnam_1972_a2
: (∀ (S : Type*) (_ : Mul S), (∀ x y : S, x * (x * y) = y ∧ ((y * x) * x) = y) → (∀ x y : S, x * y = y * x)) ∧ ∃ (S : Type*) (_ : Mul S), (∀ x y : S, x * (x * y) = y ∧ ((y * x) * x) = y) ∧ ¬(∀ x y z : S, x * (y * z) = (x * y) * z) := by