From 1d20ba611f98416ed172882d1d9c10742ef7ca86 Mon Sep 17 00:00:00 2001
From: Oliver Nash <ddojsioc@google.com>
Date: Tue, 22 Oct 2024 16:08:34 +0000
Subject: [PATCH 1/4] Fix 2020 B5

The error was a simple typo: `<` instead of `=`.
---
 lean4/src/putnam_2020_b5.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean4/src/putnam_2020_b5.lean b/lean4/src/putnam_2020_b5.lean
index 3c8123b4..b5bfa00c 100644
--- a/lean4/src/putnam_2020_b5.lean
+++ b/lean4/src/putnam_2020_b5.lean
@@ -8,7 +8,7 @@ For $j \in \{1, 2, 3, 4\}$, let $z_j$ be a complex number with $|z_j| = 1$ and $
 -/
 theorem putnam_2020_b5
 (z : Fin 4 → ℂ)
-(hzle1 : ∀ n, ‖z n‖ < 1)
+(hzle1 : ∀ n, ‖z n‖ = 1)
 (hzne1 : ∀ n, z n ≠ 1)
 : 3 - z 0 - z 1 - z 2 - z 3 + (z 0) * (z 1) * (z 2) * (z 3) ≠ 0:=
 sorry

From e37a306070cef4dcd202e113410d486322ffce42 Mon Sep 17 00:00:00 2001
From: Oliver Nash <ddojsioc@google.com>
Date: Tue, 22 Oct 2024 16:16:50 +0000
Subject: [PATCH 2/4] Fix 2020 A5
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The problem was that `(a * b : Fin 3 → ℝ)` first coerces `a` and `b`
to vectors and then uses the multiplication on vectors (which is
pointwise multiplication). Thus the group structure declared in `hGgrp`
was completely ignored. This could have been fixed by writing
`(↑(a * b) : Fin 3 → ℝ)` but I think it is much clearer to use an
embedding and not depend upon arcane details Lean's coercion
elaboration.
---
 lean4/src/putnam_2010_a5.lean | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/lean4/src/putnam_2010_a5.lean b/lean4/src/putnam_2010_a5.lean
index 402aa82b..1d58dd8d 100644
--- a/lean4/src/putnam_2010_a5.lean
+++ b/lean4/src/putnam_2010_a5.lean
@@ -1,12 +1,15 @@
 import Mathlib
 open BigOperators
 
+open scoped Matrix
+
 /--
 Let $G$ be a group, with operation $*$. Suppose that \begin{enumerate} \item[(i)] $G$ is a subset of $\mathbb{R}^3$ (but $*$ need not be related to addition of vectors); \item[(ii)] For each $\mathbf{a},\mathbf{b} \in G$, either $\mathbf{a}\times \mathbf{b} = \mathbf{a}*\mathbf{b}$ or $\mathbf{a}\times \mathbf{b} = 0$ (or both), where $\times$ is the usual cross product in $\mathbb{R}^3$. \end{enumerate} Prove that $\mathbf{a} \times \mathbf{b} = 0$ for all $\mathbf{a}, \mathbf{b} \in G$.
 -/
 theorem putnam_2010_a5
-(G : Set (Fin 3 → ℝ))
-(hGgrp : Group G)
-(hGcross : ∀ a b : G, crossProduct a b = (a * b : Fin 3 → ℝ) ∨ crossProduct (a : Fin 3 → ℝ) b = 0)
-: ∀ a b : G, crossProduct (a : Fin 3 → ℝ) b = 0 :=
-sorry
+    (G : Type*) [Group G]
+    (i : G ↪ (Fin 3 → ℝ))
+    (h : ∀ a b, (i a) ×₃ (i b) = i (a * b) ∨ (i a) ×₃ (i b) = 0)
+    (a b : G) :
+    (i a) ×₃ (i b) = 0 :=
+  sorry

From fac23f27d5711e6406565cd74069f2263e30699e Mon Sep 17 00:00:00 2001
From: Oliver Nash <ddojsioc@google.com>
Date: Tue, 22 Oct 2024 17:06:24 +0000
Subject: [PATCH 3/4] Fix 1994 B3

This is a slightly subjective fix. The issue is that `f > 0` does not
mean that `f` is positive everywhere; it means that `f` is non-negative
everywhere and positive at at least one point. I believe this is what is
intended in the informal statement.

The issue is slightly confounded by the fact that if for all `x`,
`deriv f x > f x` and `f x` is non-negative then the derivative is
strictly positive, and thus `f` is strictly monotone, and thus being
non-negative implies being strictly positive everywhere.

So there is no mathematical change to the meaning here but I think this
is a more faithful representation of the question. It should also be
noted that the fact that there is no mathematical change depends upon
not-quite-totally-trivial facts.

I have also taken the opportunity to rewrite question with slightly
improved style.
---
 lean4/src/putnam_1994_b3.lean | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/lean4/src/putnam_1994_b3.lean b/lean4/src/putnam_1994_b3.lean
index ec69120f..be9f6068 100644
--- a/lean4/src/putnam_1994_b3.lean
+++ b/lean4/src/putnam_1994_b3.lean
@@ -8,9 +8,7 @@ abbrev putnam_1994_b3_solution : Set ℝ := sorry
 /--
 Find the set of all real numbers $k$ with the following property: For any positive, differentiable function $f$ that satisfies $f'(x)>f(x)$ for all $x$, there is some number $N$ such that $f(x)>e^{kx}$ for all $x>N$.
 -/
-theorem putnam_1994_b3
-(k : ℝ)
-(allfexN : Prop)
-(hallfexN : allfexN = ∀ f : ℝ → ℝ, (f > 0 ∧ Differentiable ℝ f ∧ ∀ x : ℝ, deriv f x > f x) → (∃ N : ℝ, ∀ x > N, f x > Real.exp (k * x)))
-: allfexN ↔ k ∈ putnam_1994_b3_solution :=
-sorry
+theorem putnam_1994_b3 :
+    {k | ∀ f (hf : (∀ x, 0 < f x ∧ f x < deriv f x) ∧ Differentiable ℝ f),
+      ∃ N, ∀ x > N, Real.exp (k * x) < f x} = putnam_1994_b3_solution :=
+  sorry

From 958aaea2c451eda62de72339236ee6459df24550 Mon Sep 17 00:00:00 2001
From: Oliver Nash <ddojsioc@google.com>
Date: Tue, 22 Oct 2024 17:16:47 +0000
Subject: [PATCH 4/4] Fix 1994 A1

The statement should be that the sum diverges, rather than that it has
no finite limit (even though these are easily equivalent given the
latent positivity hypotheses).
---
 lean4/src/putnam_1994_a1.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/lean4/src/putnam_1994_a1.lean b/lean4/src/putnam_1994_a1.lean
index 99884791..7a7f0a8c 100644
--- a/lean4/src/putnam_1994_a1.lean
+++ b/lean4/src/putnam_1994_a1.lean
@@ -7,7 +7,7 @@ open Filter Topology
 Suppose that a sequence $a_1,a_2,a_3,\dots$ satisfies $0<a_n \leq a_{2n}+a_{2n+1}$ for all $n \geq 1$. Prove that the series $\sum_{n=1}^\infty a_n$ diverges.
 -/
 theorem putnam_1994_a1
-(a : ℕ → ℝ)
-(ha : ∀ n ≥ 1, 0 < a n ∧ a n ≤ a (2 * n) + a (2 * n + 1))
-: ¬(∃ s : ℝ, Tendsto (fun N : ℕ => ∑ n : Set.Icc 1 N, a n) atTop (𝓝 s)) :=
-sorry
+    (a : ℕ → ℝ)
+    (ha : ∀ n ≥ 1, 0 < a n ∧ a n ≤ a (2 * n) + a (2 * n + 1)) :
+    Tendsto (fun N : ℕ => ∑ n : Set.Icc 1 N, a n) atTop atTop :=
+  sorry