From e2163be120fcd8d5d91624350138bed7e2fb7a08 Mon Sep 17 00:00:00 2001 From: George Tsoukalas Date: Tue, 29 Oct 2024 16:29:21 +0000 Subject: [PATCH 1/2] Clean formalizations. --- coq/src/putnam_1980_a5.v | 2 +- coq/src/putnam_2006_b2.v | 25 +++++++++++++++++-------- lean4/src/putnam_2018_b1.lean | 13 +++++-------- 3 files changed, 23 insertions(+), 17 deletions(-) diff --git a/coq/src/putnam_1980_a5.v b/coq/src/putnam_1980_a5.v index 08a4425b..ceeec395 100644 --- a/coq/src/putnam_1980_a5.v +++ b/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. \ No newline at end of file diff --git a/coq/src/putnam_2006_b2.v b/coq/src/putnam_2006_b2.v index e2af6e17..9cdb72c1 100644 --- a/coq/src/putnam_2006_b2.v +++ b/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. \ No newline at end of file diff --git a/lean4/src/putnam_2018_b1.lean b/lean4/src/putnam_2018_b1.lean index 37998aa5..55ab69b2 100644 --- a/lean4/src/putnam_2018_b1.lean +++ b/lean4/src/putnam_2018_b1.lean @@ -1,5 +1,4 @@ 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]} @@ -7,14 +6,12 @@ abbrev putnam_2018_b1_solution : Set (Mathlib.Vector ℤ 2) := sorry 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 From a99832e2506a245e239b1fbe19ce1895be7183d5 Mon Sep 17 00:00:00 2001 From: George Tsoukalas Date: Tue, 29 Oct 2024 16:32:04 +0000 Subject: [PATCH 2/2] Fix inaccurate informal statement. --- informal/putnam.json | 2 +- lean4/src/putnam_1996_a4.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/informal/putnam.json b/informal/putnam.json index 47ff069b..0afbcedb 100644 --- a/informal/putnam.json +++ b/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" diff --git a/lean4/src/putnam_1996_a4.lean b/lean4/src/putnam_1996_a4.lean index c3771b9e..8e9be779 100644 --- a/lean4/src/putnam_1996_a4.lean +++ b/lean4/src/putnam_1996_a4.lean @@ -4,7 +4,7 @@ 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*) @@ -12,7 +12,7 @@ theorem putnam_1996_a4 (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