From 955906c40ae1c19a4be2b450f9cf9501fd0a903e Mon Sep 17 00:00:00 2001 From: JohnEdwardJennings Date: Fri, 12 Jul 2024 00:59:27 -0500 Subject: [PATCH 1/2] Batch 53 Coq --- coq/src/putnam_1963_a2.v | 9 +++++++++ coq/src/putnam_1963_a4.v | 6 ++++++ coq/src/putnam_1963_b1.v | 9 +++++++++ coq/src/putnam_1963_b2.v | 7 +++++++ coq/src/putnam_1963_b3.v | 9 +++++++++ coq/src/putnam_1963_b5.v | 7 +++++++ coq/src/putnam_1963_b6.v | 10 ++++++++++ isabelle/putnam_1963_a2.thy | 2 +- isabelle/putnam_1963_a2.thy~ | 13 +++++++++++++ isabelle/putnam_1963_a4.thy | 2 +- isabelle/putnam_1963_a4.thy~ | 11 +++++++++++ lean4/src/putnam_1963_a2.lean | 2 +- lean4/src/putnam_1963_a4.lean | 2 +- 13 files changed, 85 insertions(+), 4 deletions(-) create mode 100644 coq/src/putnam_1963_a2.v create mode 100644 coq/src/putnam_1963_a4.v create mode 100644 coq/src/putnam_1963_b1.v create mode 100644 coq/src/putnam_1963_b2.v create mode 100644 coq/src/putnam_1963_b3.v create mode 100644 coq/src/putnam_1963_b5.v create mode 100644 coq/src/putnam_1963_b6.v create mode 100644 isabelle/putnam_1963_a2.thy~ create mode 100644 isabelle/putnam_1963_a4.thy~ diff --git a/coq/src/putnam_1963_a2.v b/coq/src/putnam_1963_a2.v new file mode 100644 index 00000000..4e4b4688 --- /dev/null +++ b/coq/src/putnam_1963_a2.v @@ -0,0 +1,9 @@ +Require Import Nat. +Theorem putnam_1963_a2 + (f : nat -> nat) + (hfpos : forall n : nat, gt (f n) 0) + (hfinc : forall i j : nat, gt i 0 -> gt j i -> gt (f j) (f i)) + (hf2 : f 2 = 2) + (hfmn : forall m n : nat, gt m 0 -> gt n 0 -> gcd m n = 1 -> f (m * n) = f m * f n) + : (forall (n : nat), n > 0 -> f n = n). +Proof. Admitted. \ No newline at end of file diff --git a/coq/src/putnam_1963_a4.v b/coq/src/putnam_1963_a4.v new file mode 100644 index 00000000..bd247cd0 --- /dev/null +++ b/coq/src/putnam_1963_a4.v @@ -0,0 +1,6 @@ +Require Import Reals. From Coquelicot Require Import Rbar Lim_seq. +Theorem putnam_1963_a4 + (apos : (nat -> R) -> Prop := fun a : nat -> R => forall n : nat, a n > 0) + (f : (nat -> R) -> nat -> R := fun a : nat -> R => fun n : nat => (INR n) * (((1 + a (S n)) / (a n)) - 1)) + : ((forall a : nat -> R, apos a -> LimSup_seq (f a) >= 1) /\ ~(exists c : R, c > 1 /\ forall a : nat -> R, apos a -> LimSup_seq (f a) >= c)). +Proof. Admitted. \ No newline at end of file diff --git a/coq/src/putnam_1963_b1.v b/coq/src/putnam_1963_b1.v new file mode 100644 index 00000000..9ac0d11d --- /dev/null +++ b/coq/src/putnam_1963_b1.v @@ -0,0 +1,9 @@ +Require Import ZArith. From mathcomp Require Import fintype ssralg ssrnat ssrnum poly polydiv. +Open Scope ring_scope. +Definition putnam_1963_b1_solution : Z := 2. +Theorem putnam_1963_b1 + (R : numDomainType) + (ZtoR : Z -> {poly R} := fun a => if (0 <=? a)%Z then (Z.to_nat a)%:R else -(Z.to_nat (-a))%:R) + : (forall a : Z, ('X^2 - 'X + ZtoR a) %| ('X^13 + 'X + 90%:R) = true <-> a = putnam_1963_b1_solution). +Proof. Admitted. + diff --git a/coq/src/putnam_1963_b2.v b/coq/src/putnam_1963_b2.v new file mode 100644 index 00000000..b38709a8 --- /dev/null +++ b/coq/src/putnam_1963_b2.v @@ -0,0 +1,7 @@ +Require Import ZArith Ensembles Reals. From Coquelicot Require Import Hierarchy. +Definition putnam_1963_b2_solution : Prop := True. +Theorem putnam_1963_b2 + (T : Ensemble R := fun x => exists m n : Z, x = (Rpower 2 (IZR m)) * (Rpower 3 (IZR n))) + (P : Ensemble R := fun x => x > 0) + : ((forall A : Ensemble R, Included R A P -> open A -> A <> Empty_set R -> Intersection R A T <> Empty_set R) <-> putnam_1963_b2_solution). +Proof. Admitted. \ No newline at end of file diff --git a/coq/src/putnam_1963_b3.v b/coq/src/putnam_1963_b3.v new file mode 100644 index 00000000..d21960a3 --- /dev/null +++ b/coq/src/putnam_1963_b3.v @@ -0,0 +1,9 @@ +Require Import Ensembles Reals Rtrigo_def Coquelicot.Coquelicot. +Open Scope R. +Definition putnam_1963_b3_solution : Ensemble (R -> R) := + Union (R -> R) (Union (R -> R) (fun f => exists A k : R, f = (fun x => A * sinh (k * x))) (fun f => exists A : R, f = (fun x => A * x))) (fun f => exists A k : R, f = fun x => (A * sin (k * x))). +Theorem putnam_1963_b3 + (f : R -> R) + (fdiff : forall x, ex_derive f x /\ ex_derive (Derive f) x) + : ((forall x y : R, (f x) ^ 2 - (f y) ^ 2 = f (x + y) * f (x - y)) <-> In (R -> R) putnam_1963_b3_solution f). +Proof. Admitted. \ No newline at end of file diff --git a/coq/src/putnam_1963_b5.v b/coq/src/putnam_1963_b5.v new file mode 100644 index 00000000..a2d2d479 --- /dev/null +++ b/coq/src/putnam_1963_b5.v @@ -0,0 +1,7 @@ +Require Import Reals ZArith. From Coquelicot Require Import Series Lim_seq Hierarchy Rbar. +Theorem putnam_1963_b5 + (a : Z -> R) + (haineq : forall n : Z, (n >= 1)%Z -> forall k : Z, ((n <= k)%Z /\ (k <= 2 * n)%Z) -> (0 <= a k /\ a k <= 100 * a n)) + (haseries : ex_lim_seq (fun nInc => sum_n (fun n => a (Z.of_nat n)) nInc)) + : (is_lim_seq (fun n : nat => (INR n) * (a (Z.of_nat n))) 0). +Proof. Admitted. \ No newline at end of file diff --git a/coq/src/putnam_1963_b6.v b/coq/src/putnam_1963_b6.v new file mode 100644 index 00000000..e9764bda --- /dev/null +++ b/coq/src/putnam_1963_b6.v @@ -0,0 +1,10 @@ +Require Import Ensembles. From GeoCoq Require Import Main.Tarski_dev.Ch16_coordinates_with_functions. +(* Note: This formalization assumes a 3D space; 1D and 2D spaces can be seen as lines and planes in this larger space. *) +Context `{T3D:Tarski_3D}. +Theorem putnam_1963_b6 + (T : Ensemble Tpoint -> Ensemble Tpoint := fun A => (fun r => exists p q, In Tpoint A p /\ In Tpoint A q /\ Bet p r q)) + (A : nat -> Ensemble Tpoint) + (hA0 : (A 0) <> Empty_set Tpoint) + (hAn : forall n : nat, n >= 1 -> A n = T (A (n - 1))) + : (forall n : nat, n >= 2 -> A n = A (n + 1)). +Proof. Admitted. \ No newline at end of file diff --git a/isabelle/putnam_1963_a2.thy b/isabelle/putnam_1963_a2.thy index 3c92af7d..3583f47c 100644 --- a/isabelle/putnam_1963_a2.thy +++ b/isabelle/putnam_1963_a2.thy @@ -4,7 +4,7 @@ begin theorem putnam_1963_a2: fixes f::"nat\nat" assumes hfpos : "\n. f n > 0" - and hfinc : "strict_mono f" + and hfinc : "strict_mono_on {1..} f" and hf2 : "f 2 = 2" and hfmn : "\m n. m > 0 \ n > 0 \ coprime m n \ f (m * n) = f m * f n" shows "\n > 0. f n = n" diff --git a/isabelle/putnam_1963_a2.thy~ b/isabelle/putnam_1963_a2.thy~ new file mode 100644 index 00000000..3c92af7d --- /dev/null +++ b/isabelle/putnam_1963_a2.thy~ @@ -0,0 +1,13 @@ +theory putnam_1963_a2 imports Complex_Main +begin + +theorem putnam_1963_a2: + fixes f::"nat\nat" + assumes hfpos : "\n. f n > 0" + and hfinc : "strict_mono f" + and hf2 : "f 2 = 2" + and hfmn : "\m n. m > 0 \ n > 0 \ coprime m n \ f (m * n) = f m * f n" + shows "\n > 0. f n = n" + sorry + +end \ No newline at end of file diff --git a/isabelle/putnam_1963_a4.thy b/isabelle/putnam_1963_a4.thy index 70eac977..bc364421 100644 --- a/isabelle/putnam_1963_a4.thy +++ b/isabelle/putnam_1963_a4.thy @@ -5,7 +5,7 @@ theorem putnam_1963_a4: fixes apos::"(nat\real) \ bool" and f::"(nat\real) \ nat \ ereal" defines "apos \ \a. \n. a n > 0" and "f \ \a::(nat\real). \n::nat. ereal (n * (((1 + a (n+1)) / (a n)) - 1))" - shows "(\a::(nat\real). apos a \ (limsup (f a)) \ 1) \ (\a. apos a \ (limsup (f a)) = 1)" + shows "(\a::(nat\real). apos a \ (limsup (f a)) \ 1) \ \(\ c > 1. \a. apos a \ (limsup (f a)) \ c)" sorry end \ No newline at end of file diff --git a/isabelle/putnam_1963_a4.thy~ b/isabelle/putnam_1963_a4.thy~ new file mode 100644 index 00000000..70eac977 --- /dev/null +++ b/isabelle/putnam_1963_a4.thy~ @@ -0,0 +1,11 @@ +theory putnam_1963_a4 imports Complex_Main "HOL-Library.Liminf_Limsup" "HOL-Library.Extended_Real" +begin + +theorem putnam_1963_a4: + fixes apos::"(nat\real) \ bool" and f::"(nat\real) \ nat \ ereal" + defines "apos \ \a. \n. a n > 0" + and "f \ \a::(nat\real). \n::nat. ereal (n * (((1 + a (n+1)) / (a n)) - 1))" + shows "(\a::(nat\real). apos a \ (limsup (f a)) \ 1) \ (\a. apos a \ (limsup (f a)) = 1)" + sorry + +end \ No newline at end of file diff --git a/lean4/src/putnam_1963_a2.lean b/lean4/src/putnam_1963_a2.lean index 78859bf2..2dbf6783 100644 --- a/lean4/src/putnam_1963_a2.lean +++ b/lean4/src/putnam_1963_a2.lean @@ -6,7 +6,7 @@ open Topology Filter theorem putnam_1963_a2 (f : ℕ → ℕ) (hfpos : ∀ n, f n > 0) -(hfinc : StrictMono f) +(hfinc : StrictMonoOn f (Set.Ici 1)) (hf2 : f 2 = 2) (hfmn : ∀ m n, m > 0 → n > 0 → IsRelPrime m n → f (m * n) = f m * f n) : ∀ n > 0, f n = n := diff --git a/lean4/src/putnam_1963_a4.lean b/lean4/src/putnam_1963_a4.lean index 760d4762..ece0b33f 100644 --- a/lean4/src/putnam_1963_a4.lean +++ b/lean4/src/putnam_1963_a4.lean @@ -6,5 +6,5 @@ open Topology Filter theorem putnam_1963_a4 (apos : (ℕ → ℝ) → Prop := fun a => ∀ n, a n > 0) (f : (ℕ → ℝ) → ℕ → ℝ := fun a n => n * (((1 + a (n+1)) / (a n)) - 1)) -: (∀ a, apos a → limsup (f a) ⊤ ≥ 1) ∧ (∃ a, apos a ∧ limsup (f a) ⊤ = 1) := +: (∀ a, apos a → limsup (f a) atTop ≥ 1) ∧ (¬∃ c > 1, ∀ a, apos a → limsup (f a) atTop ≥ c) := sorry From fdd4e020c84bea0a3ec29d7a51c22c273c5d3e19 Mon Sep 17 00:00:00 2001 From: JohnEdwardJennings Date: Fri, 12 Jul 2024 01:00:19 -0500 Subject: [PATCH 2/2] Cleaned up .thy~ files --- isabelle/putnam_1963_a2.thy~ | 13 ------------- isabelle/putnam_1963_a4.thy~ | 11 ----------- 2 files changed, 24 deletions(-) delete mode 100644 isabelle/putnam_1963_a2.thy~ delete mode 100644 isabelle/putnam_1963_a4.thy~ diff --git a/isabelle/putnam_1963_a2.thy~ b/isabelle/putnam_1963_a2.thy~ deleted file mode 100644 index 3c92af7d..00000000 --- a/isabelle/putnam_1963_a2.thy~ +++ /dev/null @@ -1,13 +0,0 @@ -theory putnam_1963_a2 imports Complex_Main -begin - -theorem putnam_1963_a2: - fixes f::"nat\nat" - assumes hfpos : "\n. f n > 0" - and hfinc : "strict_mono f" - and hf2 : "f 2 = 2" - and hfmn : "\m n. m > 0 \ n > 0 \ coprime m n \ f (m * n) = f m * f n" - shows "\n > 0. f n = n" - sorry - -end \ No newline at end of file diff --git a/isabelle/putnam_1963_a4.thy~ b/isabelle/putnam_1963_a4.thy~ deleted file mode 100644 index 70eac977..00000000 --- a/isabelle/putnam_1963_a4.thy~ +++ /dev/null @@ -1,11 +0,0 @@ -theory putnam_1963_a4 imports Complex_Main "HOL-Library.Liminf_Limsup" "HOL-Library.Extended_Real" -begin - -theorem putnam_1963_a4: - fixes apos::"(nat\real) \ bool" and f::"(nat\real) \ nat \ ereal" - defines "apos \ \a. \n. a n > 0" - and "f \ \a::(nat\real). \n::nat. ereal (n * (((1 + a (n+1)) / (a n)) - 1))" - shows "(\a::(nat\real). apos a \ (limsup (f a)) \ 1) \ (\a. apos a \ (limsup (f a)) = 1)" - sorry - -end \ No newline at end of file