Fixed statements for 15 problems.

lean4/src/putnam_1963_a6.lean

@@ -11,14 +11,16 @@ theorem putnam_1963_a6
 (E : Set (EuclideanSpace ℝ (Fin 2)))
 (hE : E = {H : EuclideanSpace ℝ (Fin 2) | dist F1 H + dist F2 H = r})
 (M : EuclideanSpace ℝ (Fin 2))
-(hM : M = midpoint ℝ U V)
+(hMuv : M = midpoint ℝ U V)
 (hr : r > dist F1 F2)
 (hUV : U ∈ E ∧ V ∈ E ∧ U ≠ V)
 (hAB : A ∈ E ∧ B ∈ E ∧ A ≠ B)
 (hCD : C ∈ E ∧ D ∈ E ∧ C ≠ D)
+(hAC : A ≠ C)
+(hBD : B ≠ D)
 (hdistinct : segment ℝ A B ≠ segment ℝ U V ∧ segment ℝ C D ≠ segment ℝ U V ∧ segment ℝ A B ≠ segment ℝ C D)
 (hM : M ∈ segment ℝ A B ∧ M ∈ segment ℝ C D)
 (hP : Collinear ℝ {P, A, C} ∧ Collinear ℝ {P, U, V})
-(hQ : Collinear ℝ {P, B, D} ∧ Collinear ℝ {Q, U, V})
+(hQ : Collinear ℝ {Q, B, D} ∧ Collinear ℝ {Q, U, V})
 : M = midpoint ℝ P Q :=
 sorry

lean4/src/putnam_1964_b4.lean

@@ -19,6 +19,7 @@ theorem putnam_1964_b4
     (hv : ∀ i, C i = Metric.sphere 0 1 ∩ {x : EuclideanSpace ℝ (Fin 3) | ⟪v i, x⟫_ℝ = 0 })
     --all the `v_i`'s are non-zero
     (hv' : ∀ i, v i ≠ 0)
+    (hCinj : Function.Injective C)
     -- The circles in `C` are in general position
     (hT₂ : ∀ᵉ (x ∈ Metric.sphere 0 1) (y ∈ Metric.sphere 0 1),
       (Finset.univ.filter (fun i => {x, y} ⊆ (C i))).card ≤ 2)

lean4/src/putnam_1977_a2.lean

@@ -6,6 +6,8 @@ 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 : ℝ, 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) :=
+    ∀ a b c d : ℝ,
+      a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 →
+        (putnam_1977_a2_solution a b c d ↔
+          (a + b + c = d ∧ 1 / a + 1 / b + 1 / c = 1 / d)) :=
   sorry

lean4/src/putnam_1977_b6.lean

@@ -9,6 +9,7 @@ theorem putnam_1977_b6
 {G : Type*}
 [Group G]
 (H : Subgroup G)
+[Finite H]
 (h : ℕ)
 (h_def : h = Nat.card H)
 (a : G)

lean4/src/putnam_1980_a4.lean

@@ -8,7 +8,7 @@ import Mathlib
 -/
 theorem putnam_1980_a4
     (abcvals : ℤ → ℤ → ℤ → Prop)
-    (habcvals : ∀ a b c : ℤ, abcvals a b c ↔ (a = 0 ∧ b = 0 ∧ c = 0) ∧ |a| < 1000000 ∧ |b| < 1000000 ∧ |c| < 1000000) :
+    (habcvals : ∀ a b c : ℤ, abcvals a b c ↔ ¬(a = 0 ∧ b = 0 ∧ c = 0) ∧ |a| < 1000000 ∧ |b| < 1000000 ∧ |c| < 1000000) :
     (∃ a b c : ℤ,
       abcvals a b c ∧
       |a + b * Real.sqrt 2 + c * Real.sqrt 3| < 10 ^ (-(11 : ℝ))) ∧

lean4/src/putnam_1989_b6.lean

@@ -13,7 +13,7 @@ theorem putnam_1989_b6
     (X : Set (Fin n → ℝ))
     (X_def : ∀ x, x ∈ X ↔ 0 < x 0 ∧ x (-1) < 1 ∧ StrictMono x)
     (S : (ℝ → ℝ) → (Fin (n + 2) → ℝ) → ℝ)
-    (S_def : ∀ f x, S f x = ∑ i : Fin n.succ, (x i.succ - x i.castSucc) * f (i + 1)) :
+    (S_def : ∀ f x, S f x = ∑ i : Fin n.succ, (x i.succ - x i.castSucc) * f (x i.succ)) :
     ∃ P : Polynomial ℝ,
       P.degree = n ∧
       (∀ t ∈ Icc 0 1, P.eval t ∈ Icc 0 1) ∧

lean4/src/putnam_1997_a5.lean

@@ -9,6 +9,6 @@ Let $N_n$ denote the number of ordered $n$-tuples of positive integers $(a_1,a_2
 -/
 theorem putnam_1997_a5
 (N : (n : ℕ+) → Set (Fin n → ℕ+))
-(hN : N = fun (n : ℕ+) => {t : Fin n → ℕ+ | (∀ i j : Fin n, i < j → t i <= t j) ∧ (∑ i : Fin n, (1 : ℝ)/(t i) = 1) })
+(hN : N = fun (n : ℕ+) => {t : Fin n → ℕ+ | (∑ i : Fin n, (1 : ℝ)/(t i) = 1) })
 : Odd (N 10).ncard ↔ putnam_1997_a5_solution :=
 sorry

lean4/src/putnam_1999_b3.lean

@@ -11,6 +11,6 @@ theorem putnam_1999_b3
 (A : Set (ℝ × ℝ))
 (hA : A = {xy | 0 ≤ xy.1 ∧ xy.1 < 1 ∧ 0 ≤ xy.2 ∧ xy.2 < 1})
 (S : ℝ → ℝ → ℝ)
-(hS : S = fun x y => ∑' m : ℕ, ∑' n : ℕ, if (m > 0 ∧ n > 0 ∧ 1/2 ≤ m/n ∧ m/n ≤ 2) then x^m * y^n else 0)
+(hS : S = fun x y => ∑' m : ℕ, ∑' n : ℕ, if (m > 0 ∧ n > 0 ∧ (1 : ℝ)/2 ≤ (m : ℝ)/n ∧ (m : ℝ)/n ≤ 2) then x^m * y^n else 0)
 : Tendsto (fun xy : (ℝ × ℝ) => (1 - xy.1 * xy.2^2) * (1 - xy.1^2 * xy.2) * (S xy.1 xy.2)) (𝓝[A] ⟨1,1⟩) (𝓝 putnam_1999_b3_solution) :=
 sorry

lean4/src/putnam_2003_a5.lean

@@ -12,7 +12,7 @@ theorem putnam_2003_a5
       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 i = -1) ∧
+      ¬∃ 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 :=

lean4/src/putnam_2003_a6.lean

@@ -10,5 +10,5 @@ For a set $S$ of nonnegative integers, let $r_S(n)$ denote the number of ordered
 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 = ℕ ∧ A ∩ B = ∅ ∧ (∀ n : ℕ, r A n = r B n)) ↔ putnam_2003_a6_solution :=
+: (∃ A B : Set ℕ, A ∪ B = (Set.univ : Set ℕ) ∧ A ∩ B = ∅ ∧ (∀ n : ℕ, r A n = r B n)) ↔ putnam_2003_a6_solution :=
 sorry

lean4/src/putnam_2003_b5.lean

@@ -7,7 +7,7 @@ Let $A,B$, and $C$ be equidistant points on the circumference of a circle of uni
 -/
 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)
+(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)) :=

lean4/src/putnam_2019_a5.lean

@@ -17,6 +17,6 @@ theorem putnam_2019_a5
   (hq : ∀ k : ℕ, q.coeff k = a k)
   (ha0 : a 0 = 0 ∧ ∀ k > p - 1, a k = 0)
   (haother : ∀ k : Set.Icc 1 (p - 1), a k = ((k : ℕ) ^ ((p - 1) / 2)) % p)
-  (hnpoly : ∀ n x, (npoly n).eval x = (x - 1) ^ n) :
+  (hnpoly : ∀ n : ℕ, npoly n = (Polynomial.X - 1) ^ n) :
   IsGreatest {n | npoly n ∣ q} (putnam_2019_a5_solution p) :=
 sorry

lean4/src/putnam_2019_a6.lean

@@ -12,5 +12,5 @@ theorem putnam_2019_a6
 (hdiff : ContDiffOn ℝ 1 g (Set.Ioo 0 1) ∧ DifferentiableOn ℝ (deriv g) (Set.Ioo 0 1))
 (hr : r > 1)
 (hlim : Tendsto (fun x => g x / x ^ r) (𝓝[>] 0) (𝓝 0))
-: (Tendsto (deriv g) (𝓝[>] 0) (𝓝 0)) ∨ (Tendsto (fun x : ℝ => sSup {x' ^ r * abs (iteratedDeriv 2 g x') | x' ∈ Set.Ioc 0 x}) (𝓝[>] 0) atTop) :=
+: (Tendsto (deriv g) (𝓝[>] 0) (𝓝 0)) ∨ (Tendsto (fun x : ℝ => sSup {((x' ^ r * abs (iteratedDeriv 2 g x') : ℝ) : WithTop ℝ) | x' ∈ Set.Ioc 0 x}) (𝓝[>] 0) atTop) :=
 sorry

lean4/src/putnam_2019_b5.lean

@@ -14,5 +14,5 @@ theorem putnam_2019_b5
 (F12 : F 1 = 1 ∧ F 2 = 1)
 (Pdeg: Polynomial.degree P = 1008)
 (hp: ∀ n : ℕ, (n ≤ 1008) → P.eval (2 * n + 1 : ℝ) = F (2 * n + 1))
-: ∀ j k : ℕ, (P.eval 2019 = F j - F k) ↔ ⟨j, k⟩ = putnam_2019_b5_solution  :=
+: ∀ j k : ℕ, (P.eval 2019 = F j - F k ∧ 1 ≤ j ∧ 1 ≤ k) ↔ ⟨j, k⟩ = putnam_2019_b5_solution  :=
 sorry

lean4/src/putnam_2022_a4.lean

@@ -3,7 +3,7 @@ import Mathlib
 open MeasureTheory ProbabilityTheory Classical
 
 abbrev putnam_2022_a4_solution : ℝ := sorry
--- 2*Real.exp (-1/2) - 3
+-- 2*Real.exp ((1 : ℝ) / 2) - 3
 
 /--
 Suppose $X_1, X_2, ...$ real numbers between 0 and 1 that are chosen independently and uniformly at random. Let $S = \sum_{i=1}^k X_i / 2^i $ where $k$ is the least positive integer such that $X_k < X_{k+1}$ or $k = \infty$ if there is no such integer. Find the expected value of $S$
@@ -21,7 +21,7 @@ theorem putnam_2022_a4
     Otherwise, this is `sSup { (Set.Iic m : Set ℕ) | (m : ℕ) } = Set.univ`
     -/
     (hk : ∀ ω, k ω = sSup { s : Set ℕ |
-      ∃ m, s = Set.Iic m ∧ ∀ l ∈ s, X l ω < X (l + 1) ω })
+      ∃ m, s = Set.Iic m ∧ ∀ l, l < m → X l ω > X (l + 1) ω })
     (S : Ω → ℝ)
     (hS : ∀ ω, S ω = ∑' (i : k ω), (X i ω) / (2 ^ (i.val + 1))) :
     ∫ ω, S ω ∂(ℙ : Measure Ω) = putnam_2022_a4_solution := by