Clean formalizations.

coq/src/putnam_1980_a5.v

@@ -14,5 +14,5 @@ Definition mu := [the measure _ _ of @lebesgue_measure R].
 Theorem putnam_1980_a5
     (P : {poly R})
     (Pnonconst : gtn (size P) (1%nat))
-    : finite_set [set x : R | \int[mu]_(t in [set t : R | 0 <= t <= x]) (fun x => P.[x] * (sin x)) t = 0 /\ \int[mu]_(t in [set t : R | 0 <= t <= x]) (fun x => P.[x] * (cos x)) t = 0].
+    : finite_set [set x : R | \int[mu]_(t in [set t : R | 0 <= t <= x]) (fun y => P.[y] * (sin y)) t = 0 /\ \int[mu]_(t in [set t : R | 0 <= t <= x]) (fun y => P.[y] * (cos y)) t = 0].
 Proof. Admitted.

coq/src/putnam_2006_b2.v

@@ -1,10 +1,19 @@
-Require Import List Reals Coquelicot.Coquelicot.
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Open Scope ring_scope.
+
+Variable R : realType.
 Theorem putnam_2006_b2
     (n : nat)
-    (npos : gt n 0)
-    (X : list R)
-    (hXcard : length X = n)
-    : exists (presS: R -> Prop) (m: Z) (S: list R), 
-    (neq (length S) 0) /\ NoDup S /\ (forall (x: R), In x S <-> (In x X /\ presS x)) /\
-    (Rabs (IZR m + (fold_left Rplus S 0)) <= 1 / INR (n + 1)).
-Proof. Admitted.
+    (hn : gt n 0)
+    (X : seq R)
+    (hX : uniq X /\ size X = n)
+    : exists S : seq R, subseq S X /\
+        size S <> 0%nat /\
+        (exists m : int, `|m%:~R + \sum_(s <- S) s| <= 1 / (n%:R + 1)).
+Proof. Admitted.

lean4/src/putnam_2018_b1.lean

@@ -1,20 +1,17 @@
 import Mathlib
-open BigOperators
 
 abbrev putnam_2018_b1_solution : Set (Mathlib.Vector ℤ 2) := sorry
 -- {v : Mathlib.Vector ℤ 2 | ∃ b : ℤ, 0 ≤ b ∧ b ≤ 100 ∧ Even b ∧ v.toList = [1, b]}
 /--
 Let $\mathcal{P}$ be the set of vectors defined by $\mathcal{P}=\left\{\left.\begin{pmatrix} a \\ b \end{pmatrix}\right| 0 \leq a \leq 2, 0 \leq b \leq 100,\text{ and }a,b \in \mathbb{Z}\right\}$. Find all $\mathbf{v} \in \mathcal{P}$ such that the set $\mathcal{P} \setminus \{\mathbf{v}\}$ obtained by omitting vector $\mathbf{v}$ from $\mathcal{P}$ can be partitioned into two sets of equal size and equal sum.
 -/
 theorem putnam_2018_b1
-(P : Finset (Mathlib.Vector ℤ 2))
+(P Pvdiff : Finset (Mathlib.Vector ℤ 2))
 (v : Mathlib.Vector ℤ 2)
-(vinP : Prop)
-(Pvdiff : Finset (Mathlib.Vector ℤ 2))
-(Pvpart : Prop)
 (hP : P = {v' : Mathlib.Vector ℤ 2 | 0 ≤ v'[0] ∧ v'[0] ≤ 2 ∧ 0 ≤ v'[1] ∧ v'[1] ≤ 100})
-(hvinP : vinP = (v ∈ P))
 (hPvdiff : Pvdiff = P \ ({v} : Finset (Mathlib.Vector ℤ 2)))
-(hPvpart : Pvpart = (∃ Q R : Finset (Mathlib.Vector ℤ 2), (Q ∪ R = Pvdiff) ∧ (Q ∩ R = ∅) ∧ (Q.card = R.card) ∧ (∑ q in Q, q[0] = ∑ r in R, r[0]) ∧ (∑ q in Q, q[1] = ∑ r in R, r[1])))
-: (vinP ∧ Pvpart) ↔ v ∈ putnam_2018_b1_solution :=
+: (v ∈ P ∧ (∃ Q R : Finset (Mathlib.Vector ℤ 2),
+    (Q ∪ R = Pvdiff) ∧ (Q ∩ R = ∅) ∧ (Q.card = R.card) ∧
+    (∑ q in Q, q[0] = ∑ r in R, r[0]) ∧ (∑ q in Q, q[1] = ∑ r in R, r[1])))
+  ↔ v ∈ putnam_2018_b1_solution :=
 sorry