Clean some formalizations + fix informal statement

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.

informal/putnam.json

@@ -2854,7 +2854,7 @@
     },
     {
         "problem_name": "putnam_1996_a4",
-        "informal_statement": "Let $S$ be the set of ordered triples $(a, b, c)$ of distinct elements of a finite set $A$. Suppose that \\begin{enumerate} \\item $(a,b,c) \\in S$ if and only if $(b,c,a) \\in S$; \\item $(a,b,c) \\in S$ if and only if $(c,b,a) \\notin S$; \\item $(a,b,c)$ and $(c,d,a)$ are both in $S$ if and only if $(b,c,d)$ and $(d,a,b)$ are both in $S$. \\end{enumerate} Prove that there exists a one-to-one function $g$ from $A$ to $\\R$ such that $g(a) < g(b) < g(c)$ implies $(a,b,c) \\in S$.",
+        "informal_statement": "Let $S$ be a set of ordered triples $(a, b, c)$ of distinct elements of a finite set $A$. Suppose that \\begin{enumerate} \\item $(a,b,c) \\in S$ if and only if $(b,c,a) \\in S$; \\item $(a,b,c) \\in S$ if and only if $(c,b,a) \\notin S$; \\item $(a,b,c)$ and $(c,d,a)$ are both in $S$ if and only if $(b,c,d)$ and $(d,a,b)$ are both in $S$. \\end{enumerate} Prove that there exists a one-to-one function $g$ from $A$ to $\\R$ such that $g(a) < g(b) < g(c)$ implies $(a,b,c) \\in S$.",
         "informal_solution": "None.",
         "tags": [
             "algebra"

lean4/src/putnam_1996_a4.lean

@@ -4,15 +4,15 @@ open BigOperators
 open Function
 
 /--
-Let $S$ be the set of ordered triples $(a, b, c)$ of distinct elements of a finite set $A$. Suppose that \begin{enumerate} \item $(a,b,c) \in S$ if and only if $(b,c,a) \in S$; \item $(a,b,c) \in S$ if and only if $(c,b,a) \notin S$; \item $(a,b,c)$ and $(c,d,a)$ are both in $S$ if and only if $(b,c,d)$ and $(d,a,b)$ are both in $S$. \end{enumerate} Prove that there exists a one-to-one function $g$ from $A$ to $\R$ such that $g(a) < g(b) < g(c)$ implies $(a,b,c) \in S$.
+Let $S$ be a set of ordered triples $(a, b, c)$ of distinct elements of a finite set $A$. Suppose that \begin{enumerate} \item $(a,b,c) \in S$ if and only if $(b,c,a) \in S$; \item $(a,b,c) \in S$ if and only if $(c,b,a) \notin S$; \item $(a,b,c)$ and $(c,d,a)$ are both in $S$ if and only if $(b,c,d)$ and $(d,a,b)$ are both in $S$. \end{enumerate} Prove that there exists a one-to-one function $g$ from $A$ to $\R$ such that $g(a) < g(b) < g(c)$ implies $(a,b,c) \in S$.
 -/
 theorem putnam_1996_a4
 (A : Type*)
 [Finite A]
 (S : Set (A × A × A))
 (hSdistinct : ∀ a b c : A, ⟨a, b, c⟩ ∈ S → a ≠ b ∧ b ≠ c ∧ a ≠ c)
 (hS1 : ∀ a b c : A, ⟨a, b, c⟩ ∈ S ↔ ⟨b, c, a⟩ ∈ S)
-(hS2 : ∀ a b c : A, ⟨a, b, c⟩ ∈ S ↔ ⟨c, b, a⟩ ∉ S)
+(hS2 : ∀ a b c : A, a ≠ c → (⟨a, b, c⟩ ∈ S ↔ ⟨c, b, a⟩ ∉ S))
 (hS3 : ∀ a b c d : A, (⟨a, b, c⟩ ∈ S ∧ ⟨c, d, a⟩ ∈ S) ↔ (⟨b,c,d⟩ ∈ S ∧ ⟨d,a,b⟩ ∈ S))
 : ∃ g : A → ℝ, Injective g ∧ (∀ a b c : A, g a < g b ∧ g b < g c → ⟨a,b,c⟩ ∈ S) :=
 sorry

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