Improve readability.

coq/src/putnam_1994_b3.v

@@ -1,6 +1,18 @@
-Require Import Reals Coquelicot.Coquelicot.
-Open Scope R.
-Definition putnam_1994_b3_solution (k: R) := k < 1.
-Theorem putnam_1994_b3
-    : forall k : R, (forall f : R -> R, (forall x : R, f x > 0 /\ ex_derive f x /\ (Derive f) x > f x) -> exists N : R, forall x : R, x > N -> f x > exp (k * x)) <-> putnam_1994_b3_solution k.
-Proof. Admitted.
+From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import reals normedtype derive topology sequences.
+From mathcomp Require Import classical_sets.
+Import numFieldNormedType.Exports.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+Local Open Scope classical_set_scope.
+
+Variable R : realType.
+Definition putnam_1993_b3_solution : set R := [set k | k < 1].
+Theorem putnam_1993_b3
+    : [set k | forall f (hf : forall x, differentiable f x /\ 0 < f x < f^`() x),
+        exists N : R, forall x, N < x -> expR (k * x) < f x] = putnam_1993_b3_solution.
+Proof. Admitted.

lean4/src/putnam_1963_b3.lean

@@ -8,8 +8,8 @@ abbrev putnam_1963_b3_solution : Set (ℝ → ℝ) := sorry
 Find every twice-differentiable real-valued function $f$ with domain the set of all real numbers and satisfying the functional equation $(f(x))^2-(f(y))^2=f(x+y)f(x-y)$ for all real numbers $x$ and $y$.
 -/
 theorem putnam_1963_b3
-(f : ℝ → ℝ)
-(fdiff : Prop)
-(hfdiff : fdiff ↔ ContDiff ℝ 1 f ∧ Differentiable ℝ (deriv f))
-: (fdiff ∧ ∀ x y : ℝ, (f x) ^ 2 - (f y) ^ 2 = f (x + y) * f (x - y)) ↔ f ∈ putnam_1963_b3_solution :=
-sorry
+    (f : ℝ → ℝ) :
+    f ∈ putnam_1963_b3_solution ↔
+      (ContDiff ℝ 1 f ∧ Differentiable ℝ (deriv f) ∧
+      ∀ x y : ℝ, (f x) ^ 2 - (f y) ^ 2 = f (x + y) * f (x - y)) :=
+  sorry

lean4/src/putnam_1964_a5.lean

@@ -9,7 +9,8 @@ Prove that there exists a constant $k$ such that for any sequence $a_i$ of posit
 \]
 -/
 theorem putnam_1964_a5
-(pa : (ℕ → ℝ) → Prop)
-(hpa : pa = fun a ↦ (∀ n : ℕ, a n > 0) ∧ ∃ L : ℝ, Tendsto (fun N ↦ ∑ n in Finset.range N, 1 / a n) atTop (𝓝 L))
-: (∃ k : ℝ, ∀ a : ℕ → ℝ, pa a → ∑' n : ℕ, (n + 1) / (∑ i in Finset.range (n + 1), a i) ≤ k * ∑' n : ℕ, 1 / a n) :=
-sorry
+    (pa : (ℕ → ℝ) → Prop)
+    (hpa : ∀ a, pa a ↔ (∀ n : ℕ, a n > 0) ∧ ∃ L : ℝ, Tendsto (fun N ↦ ∑ n in Finset.range N, 1 / a n) atTop (𝓝 L)) :
+    ∃ k : ℝ, ∀ a : ℕ → ℝ, pa a →
+      ∑' n : ℕ, (n + 1) / (∑ i in Finset.range (n + 1), a i) ≤ k * ∑' n : ℕ, 1 / a n :=
+  sorry

lean4/src/putnam_1964_b6.lean

@@ -6,9 +6,9 @@ open Set Function Filter Topology
 Let $D$ be the unit disk in the plane. Show that we cannot find congruent sets $A, B$ with $A \cap B = \emptyset$ and $A \cup B = D$.
 -/
 theorem putnam_1964_b6
-(D : Set (EuclideanSpace ℝ (Fin 2)))
-(hD : D = {v : EuclideanSpace ℝ (Fin 2) | dist 0 v ≤ 1})
-(cong : Set (EuclideanSpace ℝ (Fin 2)) → Set (EuclideanSpace ℝ (Fin 2)) → Prop)
-(hcong : cong = fun A B ↦ ∃ f : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)), B = f '' A ∧ ∀ v w : EuclideanSpace ℝ (Fin 2), dist v w = dist (f v) (f w))
-: (¬∃ A B : Set (Fin 2 → ℝ), cong A B ∧ A ∩ B = ∅ ∧ A ∪ B = D) :=
-sorry
+    (D : Set (EuclideanSpace ℝ (Fin 2)))
+    (hD : D = {v : EuclideanSpace ℝ (Fin 2) | dist 0 v ≤ 1})
+    (cong : Set (EuclideanSpace ℝ (Fin 2)) → Set (EuclideanSpace ℝ (Fin 2)) → Prop)
+    (hcong : ∀ A B, cong A B ↔ ∃ f : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)), B = f '' A ∧ ∀ v w : EuclideanSpace ℝ (Fin 2), dist v w = dist (f v) (f w))
+    : (¬∃ A B : Set (Fin 2 → ℝ), cong A B ∧ A ∩ B = ∅ ∧ A ∪ B = D) :=
+  sorry

lean4/src/putnam_1965_b6.lean

@@ -6,13 +6,14 @@ open EuclideanGeometry Topology Filter Complex SimpleGraph.Walk
 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).
 -/
 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 : EuclideanSpace ℝ (Fin 2), through (r, P) A ∧ through (r, P) B ∧ through (s, Q) C ∧ through (s, Q) D →
-∃ I : EuclideanSpace ℝ (Fin 2), through (r, P) I ∧ through (s, Q) I)
-: Collinear ℝ S ∨ ∃ r : ℝ, ∃ P : EuclideanSpace ℝ (Fin 2), ∀ Q ∈ S, through (r, P) Q :=
-sorry
+    (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 :=
+  sorry

lean4/src/putnam_1967_a1.lean

@@ -6,11 +6,10 @@ open Nat Topology Filter
 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$.
 -/
 theorem putnam_1967_a1
-(n : ℕ)
+(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)))
-(npos : n > 0)
 (flesin : ∀ x : ℝ, abs (f x) ≤ abs (Real.sin x))
 : abs (∑ i : Set.Icc 1 n, i * a i) ≤ 1 :=
 sorry

lean4/src/putnam_1967_a2.lean

@@ -10,8 +10,9 @@ Define $S_0$ to be $1$. For $n \geq 1$, let $S_n$ be the number of $n \times n$
 \end{enumerate}
 -/
 theorem putnam_1967_a2
-(S : ℕ → ℤ)
-(hS0 : S 0 = 1)
-(hSn : ∀ n ≥ 1, S n = {A : Matrix (Fin n) (Fin n) ℕ | (∀ i j : Fin n, A i j = A j i) ∧ (∀ j : Fin n, (∑ i : Fin n, 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)) :=
-sorry
+    (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)) :=
+  sorry

lean4/src/putnam_1967_a3.lean

@@ -1,16 +1,17 @@
 import Mathlib
 
-open Nat Topology Filter
+open Polynomial
 
 abbrev putnam_1967_a3_solution : ℕ := sorry
 -- 5
 /--
 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.
 -/
-theorem putnam_1967_a3
-(pform pzeros pall : Polynomial ℝ → Prop)
-(hpform : ∀ p : Polynomial ℝ, pform p ↔ p.degree = 2 ∧ ∀ i ∈ Finset.range 3, p.coeff i = round (p.coeff i))
-(hpzeros : ∀ p, pzeros p ↔ ∃ z1 z2 : Set.Ioo (0 : ℝ) 1, z1 ≠ z2 ∧ p.eval z1.1 = 0 ∧ p.eval z2.1 = 0)
-(hpall : ∀ p, pall p ↔ pform p ∧ pzeros p ∧ p.coeff 2 > 0)
-: (∃ p : Polynomial ℝ, pall p ∧ p.coeff 2 = putnam_1967_a3_solution) ∧ (∀ p : Polynomial ℝ, pall p → p.coeff 2 ≥ 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 :=
+  sorry

lean4/src/putnam_1970_a4.lean

@@ -7,6 +7,6 @@ Suppose $(x_n)$ is a sequence such that $\lim_{n \to \infty} (x_n - x_{n-2} = 0$
 -/
 theorem putnam_1970_a4
 (x : ℕ → ℝ)
-(hxlim : Tendsto (fun n => x n - x (n-2)) atTop (𝓝 0))
-: Tendsto (fun n => (x n - x (n-1))/n) atTop (𝓝 0) :=
+(hxlim : Tendsto (fun n => x (n+2) - x n) atTop (𝓝 0))
+: Tendsto (fun n => (x (n+1) - x (n))/(n+1)) atTop (𝓝 0) :=
 sorry

lean4/src/putnam_1971_a2.lean

@@ -8,5 +8,6 @@ abbrev putnam_1971_a2_solution : Set (Polynomial ℝ) := sorry
 Determine all polynomials $P(x)$ such that $P(x^2 + 1) = (P(x))^2 + 1$ and $P(0) = 0$.
 -/
 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 :=
-sorry
+    (P : Polynomial ℝ) :
+    (P.eval 0 = 0 ∧ (∀ x : ℝ, P.eval (x^2 + 1) = (P.eval x)^2 + 1)) ↔ P ∈ putnam_1971_a2_solution :=
+  sorry

lean4/src/putnam_1971_a3.lean

@@ -6,13 +6,14 @@ open Set
 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$.
 -/
 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)
-(oncircle : (ℝ × ℝ) → ℝ → (ℝ × ℝ) → Prop)
-(oncircle_def : oncircle = fun (C : ℝ × ℝ) (r : ℝ) (p : ℝ × ℝ) => Real.sqrt ((p.1 - C.1)^2 + (p.2 - C.2)^2) = r)
-(hcircle : ∃ C : ℝ × ℝ, oncircle C R a ∧ oncircle C R b ∧ oncircle C R c)
-: (Real.sqrt ((a.1 - b.1)^2 + (a.2 - b.2)^2)) * (Real.sqrt ((a.1 - c.1)^2 + (a.2 - c.2)^2)) * (Real.sqrt ((b.1 - c.1)^2 + (b.2 - c.2)^2)) ≥ 2 * R :=
-sorry
+    (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 :=
+  sorry

lean4/src/putnam_1971_a5.lean

@@ -8,9 +8,11 @@ abbrev putnam_1971_a5_solution : ℤ × ℤ := sorry
 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$.
 -/
 theorem putnam_1971_a5
-(a b : ℤ)
-(hab : a > 0 ∧ b > 0 ∧ a > b)
-(pab : ℤ → ℤ → Prop)
-(hpab : pab = fun 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 :=
-sorry
+    (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 :=
+  sorry

lean4/src/putnam_1972_a1.lean

@@ -6,9 +6,8 @@ open EuclideanGeometry Filter Topology Set
 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.
 -/
 theorem putnam_1972_a1
-(n : ℕ)
-(hn : n > 0)
-(fourAP : ℤ → ℤ → ℤ → ℤ → Prop)
-(hfourAP : fourAP = fun 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)) :=
-sorry
+    (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)) :=
+  sorry

lean4/src/putnam_1972_a3.lean

@@ -9,9 +9,9 @@ abbrev putnam_1972_a3_solution : Set (ℝ → ℝ) := sorry
 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]$.
 -/
 theorem putnam_1972_a3
-(climit_exists : (ℕ → ℝ) → Prop)
-(hclimit_exists : climit_exists = fun x => ∃ C : ℝ, Tendsto (fun n => (∑ i in Finset.range n, (x i))/(n : ℝ)) atTop (𝓝 C))
-(supercontinuous : (ℝ → ℝ) → Prop)
-(hsupercontinuous : supercontinuous = fun 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 :=
-sorry
+    (climit_exists : (ℕ → ℝ) → Prop)
+    (supercontinuous : (ℝ → ℝ) → Prop)
+    (hclimit_exists : ∀ x, climit_exists x ↔ ∃ C : ℝ, Tendsto (fun n => (∑ i in 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 :=
+  sorry

lean4/src/putnam_1972_b2.lean

@@ -8,13 +8,13 @@ noncomputable abbrev putnam_1972_b2_solution : ℝ → ℝ → ℝ := sorry
 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$.
 -/
 theorem putnam_1972_b2
-(s v : ℝ)
-(hs : s > 0)
-(hv : v > 0)
-(valid : ℝ → (ℝ → ℝ) → Prop)
-(hvalid : valid = fun (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)
-: (∃ x : ℝ → ℝ, valid (putnam_1972_b2_solution s v) x) ∧
-∀ t > putnam_1972_b2_solution s v, ¬(∃ x : ℝ → ℝ, valid t x) :=
-sorry
+    (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) :=
+  sorry

lean4/src/putnam_1974_a1.lean

@@ -8,7 +8,7 @@ abbrev putnam_1974_a1_solution : ℕ := sorry
 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?
 -/
 theorem putnam_1974_a1
-(conspiratorial : Set ℤ → Prop)
-(hconspiratorial : conspiratorial = fun 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)))
-: (∀ S : Set ℤ, S ⊆ Icc 1 16 → conspiratorial S → S.encard ≤ putnam_1974_a1_solution) ∧ (∃ S : Set ℤ, S ⊆ Icc 1 16 ∧ conspiratorial S ∧ S.encard = putnam_1974_a1_solution) :=
-sorry
+    (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 :=
+  sorry

lean4/src/putnam_1976_b6.lean

@@ -9,6 +9,6 @@ theorem putnam_1976_b6
 (σ : ℕ → ℤ)
 (hσ : σ = fun N : ℕ => ∑ d in Nat.divisors N, (d : ℤ))
 (quasiperfect : ℕ → Prop)
-(quasiperfect_def : quasiperfect = fun N : ℕ => σ N = 2*N + 1)
+(quasiperfect_def : ∀ N, quasiperfect N ↔ σ N = 2*N + 1)
 : ∀ N : ℕ, quasiperfect N → ∃ m : ℤ, Odd m ∧ m^2 = N :=
 sorry

lean4/src/putnam_1977_a2.lean

@@ -5,6 +5,7 @@ abbrev putnam_1977_a2_solution : ℝ → ℝ → ℝ → ℝ → Prop := sorry
 /--
 Find all real solutions $(a, b, c, d)$ to the equations $a + b + c = d$, $\frac{1}{a} + \frac{1}{b} + \frac{1}{c} = \frac{1}{d}$.
 -/
-theorem putnam_1977_a2
-: (∀ a b c d : ℝ, a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 → ((a + b + c = d ∧ 1 / a + 1 / b + 1 / c = 1 / d) ↔ putnam_1977_a2_solution a b c d)) :=
-sorry
+theorem putnam_1977_a2 :
+    ∀ a b c d : ℝ, putnam_1977_a2_solution a b c d ↔
+      a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 → (a + b + c = d ∧ 1 / a + 1 / b + 1 / c = 1 / d) :=
+  sorry

lean4/src/putnam_1977_a4.lean

@@ -7,6 +7,7 @@ noncomputable abbrev putnam_1977_a4_solution : RatFunc ℝ := sorry
 /--
 Find $\sum_{n=0}^{\infty} \frac{x^{2^n}}{1 - x^{2^{n+1}}}$ as a rational function of $x$ for $x \in (0, 1)$.
 -/
-theorem putnam_1977_a4
-: (∀ x ∈ Ioo 0 1, putnam_1977_a4_solution.eval (id ℝ) x = ∑' n : ℕ, x ^ 2 ^ n / (1 - x ^ 2 ^ (n + 1))) :=
-sorry
+theorem putnam_1977_a4 :
+    ∀ x ∈ Ioo 0 1,
+      putnam_1977_a4_solution.eval (id ℝ) x = ∑' n : ℕ, x ^ 2 ^ n / (1 - x ^ 2 ^ (n + 1)) :=
+  sorry

lean4/src/putnam_1978_a3.lean

@@ -12,9 +12,9 @@ I_k = \int_0^{\infty} \frac{x^k}{p(x)} \, dx.
 For which $k$ is $I_k$ smallest?
 -/
 theorem putnam_1978_a3
-(p : Polynomial ℝ)
-(hp : p = 2 * (X ^ 6 + 1) + 4 * (X ^ 5 + X) + 3 * (X ^ 4 + X ^ 2) + 5 * X ^ 3)
-(I : ℕ → ℝ)
-(hI : I = fun k ↦ ∫ x in Ioi 0, x ^ k / p.eval x)
-: (putnam_1978_a3_solution ∈ Ioo 0 5 ∧ ∀ k ∈ Ioo 0 5, I putnam_1978_a3_solution ≤ I k) :=
-sorry
+    (p : Polynomial ℝ)
+    (hp : p = 2 * (X ^ 6 + 1) + 4 * (X ^ 5 + X) + 3 * (X ^ 4 + X ^ 2) + 5 * X ^ 3)
+    (I : ℕ → ℝ)
+    (hI : I = fun k ↦ ∫ x in Ioi 0, x ^ k / p.eval x) :
+    IsLeast {y | ∃ k ∈ Ioo 0 5, I k = y} putnam_1978_a3_solution :=
+  sorry

lean4/src/putnam_1978_b4.lean

@@ -5,6 +5,9 @@ open Set Real Filter Topology Polynomial
 /--
 Show that we can find integers $a, b, c, d$ such that $a^2 + b^2 + c^2 + d^2 = abc + abd + acd + bcd$, and the smallest of $a, b, c, d$ is arbitrarily large.
 -/
-theorem putnam_1978_b4
-: (∀ N : ℝ, ∃ a b c d : ℤ, a > N ∧ b > N ∧ c > N ∧ d > N ∧ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = a * b * c + a * b * d + a * c * d + b * c * d) :=
+theorem putnam_1978_b4 :
+  ∀ N : ℝ,
+    ∃ a b c d : ℤ,
+      a > N ∧ b > N ∧ c > N ∧ d > N ∧
+      a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = a * b * c + a * b * d + a * c * d + b * c * d :=
 sorry

lean4/src/putnam_1979_a1.lean

@@ -6,7 +6,7 @@ abbrev putnam_1979_a1_solution : Multiset ℕ := sorry
 For which positive integers $n$ and $a_1, a_2, \dots, a_n$ with $\sum_{i = 1}^{n} a_i = 1979$ does $\prod_{i = 1}^{n} a_i$ attain the greatest value?
 -/
 theorem putnam_1979_a1
-(P : Multiset ℕ → Prop)
-(hP : P = fun a => Multiset.card a > 0 ∧ (∀ i ∈ a, i > 0) ∧ a.sum = 1979)
-: P putnam_1979_a1_solution ∧ ∀ a : Multiset ℕ, P a → putnam_1979_a1_solution.prod ≥ a.prod :=
-sorry
+    (P : Multiset ℕ → Prop)
+    (hP : ∀ a, P a ↔ Multiset.card a > 0 ∧ (∀ i ∈ a, i > 0) ∧ a.sum = 1979) :
+    P putnam_1979_a1_solution ∧ ∀ a : Multiset ℕ, P a → putnam_1979_a1_solution.prod ≥ a.prod :=
+  sorry