ChristianZ97/putnambench-satp-v4.27 huggingface dataset:
Problem: putnam_1965_a5
Category: combinatorics

How many orderings of the integers from $1$ to $n$ satisfy the condition that, for every integer $i$ except the first, there exists some earlier integer in the ordering which differs from $i$ by $1$?

Solution: There are $2^{n-1}$ such orderings.

Lean 4 formalization:
import Mathlib

open EuclideanGeometry Topology Filter Complex

abbrev putnam_1965_a5_solution : ℕ → ℕ := sorry
theorem putnam_1965_a5
: ∀ n > 0, {p ∈ permsOfFinset (Finset.Icc 1 n) | ∀ m ∈ Finset.Icc 2 n, ∃ k ∈ Finset.Ico 1 m, p m = p k + 1 ∨ p m = p k - 1}.card = putnam_1965_a5_solution n := by
Problem: putnam_1965_a6
Category: geometry

Prove that the line $ux + vy = 1$ (where $u \ge 0$ and $v \ge 0$) will lie tangent to the curve $x^m + y^m = 1$ (where $m > 1$) if and only if $u^n + v^n = 1$ for some $n$ such that $m^{-1} + n^{-1} = 1$.


Lean 4 formalization:
import Mathlib

open EuclideanGeometry Topology Filter Complex

theorem putnam_1965_a6
    (u v m : ℝ)
    (hu : 0 < u)
    (hv : 0 < v)
    (hm : 1 < m) :
    (∃ᵉ (x > 0) (y > 0),
      u * x + v * y = 1 ∧
      x ^ m + y ^ m = 1 ∧
      u = x ^ (m - 1) ∧
      v = y ^ (m - 1)) ↔
    ∃ n, u ^ n + v ^ n = 1 ∧ m⁻¹ + n⁻¹ = 1 := by
Problem: putnam_1965_b1
Category: analysis

Find $$\lim_{n \to \infty} \int_{0}^{1} \int_{0}^{1} \cdots \int_{0}^{1} \cos^2\left(\frac{\pi}{2n}(x_1 + x_2 + \cdots + x_n)\right) dx_1 dx_2 \cdots dx_n.$$

Solution: Show that the limit is $\frac{1}{2}$.

Lean 4 formalization:
import Mathlib

open EuclideanGeometry Topology Filter Complex

noncomputable abbrev putnam_1965_b1_solution : ℝ := sorry
theorem putnam_1965_b1
: Tendsto (fun n : ℕ ↦ ∫ x in {x : Fin (n+1) → ℝ | ∀ k : Fin (n+1), x k ∈ Set.Icc 0 1}, (Real.cos (Real.pi/(2 * (n+1)) * ∑ k : Fin (n+1), x k))^2) atTop (𝓝 putnam_1965_b1_solution) := by
Problem: putnam_1965_b2
Category: combinatorics

A round-robin tournament has $n > 1$ players $P_1, P_2, \dots, P_n$, who each play one game with each other player. Each game results in a win for one player and a loss for the other. If $w_r$ and $l_r$ denote the number of games won and lost, respectively, by $P_r$, prove that $$\sum_{r=1}^{n} w_r^2 = \sum_{r=1}^{n} l_r^2.$$


Lean 4 formalization:
import Mathlib

open EuclideanGeometry Topology Filter Complex

theorem putnam_1965_b2
(n : ℕ)
(hn : n > 1)
(won : Fin n → Fin n → Bool)
(hirrefl : ∀ i : Fin n, won i i = false)
(hantisymm : ∀ i j : Fin n, i ≠ j → won i j = ¬won j i)
(w l : Fin n → ℤ)
(hw : w = fun r : Fin n => ∑ j : Fin n, (if won r j then 1 else 0))
(hl : l = fun r : Fin n => n - 1 - w r)
: ∑ r : Fin n, (w r)^2 = ∑ r : Fin n, (l r)^2 := by
Problem: putnam_1965_b3
Category: algebra, geometry

Prove that there are exactly three right triangles (up to orientation and translation) with integer side lengths and area equal to twice their perimeter.


Lean 4 formalization:
import Mathlib

open EuclideanGeometry Topology Filter Complex

theorem putnam_1965_b3
: {(a, b, c) : ℤ × ℤ × ℤ | a > 0 ∧ a ≤ b ∧ c > 0 ∧ a^2 + b^2 = c^2 ∧ a*b/(2 : ℚ) = 2*(a + b + c)}.ncard = 3 := by
Problem: putnam_1965_b4
Category: algebra, analysis

Let $$f(x, n) = \frac{{n \choose 0} + {n \choose 2}x + {n \choose 4}x^2 + \cdots}{{n \choose 1} + {n \choose 3}x + {n \choose 5}x^2 + \cdots}$$ for all real numbers $x$ and positive integers $n$. Express $f(x, n+1)$ as a rational function involving $f(x, n)$ and $x$, and find $\lim_{n \to \infty} f(x, n)$ for all $x$ for which this limit converges.

Solution: We have $$f(x, n+1) = \frac{f(x, n) + x}{f(x, n) + 1};$$ $\lim_{n \to \infty} f(x, n) = \sqrt{x}$ for all $x \ge 0$ and diverges otherwise.

Lean 4 formalization:
import Mathlib

open EuclideanGeometry Topology Filter Complex

noncomputable abbrev putnam_1965_b4_solution : ((((ℝ → ℝ) → (ℝ → ℝ)) × ((ℝ → ℝ) → (ℝ → ℝ))) × ((Set ℝ) × (ℝ → ℝ))) := sorry
theorem putnam_1965_b4
    (f u v : ℕ → ℝ → ℝ)
    (hu : ∀ n > 0, ∀ x, u n x = ∑ i ∈ Finset.Icc 0 (n / 2), (n.choose (2 * i)) * x ^ i)
    (hv : ∀ n > 0, ∀ x, v n x = ∑ i ∈ Finset.Icc 0 ((n - 1) / 2), (n.choose (2 * i + 1)) * x ^ i)
    (hf : ∀ n > 0, ∀ x, f n x = u n x / v n x)
    (n : ℕ)
    (hn : 0 < n) :
    let ⟨⟨p, q⟩, ⟨s, g⟩⟩ := putnam_1965_b4_solution
    (∀ x, v n x ≠ 0 → v (n + 1) x ≠ 0 → q (f n) x ≠ 0 → f (n + 1) x = p (f n) x / q (f n) x) ∧
    s = {x | ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)} ∧
    ∀ x ∈ s, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x)) := by
Problem: putnam_1965_b5
Category: combinatorics

Prove that, if $4E \le V^2$, there exists a graph with $E$ edges and $V$ vertices with no triangles (cycles of length $3$).


Lean 4 formalization:
import Mathlib

open EuclideanGeometry Topology Filter Complex SimpleGraph.Walk

theorem putnam_1965_b5
{K : Type*}
[Fintype K]
(V E : ℕ)
(hV : V = Nat.card K)
(hE: 4*E ≤ V^2)
: ∃ G : SimpleGraph K, G.edgeSet.ncard = E ∧ ∀ a : K, ∀ w : G.Walk a a, w.length ≠ 3 := by
Problem: putnam_1965_b6
Category: geometry

Let $A$, $B$, $C$, and $D$ be four distinct points for which every circle through $A$ and $B$ intersects every circle through $C$ and $D$. Prove that $A$, $B$, $C$ and $D$ are either collinear (all lying on the same line) or cocyclic (all lying on the same circle).


Lean 4 formalization:
import Mathlib

open EuclideanGeometry Topology Filter Complex SimpleGraph.Walk

theorem putnam_1965_b6
    (A B C D : EuclideanSpace ℝ (Fin 2))
    (S : Set (EuclideanSpace ℝ (Fin 2)))
    (hS : S = {A, B, C, D})
    (hdistinct : S.ncard = 4)
    (through : (ℝ × (EuclideanSpace ℝ (Fin 2))) → (EuclideanSpace ℝ (Fin 2)) → Prop)
    (through_def : through = fun (r, P) => fun Q => dist P Q = r)
    (hABCD : ∀ r s : ℝ, ∀ P Q,
      through (r, P) A ∧ through (r, P) B ∧ through (s, Q) C ∧ through (s, Q) D →
      ∃ I, through (r, P) I ∧ through (s, Q) I) :
    Collinear ℝ S ∨ ∃ r : ℝ, ∃ P, ∀ Q ∈ S, through (r, P) Q := by
Problem: putnam_1966_a1
Category: algebra

Let $a_n$ denote the sequence $0, 1, 1, 2, 2, 3, \dots$, where $a_n = \frac{n}{2}$ if $n$ is even and $\frac{n - 1}{2}$ if n is odd. Furthermore, let $f(n)$ denote the sum of the first $n$ terms of $a_n$. Prove that all positive integers $x$ and $y$ with $x > y$ satisfy $xy = f(x + y) - f(x - y)$.


Lean 4 formalization:
import Mathlib

theorem putnam_1966_a1
(f : ℤ → ℤ)
(hf : f = fun n : ℤ => ∑ m ∈ Finset.Icc 0 n, (if Even m then m / 2 else (m - 1)/2))
: ∀ x y : ℤ, x > 0 ∧ y > 0 ∧ x > y → x * y = f (x + y) - f (x - y) := by
Problem: putnam_1966_a2
Category: geometry

Let $a$, $b$, and $c$ be the side lengths of a triangle with inradius $r$. If $p = \frac{a + b + c}{2}$, show that $$\frac{1}{(p - a)^2} + \frac{1}{(p - b)^2} + \frac{1}{(p - c)^2} \ge \frac{1}{r^2}.$$


Lean 4 formalization:
import Mathlib

theorem putnam_1966_a2
(r : ℝ)
(A B C : EuclideanSpace ℝ (Fin 2))
(hABC : ¬Collinear ℝ {A, B, C})
(a b c p : ℝ)
(ha : a = dist B C)
(hb : b = dist C A)
(hc : c = dist A B)
(hp : p = (dist B C + dist C A + dist A B)/2)
(hr : ∃ I : EuclideanSpace ℝ (Fin 2),
(∃! P : EuclideanSpace ℝ (Fin 2), dist I P = r ∧ Collinear ℝ {P, B, C}) ∧
(∃! Q : EuclideanSpace ℝ (Fin 2), dist I Q = r ∧ Collinear ℝ {Q, C, A}) ∧
(∃! R : EuclideanSpace ℝ (Fin 2), dist I R = r ∧ Collinear ℝ {R, A, B}) ∧
(∀ Z : EuclideanSpace ℝ (Fin 2), dist I Z ≤ r → Z ∈ convexHull ℝ {A, B, C}))
: 1/(p - a)^2 + 1/(p - b)^2 + 1/(p - c)^2 ≥ 1/r^2 := by
Problem: putnam_1966_a3
Category: analysis

If $0 < x_1 < 1$ and $x_{n+1} = x_n(1 - x_n)$ for all $n \ge 1$, prove that $\lim_{n \to \infty} nx_n = 1$.


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_1966_a3
(x : ℕ → ℝ)
(hx1 : 0 < x 1 ∧ x 1 < 1)
(hxi : ∀ n ≥ 1, x (n + 1) = (x n) * (1 - (x n)))
: Tendsto (fun n : ℕ => n * (x n)) atTop (𝓝 1) := by
Problem: putnam_1966_a4
Category: analysis

Prove that the $n$th item in the ascending list of non-perfect-square positive integers equals $n + \{\sqrt{n}\}$, where $\{m\}$ denotes the closest integer to $m$.


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_1966_a4
(a : ℕ → ℤ)
(ha1 : a 1 = 2)
(hai : ∀ n ≥ 1, a (n + 1) = (if ∃ m : ℤ, m^2 = a n + 1 = True then a n + 2 else a n + 1))
: ∀ n ≥ 1, a n = n + round (Real.sqrt n) := by
Problem: putnam_1966_a5
Category: algebra

Let $C$ be the set of continuous functions $f : \mathbb{R} \to \mathbb{R}$. Let $T : C \to C$ satisfty the following two properties:
\begin{enumerate}
\item Linearity: $T(af + bg) = aT(f) + bT(g)$ for all $a, b \in \mathbb{R}$ and all $f, g \in C$.
\item Locality: If $f \in C$ and $g \in C$ are identical on some interval $I$, then $T(f)$ and $T(g)$ are also identical on $I$.
\end{enumerate}
Prove that there exists some function $f \in C$ such that $T(g(x)) = f(x)g(x)$ for all $g \in C$.


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_1966_a5
(C : Set (ℝ → ℝ))
(hC : C = {f : ℝ → ℝ | Continuous f})
(T : (ℝ → ℝ) → (ℝ → ℝ))
(imageTC : ∀ f ∈ C, T f ∈ C)
(linearT : ∀ a b : ℝ, ∀ f ∈ C, ∀ g ∈ C, T ((fun x => a)*f + (fun x => b)*g) = (fun x => a)*(T f) + (fun x => b)*(T g))
(localT : ∀ r s : ℝ, r ≤ s → ∀ f ∈ C, ∀ g ∈ C, (∀ x ∈ Set.Icc r s, f x = g x) → (∀ x ∈ Set.Icc r s, T f x = T g x))
: ∃ f ∈ C, ∀ g ∈ C, T g = f * g := by
Problem: putnam_1966_a6
Category: analysis

Prove that $$\sqrt {1 + 2 \sqrt {1 + 3 \sqrt {1 + 4 \sqrt {1 + 5 \sqrt {\dots}}}}} = 3.$$


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_1966_a6
(a : ℕ → (ℕ → ℝ))
(ha : ∀ n ≥ 1, a n n = n ∧ ∀ m ≥ 1, m < n → a n m = m * Real.sqrt (1 + a n (m + 1)))
: Tendsto (fun n => a n 1) atTop (𝓝 3) := by
Problem: putnam_1966_b1
Category: geometry

If a convex polygon $L$ is contained entirely within a square of side length $1$, prove that the sum of the squares of the side lengths of $L$ is no greater than $4$.


Lean 4 formalization:
import Mathlib

open Topology

theorem putnam_1966_b1
(n : ℕ)
(hn : n ≥ 3)
(L : ZMod n → (EuclideanSpace ℝ (Fin 2)))
(hsq : ∀ i : ZMod n, L i 0 ∈ Set.Icc 0 1 ∧ L i 1 ∈ Set.Icc 0 1)
(hnoncol : ∀ i j k : ZMod n, i ≠ j ∧ j ≠ k ∧ k ≠ i → ¬Collinear ℝ {L i, L j, L k})
(hconvex : ∀ i : ZMod n, segment ℝ (L i) (L (i + 1)) ∩ interior (convexHull ℝ {L j | j : ZMod n}) = ∅)
: ∑ i : Fin n, (dist (L i) (L (i + 1)))^2 ≤ 4 := by
Problem: putnam_1966_b2
Category: number_theory

Prove that, for any ten consecutive integers, at least one is relatively prime to all of the others.


Lean 4 formalization:
import Mathlib

theorem putnam_1966_b2
(S : ℤ → Set ℤ)
(hS : S = fun n : ℤ => {n, n + 1, n + 2, n + 3, n + 4, n + 5, n + 6, n + 7, n + 8, n + 9})
: ∀ n : ℤ, n > 0 → (∃ k ∈ S n, ∀ m ∈ S n, k ≠ m → IsCoprime m k) := by
Problem: putnam_1966_b3
Category: analysis

Let $p_1, p_2, \dots$ be a sequence of positive real numbers. Prove that if $\sum_{n=1}^{\infty} \frac{1}{p_n}$ converges, then $$\sum_{n=1}^{\infty} \frac {n^2 p_n}{(\sum_{i=1}^{n} p_i)^2}$$ also converges.


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_1966_b3
(p : ℕ → ℝ)
(hpos : ∀ n : ℕ, p n > 0)
(hconv : ∃ r : ℝ, Tendsto (fun m : ℕ => ∑ n ∈ Finset.Icc 1 m, 1/(p n)) atTop (𝓝 r))
: ∃ r : ℝ, Tendsto (fun m : ℕ => ∑ n ∈ Finset.Icc 1 m, (p n) * n^2/(∑ i ∈ Finset.Icc 1 n, p i)^2) atTop (𝓝 r) := by
Problem: putnam_1966_b4
Category: number_theory, combinatorics

Let $a_1, a_2, ...$ be an increasing sequence of $mn + 1$ positive integers. Prove that there exists either a subset of $m + 1$ $a_i$ such that no element of the subset divides any other, or a subset of $n + 1$ $a_i$ such that each element of the subset (except the greatest) divides the next greatest element.


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_1966_b4
(m n : ℕ)
(S : Finset ℕ)
(hS : (∀ i ∈ S, i > 0) ∧ S.card = m * n + 1)
: ∃ T ⊆ S, (T.card = m + 1 ∧ ∀ j ∈ T, ∀ i ∈ T, i ≠ j → ¬(j ∣ i)) ∨ (T.card = n + 1 ∧ ∀ i ∈ T, ∀ j ∈ T, j < i → j ∣ i) := by
Problem: putnam_1966_b5
Category: geometry

Prove that any set of $n \ge 3$ distinct points in the Euclidean plane, no three of which are collinear, forms the vertex set of some simple (non-self-intersecting) closed polygon.


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_1966_b5
(S : Finset (EuclideanSpace ℝ (Fin 2)))
(hcard : S.card ≥ 3)
(hS : ∀ s ⊆ S, s.card = 3 → ¬Collinear ℝ s.toSet)
: ∃ L : ZMod S.card → (EuclideanSpace ℝ (Fin 2)), (∀ p ∈ S, ∃! i : ZMod S.card, p = L i) ∧
∀ i j : ZMod S.card, i ≠ j → (∀ I : EuclideanSpace ℝ (Fin 2),
(I ∈ segment ℝ (L i) (L (i + 1)) ∧ I ∈ segment ℝ (L j) (L (j + 1))) →
I = L i ∨ I = L (i + 1) ∨ I = L j ∨ I = L (j + 1)) := by
Problem: putnam_1966_b6
Category: analysis

Prove that any solution $y(x)$ to the differential equation $y'' + e^{x}y = 0$ remains bounded as $x$ goes to $+\infty$.


Lean 4 formalization:
import Mathlib

open Topology Filter

theorem putnam_1966_b6
(y : ℝ → ℝ)
(hy : Differentiable ℝ y ∧ Differentiable ℝ (deriv y))
(diffeq : deriv (deriv y) + Real.exp * y = 0)
: ∃ r s N : ℝ, ∀ x > N, r ≤ y x ∧ y x ≤ s := by
Problem: putnam_1967_a1
Category: analysis

Let $f(x)=a_1\sin x+a_2\sin 2x+\dots+a_n\sin nx$, where $a_1,a_2,\dots,a_n$ are real numbers and where $n$ is a positive integer. Given that $|f(x)| \leq |\sin x|$ for all real $x$, prove that $|a_1|+|2a_2|+\dots+|na_n| \leq 1$.


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_1967_a1
(n : ℕ) (hn : n > 0)
(a : Set.Icc 1 n → ℝ)
(f : ℝ → ℝ)
(hf : f = (fun x : ℝ => ∑ i : Set.Icc 1 n, a i * Real.sin (i * x)))
(flesin : ∀ x : ℝ, abs (f x) ≤ abs (Real.sin x))
: abs (∑ i : Set.Icc 1 n, i * a i) ≤ 1 := by
Problem: putnam_1967_a2
Category: linear_algebra, analysis

Define $S_0$ to be $1$. For $n \geq 1$, let $S_n$ be the number of $n \times n$ matrices whose elements are nonnegative integers with the property that $a_{ij}=a_{ji}$, ($i,j=1,2,\dots,n$) and where $\sum_{i=1}^n a_{ij}=1$, ($j=1,2,\dots,n$). Prove
\begin{enumerate}
\item[(a)] $S_{n+1}=S_n+nS_{n-1}$
\item[(b)] $\sum_{n=0}^\infty S_n\frac{x^n}{n!} = \exp(x+x^2/2)$, where $\exp(x)=e^x$.
\end{enumerate}


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_1967_a2
    (S : ℕ → ℤ)
    (hS0 : S 0 = 1)
    (hSn : ∀ n ≥ 1, S n = {A : Matrix (Fin n) (Fin n) ℕ | (∀ i j, A i j = A j i) ∧ (∀ j, (∑ i, A i j) = 1)}.ncard) :
    (∀ n ≥ 1, S (n + 1) = S n + n * S (n - 1)) ∧
    (∀ x : ℝ, (∑' n : ℕ, S n * (x ^ n / (n)!)) = Real.exp (x + x ^ 2 / 2)) := by
Problem: putnam_1967_a3
Category: algebra

Consider polynomial forms $ax^2-bx+c$ with integer coefficients which have two distinct zeros in the open interval $0<x<1$. Exhibit with a proof the least positive integer value of $a$ for which such a polynomial exists.

Solution: Show that the minimum possible value for $a$ is $5$.

Lean 4 formalization:
import Mathlib

open Polynomial

abbrev putnam_1967_a3_solution : ℕ := sorry
theorem putnam_1967_a3 :
    IsLeast
      {a | ∃ P : Polynomial ℤ,
        P.degree = 2 ∧
        (∃ z1 z2 : Set.Ioo (0 : ℝ) 1, z1 ≠ z2 ∧ aeval (z1 : ℝ) P = 0 ∧ aeval (z2 : ℝ) P = 0) ∧
        P.coeff 2 = a ∧ a > 0}
      putnam_1967_a3_solution := by
Problem: putnam_1967_a4
Category: analysis

Show that if $\lambda > \frac{1}{2}$ there does not exist a real-valued function $u$ such that for all $x$ in the closed interval $0 \leq x \leq 1$, $u(x)=1+\lambda\int_x^1 u(y)u(y-x)\,dy$.


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_1967_a4
(lambda : ℝ)
(hlambda : lambda > 1 / 2)
: ¬∃ u : ℝ → ℝ, MeasureTheory.IntegrableOn u (Set.Icc 0 1) ∧ ∀ x ∈ Set.Icc 0 1, u x = 1 + lambda * (∫ y in Set.Ioo x 1, u y * u (y - x)) := by
Problem: putnam_1967_a5
Category: geometry

Prove that any convex region in the Euclidean plane with area greater than $\pi/4$ contains a pair of points exactly $1$ unit apart.


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_1967_a5
(R : Set (EuclideanSpace ℝ (Fin 2)))
(hR : Convex ℝ R ∧ (MeasureTheory.volume R).toReal > Real.pi / 4)
: ∃ P ∈ R, ∃ Q ∈ R, dist P Q = 1 := by
Problem: putnam_1967_a6
Category: algebra, geometry

Given real numbers $\{a_i\}$ and $\{b_i\}$, ($i=1,2,3,4$), such that $a_1b_2-a_2b_1 \neq 0$. Consider the set of all solutions $(x_1,x_2,x_3,x_4)$ of the simultaneous equations $a_1x_1+a_2x_2+a_3x_3+a_4x_4=0$ and $b_1x_1+b_2x_2+b_3x_3+b_4x_4=0$, for which no $x_i$ ($i=1,2,3,4$) is zero. Each such solution generates a $4$-tuple of plus and minus signs $(\text{signum }x_1,\text{signum }x_2,\text{signum }x_3,\text{signum }x_4)$. Determine, with a proof, the maximum number of distinct $4$-tuples possible.

Solution: Show that the maximum number of distinct $4$-tuples is eight.

Lean 4 formalization:
import Mathlib

open Nat Topology Filter

abbrev putnam_1967_a6_solution : ℕ := sorry
theorem putnam_1967_a6
(abneq0 : (Fin 4 → ℝ) → (Fin 4 → ℝ) → Prop)
(habneq0 : abneq0 = (fun a b : Fin 4 → ℝ => a 0 * b 1 - a 1 * b 0 ≠ 0))
(numtuples : (Fin 4 → ℝ) → (Fin 4 → ℝ) → ℕ)
(hnumtuples : ∀ a b : Fin 4 → ℝ, numtuples a b = {s : Fin 4 → ℝ | ∃ x : Fin 4 → ℝ, (∀ i : Fin 4, x i ≠ 0) ∧ (∑ i : Fin 4, a i * x i) = 0 ∧ (∑ i : Fin 4, b i * x i) = 0 ∧ (∀ i : Fin 4, s i = Real.sign (x i))}.encard)
: (∃ a b : Fin 4 → ℝ, abneq0 a b ∧ numtuples a b = putnam_1967_a6_solution) ∧ (∀ a b : Fin 4 → ℝ, abneq0 a b → numtuples a b ≤ putnam_1967_a6_solution) := by
Problem: putnam_1967_b1
Category: geometry

Let $\hexagon ABCDEF$ be a hexagon inscribed in a circle of radius $r$. If $AB = CD = EF = r$, prove that the midpoints of $\overline{BC}$, $\overline{DE}$, and $\overline{FA}$ form the vertices of an equilateral triangle.


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_1967_b1
(r : ℝ)
(L : ZMod 6 → (EuclideanSpace ℝ (Fin 2)))
(P Q R: EuclideanSpace ℝ (Fin 2))
(hP : P = midpoint ℝ (L 1) (L 2))
(hQ : Q = midpoint ℝ (L 3) (L 4))
(hR : R = midpoint ℝ (L 5) (L 0))
(hr : r > 0)
(hcyclic : ∃ (O : EuclideanSpace ℝ (Fin 2)), ∀ i : ZMod 6, dist O (L i) = r)
(horder : ∀ i j : ZMod 6, i ≠ j → i + 1 = j ∨ i = j + 1 ∨ segment ℝ (L i) (L j) ∩ interior (convexHull ℝ {L k | k : ZMod 6}) ≠ ∅)
(hlens : dist (L 0) (L 1) = r ∧ dist (L 2) (L 3) = r ∧ dist (L 4) (L 5) = r)
(hdist : L 1 ≠ L 2 ∧ L 3 ≠ L 4 ∧ L 5 ≠ L 0)
: dist P Q = dist R P ∧ dist Q R = dist P Q := by
Problem: putnam_1967_b2
Category: algebra

Let $0 \leq p \leq 1$ and $0 \leq r \leq 1$ and consider the identities
\begin{enumerate}
\item[(a)] $(px+(1-p)y)^2=Ax^2+Bxy+Cy^2$,
\item[(b)] $(px+(1-p)y)(rx+(1-r)y)=\alpha x^2+\beta xy+\gamma y^2$.
\end{enumerate}
Show that (with respect to $p$ and $r$)
\begin{enumerate}
\item[(a)] $\max\{A,B,C\} \geq 4/9$,
\item[(b)] $\max\{\alpha,\beta,\gamma\} \geq 4/9$.
\end{enumerate}


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_1967_b2
(p r A B C α β γ : ℝ)
(prbound : 0 ≤ p ∧ p ≤ 1 ∧ 0 ≤ r ∧ r ≤ 1)
(id1 : ∀ x y : ℝ, (p * x + (1 - p) * y) ^ 2 = A * x ^ 2 + B * x * y + C * y ^ 2)
(id2 : ∀ x y : ℝ, (p * x + (1 - p) * y) * (r * x + (1 - r) * y) = α * x ^ 2 + β * x * y + γ * y ^ 2)
: max (max A B) C ≥ 4 / 9 ∧ max (max α β) γ ≥ 4 / 9 := by
Problem: putnam_1967_b3
Category: analysis

If $f$ and $g$ are continuous and periodic functions with period $1$ on the real line, then $\lim_{n \to \infty} \int_0^1 f(x)g(nx)\,dx=(\int_0^1 f(x)\,dx)(\int_0^1 g(x)\,dx)$.


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_1967_b3
(f g : ℝ → ℝ)
(fgcont : Continuous f ∧ Continuous g)
(fgperiod : Function.Periodic f 1 ∧ Function.Periodic g 1)
: Tendsto (fun n : ℤ => ∫ x in Set.Ioo 0 1, f x * g (n * x)) atTop (𝓝 ((∫ x in Set.Ioo 0 1, f x) * (∫ x in Set.Ioo 0 1, g x))) := by
Problem: putnam_1967_b4
Category: number_theory

A certain locker room contains $n$ lockers numbered $1,2,3,\cdots,n$ and all are originally locked. An attendant performs a sequence of operations $T_1,T_2,\cdots,T_n$ whereby with the operation $T_k$, $1 \leq k \leq n$, the condition of being locked or unlocked is changed for all those lockers and only those lockers whose numbers are multiples of $k$. After all the $n$ operations have been performed it is observed that all lockers whose numbers are perfect squares (and only those lockers) are now open or unlocked. Prove this mathematically.


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_1967_b4
(n : ℕ)
(lockers : ℕ → Set.Icc 1 n → Bool)
(npos : n ≥ 1)
(hlockers0 : ∀ i : Set.Icc 1 n, lockers 0 i = false)
(hlockersk : ∀ k ∈ Set.Icc 1 n, ∀ i : Set.Icc 1 n, lockers k i = if k ∣ i then !(lockers (k - 1) i) else (lockers (k - 1) i))
: ∀ i : Set.Icc 1 n, lockers n i ↔ (∃ j : ℤ, j ^ 2 = i) := by
Problem: putnam_1967_b5
Category: algebra

For any positive integer $n$, prove that the sum of the first $n$ terms of the bimonial expansion of $(2 - 1)^{-n}$ (starting with the maximal exponent of $2$) is $\frac{1}{2}.$


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_1967_b5
(n : ℕ)
(hn : n > 0)
: (1 : ℚ)/2 = ∑ i ∈ Finset.range n, (Nat.choose (n + i - 1) i) * (2 : ℚ)^(-(n : ℤ) - i) := by
Problem: putnam_1967_b6
Category: analysis

Let $f$ be a real-valued function having partial derivatives and which is defined for $x^2+y^2 \leq 1$ and is such that $|f(x,y)| \leq 1$. Show that there exists a point $(x_0,y_0)$ in the interior of the unit circle such that $\left(\frac{\partial f}{\partial x} (x_0,y_0)\right)^2+\left(\frac{\partial f}{\partial y} (x_0,y_0)\right)^2 \leq 16$.


Lean 4 formalization:
import Mathlib

open Nat Topology Filter

theorem putnam_1967_b6
(f : ℝ → ℝ → ℝ)
(fdiff : (∀ y : ℝ, Differentiable ℝ (fun x : ℝ => f x y)) ∧ (∀ x : ℝ, Differentiable ℝ (fun y : ℝ => f x y)))
(fcont : ContinuousOn (fun p : ℝ × ℝ => f p.1 p.2) {p : ℝ × ℝ | p.1 ^ 2 + p.2 ^ 2 ≤ 1})
(fbound : ∀ x y : ℝ, (x ^ 2 + y ^ 2 ≤ 1) → |f x y| ≤ 1)
: ∃ x0 y0 : ℝ, (x0 ^ 2 + y0 ^ 2 < 1) ∧ ((deriv (fun x : ℝ => f x y0) x0) ^ 2 + (deriv (fun y : ℝ => f x0 y) y0) ^ 2 ≤ 16) := by
Problem: putnam_1968_a1
Category: analysis

Prove that $$\frac{22}{7} - \pi = \int_{0}^{1} \frac{x^4(1 - x)^4}{1 + x^2} dx$$.


Lean 4 formalization:
import Mathlib

theorem putnam_1968_a1
: 22/7 - Real.pi = ∫ x in (0)..1, x^4 * (1 - x)^4 / (1 + x^2) := by
Problem: putnam_1968_a2
Category: analysis

For all integers $a$, $b$, $c$, $d$, $e$, and $f$ such that $ad \neq bc$ and any real number $\epsilon > 0$, prove that there exist rational numbers $r$ and $s$ such that $$0 < |ra + sb - e| < \varepsilon$$ and $$0 < |rc + sd - f| < \varepsilon.$$


Lean 4 formalization:
import Mathlib

theorem putnam_1968_a2
(a b c d e f : ℤ)
(ε : ℝ)
(hne : a * d ≠ b * c)
(hε : ε > 0)
: ∃ r s : ℚ, (|r * a + s * b - e| : ℝ) ∈ Set.Ioo 0 ε ∧ (|r * c + s * d - f| : ℝ) ∈ Set.Ioo 0 ε := by
Problem: putnam_1968_a3
Category: combinatorics

Let $S$ be a finite set. Prove that there exists a list of subsets of $S$ such that
\begin{enumerate}
\item The first element of the list is the empty set,
\item Each subset of $S$ occurs exactly once in the list, and
\item Each successive element in the list is formed by adding or removing one element from the previous subset in the list.
\end{enumerate}


Lean 4 formalization:
import Mathlib

open Finset symmDiff

theorem putnam_1968_a3
    (α : Type*) [Finite α] :
    ∃ (n : ℕ) (s : Fin (2 ^ n) → Set α),
      s 0 = ∅ ∧
      (∀ t, ∃! i, s i = t) ∧
      (∀ i, i.1 + 1 < 2 ^ n → (s i ∆ s (i + 1)).ncard = 1) := by
Problem: putnam_1968_a4
Category: geometry, algebra

Prove that the sum of the squares of the distances between any $n$ points on the unit sphere $\{(x, y, z) \mid x^2 + y^2 + z^2 = 1\}$ is at most $n^2$.


Lean 4 formalization:
import Mathlib

open Finset

theorem putnam_1968_a4
(n : ℕ)
(S : Fin n → (EuclideanSpace ℝ (Fin 3)))
(hS : ∀ i : Fin n, dist 0 (S i) = 1)
: ∑ i : Fin n, ∑ j : Fin n, (if i < j then (dist (S i) (S j))^2 else (0 : ℝ)) ≤ n^2 := by
Problem: putnam_1968_a5
Category: algebra

Let $V$ be the set of all quadratic polynomials with real coefficients such that $|P(x)| \le 1$ for all $x \in [0, 1]$. Find the supremum of $|P'(0)|$ across all $P \in V$.

Solution: The supremum is $8$.

Lean 4 formalization:
import Mathlib

open Finset Polynomial

abbrev putnam_1968_a5_solution : ℝ := sorry
theorem putnam_1968_a5
(V : Set ℝ[X])
(V_def : V = {P : ℝ[X] | P.degree = 2 ∧ ∀ x ∈ Set.Icc 0 1, |P.eval x| ≤ 1})
: sSup {|(derivative P).eval 0| | P ∈ V} = putnam_1968_a5_solution := by