ChristianZ97/putnambench-satp-v4.27 huggingface dataset:
Problem: putnam_1972_a3
Category: analysis

We call a function $f$ from $[0,1]$ to the reals to be supercontinuous on $[0,1]$ if the Cesaro-limit exists for the sequence $f(x_1), f(x_2), f(x_3), \dots$ whenever it does for the sequence $x_1, x_2, x_3 \dots$. Find all supercontinuous functions on $[0,1]$.

Solution: Show that the solution is the set of affine functions.

Lean 4 formalization:
import Mathlib

open EuclideanGeometry Filter Topology Set

abbrev putnam_1972_a3_solution : Set (ℝ → ℝ) := sorry
theorem putnam_1972_a3
    (climit_exists : (ℕ → ℝ) → Prop)
    (supercontinuous : (ℝ → ℝ) → Prop)
    (hclimit_exists : ∀ x, climit_exists x ↔ ∃ C : ℝ, Tendsto (fun n => (∑ i ∈ Finset.range n, (x i))/(n : ℝ)) atTop (𝓝 C))
    (hsupercontinuous : ∀ f, supercontinuous f ↔ ∀ (x : ℕ → ℝ), (∀ i : ℕ, x i ∈ Icc 0 1) → climit_exists x → climit_exists (fun i => f (x i))) :
    {f | supercontinuous f} = putnam_1972_a3_solution := by
Problem: putnam_1972_a5
Category: number_theory

Show that if $n$ is an integer greater than $1$, then $n$ does not divide $2^n - 1$.


Lean 4 formalization:
import Mathlib

open EuclideanGeometry Filter Topology Set

theorem putnam_1972_a5
(n : ℕ)
(hn : n > 1)
: ¬((n : ℤ) ∣ 2^n - 1) := by
Problem: putnam_1972_a6
Category: analysis

Let $f$ be an integrable function in $0 \leq x \leq 1$ and suppose for all $0 \leq i \leq n-1, \int_0^1 x^i f(x) dx = 0$. Further suppose that $\int_0^1 x^n f(x) dx = 1$. Show that $|f(x)| \geq 2^n(n+1)$ on a set of positive measure.


Lean 4 formalization:
import Mathlib

open EuclideanGeometry Filter Topology Set MeasureTheory

theorem putnam_1972_a6
(f : ℝ → ℝ)
(n : ℤ)
(hn : n ≥ 0)
(hfintegrable: IntegrableOn f (Icc 0 1))
(hfint : ∀ i ∈ Icc 0 (n-1), ∫ x in Icc 0 1, x^i*(f x) = 0)
(hfintlast : ∫ x in Icc 0 1, x^n*(f x) = 1)
: ∃ S, S ⊆ Icc (0 : ℝ) 1 ∧ MeasurableSet S ∧ volume S > 0 ∧ ∀ x ∈ S, |f x| ≥ 2^n * (n + 1) := by
Problem: putnam_1972_b1
Category: analysis

Prove that no three consecutive coefficients of the power series of $$\sum_{n = 0}^{\infty} \frac{x^n(x - 1)^{2n}}{n!}$$ all equal $0$.


Lean 4 formalization:
import Mathlib

open EuclideanGeometry Filter Topology Set MeasureTheory Metric

theorem putnam_1972_b1
(S : ℝ → ℝ)
(hS : S = fun (x : ℝ) => ∑' n : ℕ, x^n * (x - 1)^(2*n) / (Nat.factorial n))
(p : ℕ → ℝ)
(hp : ∃ a : ℝ, a > 0 ∧ ∀ x ∈ ball 0 a, ∑' n : ℕ, (p n)*x^n = S x)
: ¬∃ n : ℕ, p n = 0 ∧ p (n + 1) = 0 ∧ p (n + 2) = 0 := by
Problem: putnam_1972_b2
Category: analysis

Let $x : \mathbb{R} \to \mathbb{R}$ be a twice differentiable function whose second derivative is nonstrictly decreasing. If $x(t) - x(0) = s$, $x'(0) = 0$, and $x'(t) = v$ for some $t > 0$, find the maximum possible value of $t$ in terms of $s$ and $v$.

Solution: Show that the maximum possible time is $t = \frac{2s}{v}$.

Lean 4 formalization:
import Mathlib

open EuclideanGeometry Filter Topology Set MeasureTheory Metric

noncomputable abbrev putnam_1972_b2_solution : ℝ → ℝ → ℝ := sorry
theorem putnam_1972_b2
    (s v : ℝ)
    (hs : s > 0)
    (hv : v > 0)
    (valid : ℝ → (ℝ → ℝ) → Prop)
    (hvalid : ∀ t x, valid t x ↔
      DifferentiableOn ℝ x (Set.Icc 0 t) ∧ DifferentiableOn ℝ (deriv x) (Set.Icc 0 t) ∧
      AntitoneOn (deriv (deriv x)) (Set.Icc 0 t) ∧
      deriv x 0 = 0 ∧ deriv x t = v ∧ x t - x 0 = s)
    : IsGreatest {t | ∃ x : ℝ → ℝ, valid t x} (putnam_1972_b2_solution s v) := by
Problem: putnam_1972_b3
Category: abstract_algebra

Let $A$ and $B$ be two elements in a group such that $ABA = BA^2B$, $A^3 = 1$, and $B^{2n-1} = 1$ for some positive integer $n$. Prove that $B = 1$.


Lean 4 formalization:
import Mathlib

open EuclideanGeometry Filter Topology Set MeasureTheory Metric

theorem putnam_1972_b3
(G : Type*) [Group G]
(A B : G)
(hab : A * B * A = B * A^2 * B ∧ A^3 = 1 ∧ (∃ n : ℤ, n > 0 ∧ B^(2*n - 1) = 1))
: B = 1 := by
Problem: putnam_1972_b4
Category: algebra

Let $n \geq 2$ be an integer. Show that there exists a polynomial $P(x,y,z)$ with integral coefficients such that $x \equiv P(x^n, x^{n+1}, x + x^{n+2})$.


Lean 4 formalization:
import Mathlib

open EuclideanGeometry Filter Topology Set MeasureTheory Metric

theorem putnam_1972_b4
(n : ℕ)
(hn : n > 1)
(vars : ℤ → ℤ → ℤ → (Fin 3 → ℤ))
(hvars : vars = fun a b c ↦ fun i ↦ ite (i = 0) a (ite (i = 1) b c))
: ∃ P : MvPolynomial (Fin 3) ℤ, ∀ x : ℤ, x = MvPolynomial.eval (vars (x^n) (x^(n+1)) (x + x^(n+2))) P := by
Problem: putnam_1972_b5
Category: geometry

Let $ABCD$ be a skew (non-planar) quadrilateral. Prove that if $\angle ABC = \angle CDA$ and $\angle BCD = \angle DAB$, then $AB = CD$ and $AD = BC$.


Lean 4 formalization:
import Mathlib

open EuclideanGeometry Set Metric

theorem putnam_1972_b5
(A B C D : EuclideanSpace ℝ (Fin 3))
(hnonplanar : ¬Coplanar ℝ {A, B, C, D})
(hangles : ∠ A B C = ∠ C D A ∧ ∠ B C D = ∠ D A B)
: dist A B = dist C D ∧ dist B C = dist D A := by
Problem: putnam_1972_b6
Category: analysis

Let $n_1 < n_2 < \dots < n_k$ be a set of positive integers. Prove that the polynomail $1 + z^{n_1} + z^{n_2} + \dots + z^{n_k}$ has not roots inside the circle $|z| < (\frac{\sqrt{5}-1}{2}$.


Lean 4 formalization:
import Mathlib

open EuclideanGeometry Filter Topology Set MeasureTheory Metric

theorem putnam_1972_b6
(k : ℕ)
(hk : k ≥ 1)
(n : Fin k → ℤ)
(hn : ∀ i : Fin k, n i > 0)
(hn' : ∀ i j : Fin k, i < j → n i < n j)
(zpoly : ℂ → ℂ)
(hzpoly : zpoly = fun z => 1 + ∑ i : Fin k, z^(n i))
: ∀ z : ℂ, z ∈ ball 0 ((Real.sqrt 5 - 1)/2) → zpoly z ≠ 0 := by
Problem: putnam_1973_a1
Category: geometry

Let $\triangle ABC$ be any triangle in the Euclidean plane, and let points $X$, $Y$, and $Z$ lie on sides $\overline{BC}$, $\overline{CA}$, and $\overline{AB}$ respectively. If $BX \le XC$, $CY \le YA$, and $AZ \le ZB$, prove that $[\triangle XYZ] \ge \frac{1}{4} [\triangle ABC]$.  Regardless of this constraint on $X$, $Y$, and $Z$, prove that one of $[\triangle AZY]$, $[\triangle BXZ]$, or $[\triangle CYX]$ is less than or equal to $[\triangle XYZ]$. (Here, $[\triangle]$ denotes the area of triangle $\triangle$.)


Lean 4 formalization:
import Mathlib

open Nat Set MeasureTheory Topology Filter

theorem putnam_1973_a1
(A B C X Y Z : EuclideanSpace ℝ (Fin 2))
(hnoncol : ¬Collinear ℝ {A, B, C})
(hX : X ∈ segment ℝ B C)
(hY : Y ∈ segment ℝ C A)
(hZ : Z ∈ segment ℝ A B)
: ((dist B X ≤ dist X C ∧ dist C Y ≤ dist Y A ∧ dist A Z ≤ dist Z B) →
volume (convexHull ℝ {X, Y, Z}) ≥ (1/4) * volume (convexHull ℝ {A, B, C})) ∧
sInf {volume (convexHull ℝ {A, Z, Y}), volume (convexHull ℝ {B, X, Z}), volume (convexHull ℝ {C, Y, X})} ≤ volume (convexHull ℝ {X, Y, Z}) := by
Problem: putnam_1973_a2
Category: analysis

Consider an infinite series whose $n$th term is given by $\pm \frac{1}{n}$, where the actual values of the $\pm$ signs repeat in blocks of $8$ (so the $\frac{1}{9}$ term has the same sign as the $\frac{1}{1}$ term, and so on). Call such a sequence balanced if each block contains four $+$ and four $-$ signs. Prove that being balanced is a sufficient condition for the sequence to converge. Is being balanced also necessary for the sequence to converge?

Solution: Show that the condition is necessary.

Lean 4 formalization:
import Mathlib

open Nat Set MeasureTheory Topology Filter

abbrev putnam_1973_a2_solution : Prop := sorry
theorem putnam_1973_a2
(L : List ℝ)
(hL : L.length = 8 ∧ ∀ i : Fin L.length, L[i] = 1 ∨ L[i] = -1)
(pluses : ℕ)
(hpluses : pluses = {i : Fin L.length | L[i] = 1}.ncard)
(S : ℕ → ℝ)
(hS : S = fun n : ℕ ↦ ∑ i ∈ Finset.Icc 1 n, L[i % 8]/i)
: (pluses = 4 → ∃ l : ℝ, Tendsto S atTop (𝓝 l)) ∧ (putnam_1973_a2_solution ↔ ((∃ l : ℝ, Tendsto S atTop (𝓝 l)) → pluses = 4)) := by
Problem: putnam_1973_a3
Category: number_theory

Let $n$ be a fixed positive integer and let $b(n)$ be the minimum value of $k + \frac{n}{k}$ as $k$ is allowed to range through all positive integers. Prove that $b(n)$ and $\sqrt{4n + 1}$ have the same integer part.


Lean 4 formalization:
import Mathlib

open Nat Set MeasureTheory Topology Filter

theorem putnam_1973_a3
(b : ℤ → ℝ)
(hb : b = fun (n : ℤ) => sInf {k + (n : ℝ)/(k : ℝ) | k > (0 : ℤ)})
: ∀ n : ℤ, n > 0 → floor (b n) = floor (Real.sqrt (4 * n + 1)) := by
Problem: putnam_1973_a4
Category: analysis

How many zeros does the function $f(x) = 2^x - 1 - x^2$ have on the real line?

Solution: Show that the solution is 3.

Lean 4 formalization:
import Mathlib

open Nat Set MeasureTheory Topology Filter

abbrev putnam_1973_a4_solution : ℕ := sorry
theorem putnam_1973_a4
(f : ℝ → ℝ)
(hf : f = fun x => 2^x - 1 - x^2)
: putnam_1973_a4_solution = {x : ℝ | f x = 0}.ncard := by
Problem: putnam_1973_a6
Category: geometry

Prove that it is impossible for seven distinct straight lines to be situated in the Euclidean plane so as to have at least six points where exactly three of these lines intersect and at least four points where exactly two of these lines interest.


Lean 4 formalization:
import Mathlib

open Nat Set MeasureTheory Topology Filter

theorem putnam_1973_a6
(nint : ℕ → (Fin 7 → (ℝ × ℝ)) → ℕ)
(h_nint : nint = fun n lines => {p : ℝ × ℝ | ∃! S : Set (Fin 7), S.ncard = n ∧ p ∈ ⋂ i ∈ S, {pts | pts.2 = (lines i).1 * pts.1 + (lines i).2}}.ncard)
: ¬ ∃ lines : Fin 7 → (ℝ × ℝ), (∀ i j : Fin 7, i ≠ j → lines i ≠ lines j) ∧ nint 3 lines ≥ 6 ∧ nint 2 lines ≥ 4 := by
Problem: putnam_1973_b1
Category: algebra

Let $a_1, \dots, a_{2n + 1}$ be a set of integers such that, if any one of them is removed, the remaining ones can be divided into two sets of $n$ integers with equal sums. Prove $a_1 = a_2 = \dots = a_{2n+1}$.


Lean 4 formalization:
import Mathlib

open Nat Set MeasureTheory Topology Filter

theorem putnam_1973_b1
(n : ℕ)
(a : Finset.Icc 1 (2 * n + 1) → ℤ)
(h_remove : ∀ S : Finset (Finset.Icc 1 (2 * n + 1)), S.card = 2*n → ∃ T, T ⊆ S ∧ T.card = n ∧ ∑ i ∈ T, a i = ∑ i ∈ (S \ T), a i)
: ∀ i j : Finset.Icc 1 (2 * n + 1), a i = a j := by
Problem: putnam_1973_b2
Category: number_theory

Let $z = x+iy$ be a complex number with $x$ and $y$ rational and with $\| z \| = 1$. Show thaat the number $\| z^{2n} - 1 \|$ is rational for every integer $n$.


Lean 4 formalization:
import Mathlib

open Nat Set MeasureTheory Topology Filter

theorem putnam_1973_b2
(z : ℂ)
(hzrat : ∃ q1 q2 : ℚ, z.re = q1 ∧ z.im = q2)
(hznorm : ‖z‖ = 1)
: ∀ n : ℤ, ∃ q : ℚ, ‖z^(2*n) - 1‖ = q := by
Problem: putnam_1973_b3
Category: number_theory, algebra

Let $p > 1$ be an integer with the property that $x^2 - x + p$ is prime for all $x$ in the range $0 < x < p$. Show there exists exactly one triple of integers $a,b,c$ satisfying $b^2 - 4ac = 1 - 4p$, $0 < a \leq c$, and $-a \leq b < a$.


Lean 4 formalization:
import Mathlib

open Nat Set MeasureTheory Topology Filter

theorem putnam_1973_b3
(p : ℕ)
(pgt1 : p > 1)
(hprime : ∀ x ∈ Set.Ico 0 p, Nat.Prime (x^2 - x + p))
: ∃! triple : ℤ × ℤ × ℤ, let (a,b,c) := triple; b^2 - 4*a*c = 1 - 4*p ∧ 0 < a ∧ a ≤ c ∧ -a ≤ b ∧ b < a := by
Problem: putnam_1973_b4
Category: analysis

Suppose $f$ is a function on $[0,1]$ with continuous derivative satisfying $0 < f'(x) \leq 1$ and $f 0 = 0$. Prove that $\left[\int_0^1 f(x) dx\right]]^2 \geq \int_0^1 (f(x))^3 dx$, and find an example where equality holds.

Solution: Show that one such example where equality holds is the identity function.

Lean 4 formalization:
import Mathlib

open Nat Set MeasureTheory Topology Filter

abbrev putnam_1973_b4_solution : ℝ → ℝ := sorry
theorem putnam_1973_b4
(f : ℝ → ℝ)
(hprop : (ℝ → ℝ) → Prop)
(hprop_def : hprop = fun g => ContDiff ℝ 1 g ∧ (∀ x : ℝ, 0 < deriv g x ∧ deriv g x ≤ 1) ∧ g 0 = 0)
(hf : hprop f)
: (∫ x in Icc 0 1, f x)^2 ≥ ∫ x in Icc 0 1, (f x)^3 ∧ (hprop putnam_1973_b4_solution ∧ (∫ x in Icc 0 1, putnam_1973_b4_solution x)^2 = ∫ x in Icc 0 1, (putnam_1973_b4_solution x)^3) := by
Problem: putnam_1974_a1
Category: number_theory

Call a set of positive integers 'conspiratorial' if no three of them are pairwise relatively prime. What is the largest number of elements in any conspiratorial subset of the integers 1 through 16?

Solution: Show that the answer is 11.

Lean 4 formalization:
import Mathlib

open Set

abbrev putnam_1974_a1_solution : ℕ := sorry
theorem putnam_1974_a1
    (conspiratorial : Set ℤ → Prop)
    (hconspiratorial : ∀ S, conspiratorial S ↔ ∀ a ∈ S, ∀ b ∈ S, ∀ c ∈ S, (a > 0 ∧ b > 0 ∧ c > 0) ∧ ((a ≠ b ∧ b ≠ c ∧ a ≠ c) → (Int.gcd a b > 1 ∨ Int.gcd b c > 1 ∨ Int.gcd a c > 1))) :
    IsGreatest {k | ∃ S, S ⊆ Icc 1 16 ∧ conspiratorial S ∧ S.encard = k} putnam_1974_a1_solution := by
Problem: putnam_1974_a3
Category: number_theory

A well-known theorem asserts that a prime $p > 2$ can be written as the sum of two perfect squres if and only if $p \equiv 1 \bmod 4$. Find which primes $p > 2$ can be written in each of the following forms, using (not necessarily positive) integers $x$ and $y$: (a) $x^2 + 16y^2$, (b) $4x^2 + 4xy + 5y^2$.

Solution: Show that that the answer to (a) is the set of primes which are $1 \bmod 8$, and the solution to (b) is the set of primes which are $5 \bmod 8$.

Lean 4 formalization:
import Mathlib

open Set

abbrev putnam_1974_a3_solution : (Set ℕ) × (Set ℕ) := sorry
theorem putnam_1974_a3
(assmption : ∀ p : ℕ, p.Prime ∧ p > 2 → ((∃ m n : ℤ, p = m^2 + n^2) ↔ p ≡ 1 [MOD 4]))
: ∀ p : ℕ, ((p.Prime ∧ p > 2 ∧ (∃ x y : ℤ, p = x^2 + 16*y^2)) ↔ p ∈ putnam_1974_a3_solution.1) ∧ ((p.Prime ∧ p > 2 ∧ (∃ x y : ℤ, p = 4*x^2 + 4*x*y + 5*y^2)) ↔ p ∈ putnam_1974_a3_solution.2) := by
Problem: putnam_1974_a4
Category: algebra

Evaluate in closed form: $\frac{1}{2^{n-1}} \sum_{k < n/2} (n-2k)*{n \choose k}$.

Solution: Show that the solution is $\frac{n}{2^{n-1}} * {(n-1) \choose \left[ (n-1)/2 \right]}$.

Lean 4 formalization:
import Mathlib

open Set Nat

noncomputable abbrev putnam_1974_a4_solution : ℕ → ℚ := sorry

theorem putnam_1974_a4
    (n : ℕ)
    (hn : 0 < n) :
    (1 : ℚ) / (2 ^ (n - 1)) * ∑ k ∈ Finset.Icc 0 ⌊n / 2⌋₊, (n - 2 * k) * (n.choose k) =
    putnam_1974_a4_solution n := by
Problem: putnam_1974_a6
Category: algebra

Given $n$, let $k(n)$ be the minimal degree of any monic integral polynomial $f$ such that the value of $f(x)$ is divisible by $n$ for every integer $x$. Find the value of $k(1000000)$.

Solution: Show that the answer is 25.

Lean 4 formalization:
import Mathlib

open Set Nat Polynomial

abbrev putnam_1974_a6_solution : ℕ := sorry
theorem putnam_1974_a6
(hdivnallx : Polynomial ℤ → Prop)
(hdivnallx_def : hdivnallx = fun f => Monic f ∧ (∀ x : ℤ, (10^6 : ℤ) ∣ f.eval x))
: sInf {d : ℕ | ∃ f : Polynomial ℤ, hdivnallx f ∧ d = f.natDegree} = putnam_1974_a6_solution := by
Problem: putnam_1974_b1
Category: algebra, geometry

Prove that the optimal configuration of 5 (not necessarily distinct) points $p_1, \dots, p_5$ on the unit circle which maximizes the sum of the ten distances \[\Sigma_{i < j}, d(p_i, p_j) \] is the one which evenly spaces the points like a regular pentagon.


Lean 4 formalization:
import Mathlib

open Set Nat Polynomial

abbrev putnam_1974_b1_solution : (Fin 5 → EuclideanSpace ℝ (Fin 2)) → Prop := sorry

theorem putnam_1974_b1
    (d : (Fin 5 → EuclideanSpace ℝ (Fin 2)) → ℝ)
    (d_def : ∀ p, d p = ∑ ⟨i, j⟩ : Fin 5 × Fin 5, if i < j then dist (p i) (p j) else 0)
    (p : Fin 5 → EuclideanSpace ℝ (Fin 2))
    (hp : ∀ i, ‖p i‖ = 1) :
    d p = sSup {d q | (q) (hq : ∀ i, ‖q i‖ = 1)} ↔ putnam_1974_b1_solution p := by
Problem: putnam_1974_b2
Category: analysis

Let $y(x)$ be a continuously differentiable real-valued function of a real vairable $x$. Show that if $(y')^2 + y^3 \to 0$ as $x \to +\infty$, then $y(x)$ and $y'(x) \to 0$ as $x \to +\infty$.


Lean 4 formalization:
import Mathlib

open Set Nat Polynomial Filter Topology

theorem putnam_1974_b2
(y : ℝ → ℝ)
(ycontdiff : ContDiff ℝ 1 y)
(limy : Tendsto (fun x : ℝ => (deriv y x)^2 + (y x)^3) atTop (𝓝 0))
: Tendsto y atTop (𝓝 0) ∧ Tendsto (deriv y) atTop (𝓝 0) := by
Problem: putnam_1974_b3
Category: number_theory

Prove that if $\alpha$ is a real number such that $\cos (\pi \alpha) = 1/3$, the $\alpha$ is irrational.


Lean 4 formalization:
import Mathlib

open Set Nat Polynomial Filter Topology

theorem putnam_1974_b3
(α : ℝ)
(ha : Real.cos (Real.pi * α) = (1 : ℝ)/3)
: Irrational α := by
Problem: putnam_1974_b4
Category: analysis

Let $f : \mathbb{R} \to \mathbb{R}$ be continuous in each variable seperately. Show that there exists a sequence of continuous functions $g_n : \mathbb{R}^2 \to \mathbb{R}$ such that $f(x,y) = \lim_{n \to \infty} g_n(x,y)$ for all $(x,y) \in \mathbb{R}^2$.


Lean 4 formalization:
import Mathlib

open Set Nat Polynomial Filter Topology

theorem putnam_1974_b4
(f : ℝ × ℝ → ℝ)
(hfcontx : ∀ y : ℝ, Continuous (fun x => f ⟨x, y⟩))
(hfconty : ∀ x : ℝ, Continuous (fun y => f ⟨x, y⟩))
: ∃ g : ℕ → (ℝ × ℝ → ℝ), (∀ n : ℕ, Continuous (g n)) ∧ (∀ x y : ℝ, Tendsto (fun n => g n ⟨x, y⟩) atTop (𝓝 (f ⟨x, y⟩))) := by
Problem: putnam_1974_b5
Category: analysis

Show that $1 + (n/1!) + (n^2/2!) + \dots + (n^n/n!) > e^n/2$ for every integer $n \geq 0$.


Lean 4 formalization:
import Mathlib

open Set Nat Polynomial Filter Topology

theorem putnam_1974_b5
: ∀ n ≥ 0, ∑ i ∈ Finset.Icc (0 : ℕ) n, (n^i : ℝ)/(Nat.factorial i) > (Real.exp n)/2 := by
Problem: putnam_1974_b6
Category: set_theory

For a set with $1000$ elements, how many subsets are there whose candinality is respectively $\equiv 0 \bmod 3, \equiv 1 \bmod 3, \equiv 2 \bmod 3$?

Solution: Show that there answer is that there are $(2^1000-1)/3$ subsets of cardinality $\equiv 0 \bmod 3$ and $\equiv 1 \bmod 3$, and $1 + (2^1000-1)/3$ subsets of cardinality $\equiv 2 \bmod 3$.

Lean 4 formalization:
import Mathlib

open Set Nat Polynomial Filter Topology

abbrev putnam_1974_b6_solution : (ℕ × ℕ × ℕ) := sorry
theorem putnam_1974_b6
(n : ℤ)
(hn : n = 1000)
(count0 count1 count2 : ℕ)
(hcount0 : count0 = {S | S ⊆ Finset.Icc 1 n ∧ S.card ≡ 0 [MOD 3]}.ncard)
(hcount1 : count1 = {S | S ⊆ Finset.Icc 1 n ∧ S.card ≡ 1 [MOD 3]}.ncard)
(hcount2 : count2 = {S | S ⊆ Finset.Icc 1 n ∧ S.card ≡ 2 [MOD 3]}.ncard)
: (count0, count1, count2) = putnam_1974_b6_solution := by
Problem: putnam_1975_a1
Category: algebra, number_theory

If an integer $n$ can be written as the sum of two triangular numbers (that is, $n = \frac{a^2 + a}{2} + \frac{b^2 + b}{2}$ for some integers $a$ and $b$), express $4n + 1$ as the sum of the squares of two integers $x$ and $y$, giving $x$ and $y$ in terms of $a$ and $b$. Also, show that if $4n + 1 = x^2 + y^2$ for some integers $x$ and $y$, then $n$ can be written as the sum of two triangular numbers.

Solution: $x = a + b + 1$ and $y = a - b$ (or vice versa).

Lean 4 formalization:
import Mathlib

open Polynomial

abbrev putnam_1975_a1_solution : ((ℤ × ℤ) → ℤ) × ((ℤ × ℤ) → ℤ) := sorry
theorem putnam_1975_a1
(nab nxy : (ℤ × ℤ × ℤ) → Prop)
(hnab : nab = fun (n, a, b) => n = (a^2 + (a : ℚ))/2 + (b^2 + (b : ℚ))/2)
(hnxy : nxy = fun (n, x, y) => 4*n + 1 = x^2 + y^2)
: (∀ n a b : ℤ, nab (n, a, b) → nxy (n, putnam_1975_a1_solution.1 (a, b), putnam_1975_a1_solution.2 (a, b))) ∧
∀ n : ℤ, (∃ x y : ℤ, nxy (n, x, y)) → ∃ a b : ℤ, nab (n, a, b) := by
Problem: putnam_1975_a2
Category: algebra

For which ordered pairs $(b, c)$ of real numbers do both roots of $z^2 + bz + c$ lie strictly inside the unit disk (i.e., $\{|z| < 1\}$) in the complex plane?

Solution: The desired region is the strict interior of the triangle with vertices $(0, -1)$, $(2, 1)$, and $(-2, 1)$.

Lean 4 formalization:
import Mathlib

open Polynomial

abbrev putnam_1975_a2_solution : (ℝ × ℝ) → Prop := sorry
theorem putnam_1975_a2
: ∀ b c : ℝ, (∀ z : ℂ, (X^2 + (C (b : ℂ))*X + (C (c : ℂ)) : Polynomial ℂ).eval z = 0 → ‖z‖ < 1) ↔ putnam_1975_a2_solution (b, c) := by
Problem: putnam_1975_a3
Category: algebra

If $a$, $b$, and $c$ are real numbers satisfying $0 < a < b < c$, at what points in the set $$\{(x, y, z) \in \mathbb{R}^3 : x^b + y^b + z^b = 1, x \ge 0, y \ge 0, z \ge 0\}$$ does $f(x, y, z) = x^a + y^b + z^c$ attain its maximum and minimum?

Solution: $f$ attains its maximum at $\left(x_0, (1 - x_0^b)^{\frac{1}{b}}, 0\right)$ and its minimum at $\left(0, (1 - z_0^b)^{\frac{1}{b}}, z_0\right)$, where $x_0 = \left(\frac{a}{b}\right)^{\frac{1}{b-a}}$ and $z_0 = \left(\frac{b}{c}\right)^{\frac{1}{c-b}}$.

Lean 4 formalization:
import Mathlib

open Polynomial

noncomputable abbrev putnam_1975_a3_solution : ((ℝ × ℝ × ℝ) → (ℝ × ℝ × ℝ)) × ((ℝ × ℝ × ℝ) → (ℝ × ℝ × ℝ)) := sorry
theorem putnam_1975_a3
(a b c : ℝ)
(hi : 0 < a ∧ a < b ∧ b < c)
(P : (ℝ × ℝ × ℝ) → Prop)
(f : (ℝ × ℝ × ℝ) → ℝ)
(hP : P = fun (x, y, z) => x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ x^b + y^b + z^b = 1)
(hf : f = fun (x, y, z) => x^a + y^b + z^c)
: (P (putnam_1975_a3_solution.1 (a, b, c)) ∧ ∀ x y z : ℝ, P (x, y, z) →
f (x, y, z) ≤ f (putnam_1975_a3_solution.1 (a, b, c))) ∧
(P (putnam_1975_a3_solution.2 (a, b, c)) ∧ ∀ x y z : ℝ, P (x, y, z) →
f (x, y, z) ≥ f (putnam_1975_a3_solution.2 (a, b, c))) := by
Problem: putnam_1975_a4
Category: algebra

Let $n = 2m$, where $m$ is an odd integer greater than 1. Let $\theta = e^{2\pi i/n}$. Expression $(1 - \theta)^{-1}$ explicitly as a polynomial in $\theta$ \[ a_k \theta^k  + a_{k-1}\theta^{k-1} + \dots + a_1\theta + a_0\], with integer coefficients $a_i$.

Solution: Show that the solution is the polynomial $0 + \theta + \theta^3 + \dots + \theta^{m-2}$, alternating consecutive coefficients between 0 and 1.

Lean 4 formalization:
import Mathlib

open Polynomial Real Complex

noncomputable abbrev putnam_1975_a4_solution : ℕ → Polynomial ℤ := sorry
theorem putnam_1975_a4
(m : ℕ)
(hm : Odd m ∧ m > 1)
(θ : ℂ)
(hθ : θ = cexp (2 * Real.pi * I / (2 * m)))
: 1/(1 - θ) = Polynomial.aeval θ (putnam_1975_a4_solution m) := by
Problem: putnam_1975_a5
Category: analysis

On some interval $I$ of the real line, let $y_1(x), y_2(x)$ be linearly independent solutions of the differential equation \[y'' = f(x)y\], where $f(x)$ is a continuous real-valued function. Suppose that $y_1(x) > 0$ and $y_2(x) > 0$ on $I$. Show that there exists a positive constant $c$ such that, on $I$, the function \[z(x) = c \sqrt{y_1(x)y_2(x)}\] satisfies the equation \[z'' + 1/z^3 = f(x)z.\]


Lean 4 formalization:
import Mathlib

open Polynomial Real Complex

theorem putnam_1975_a5
(I : Interval ℝ)
(f y1 y2 : ℝ → ℝ)
(hfcont : Continuous f)
(hycdiff : ContDiff ℝ 2 y1 ∧ ContDiff ℝ 2 y2)
(hy1sol : ∀ x : ℝ, iteratedDeriv 2 y1 x = (f x) * (y1 x))
(hy2sol : ∀ x : ℝ, iteratedDeriv 2 y2 x = (f x) * (y2 x))
(hylinindep : ∀ c1 c2 : ℝ, (∀ x : ℝ, c1 * y1 x + c2 * y2 x = 0) → (c1 = 0 ∧ c2 = 0))
(hyI : ∀ x ∈ I, y1 x > 0 ∧ y2 x > 0)
: ∃ c : ℝ, c > 0 ∧ (let z : ℝ → ℝ := fun x => c * Real.sqrt ((y1 x) * (y2 x)); ∀ x ∈ I, iteratedDeriv 2 z x + 1/(z x)^3 = (f x) * (z x)) := by
Problem: putnam_1975_b1
Category: abstract_algebra, number_theory

Let $H$ be a subgroup of the additive group of ordered pairs of integers under componentwise addition. If $H$ is generated by the elements $(3, 8)$, $(4, -1)$, and $(5, 4)$, then $H$ is also generated by two elements $(1, b)$ and $(0, a)$ for some integer $b$ and positive integer $a$. Find $a$.

Solution: $a$ must equal $7$.

Lean 4 formalization:
import Mathlib

open Polynomial Real Complex

abbrev putnam_1975_b1_solution : ℤ := sorry
theorem putnam_1975_b1
(H : Set (ℤ × ℤ))
(hH : H = {(x, y) : (ℤ × ℤ) | ∃ u v w : ℤ, (x, y) = (u*3 + v*4 + w*5, u*8 + v*(-1) + w*4)})
: (∃ b : ℤ, H = {(x, y) : (ℤ × ℤ) | ∃ u v : ℤ, (x, y) = (u, u*b + v*putnam_1975_b1_solution)}) ∧ putnam_1975_b1_solution > 0 := by
Problem: putnam_1975_b2
Category: analysis, geometry

In three-dimensional Euclidean space, define a \emph{slab} to be the open set of points lying between two parallel planes. The distance between the planes is called the \emph{thickness} of the slab. Given an infinite sequence $S_1, S_2, \dots$ of slabs of thicknesses $d_1, d_2, \dots,$ respectively, such that $\Sigma_{i=1}^{\infty} d_i$ converges, prove that there is some point in the space which is not contained in any of the slabs. 


Lean 4 formalization:
import Mathlib

open Polynomial Real Complex Matrix Filter Topology

theorem putnam_1975_b2
(slab : (Fin 3 → ℝ) → ℝ → ℝ → Set (Fin 3 → ℝ))
(hslab : slab = fun normal offset thickness => {x : Fin 3 → ℝ | offset < normal ⬝ᵥ x ∧ normal ⬝ᵥ x < offset + thickness})
(normals : ℕ → (Fin 3 → ℝ))
(offsets : ℕ → ℝ)
(thicknesses : ℕ → ℝ)
(hnormalsunit : ∀ i : ℕ, ‖normals i‖ = 1)
(hthicknessespos : ∀ i : ℕ, thicknesses i > 0)
(hthicknessesconv : ∃ C : ℝ, Tendsto (fun i : ℕ => ∑ j ∈ Finset.range i, thicknesses j) atTop (𝓝 C))
: Set.univ ≠ ⋃ i : ℕ, slab (normals i) (offsets i) (thicknesses i) := by