diff --git a/coq/src/putnam_1987_a3.v b/coq/src/putnam_1987_a3.v index eab38600..3439c67a 100644 --- a/coq/src/putnam_1987_a3.v +++ b/coq/src/putnam_1987_a3.v @@ -2,8 +2,10 @@ Require Import Reals Coquelicot.Coquelicot. Open Scope R. Definition putnam_1987_a3_solution := (False, True). Theorem putnam_1987_a3 - (f g: R -> R) - (x: R) - : (((Derive_n f 2) x - 2 * (Derive_n f 1) x + f x = 2 * exp x /\ forall (x: R), f x > 0 -> forall (x: R), Derive_n f 1 x > 0) <-> fst putnam_1987_a3_solution) /\ - ((((Derive_n g 2) x - 2 * (Derive_n g 1) x + g x = 2 * exp x /\ forall (x: R), Derive_n g 1 x > 0) -> forall (x: R), g x > 0) <-> snd putnam_1987_a3_solution). + : ((forall (f: R -> R), (forall (x: R), ex_derive_n f 1 x /\ ex_derive_n f 2 x /\ (Derive_n f 2) x - 2 * (Derive_n f 1) x + f x = 2 * exp x /\ f x > 0) + -> forall (x: R), Derive_n f 1 x > 0) + <-> fst putnam_1987_a3_solution) /\ + ((forall (g: R -> R), (forall (x: R), ex_derive_n g 1 x /\ ex_derive_n g 2 x /\ (Derive_n g 2) x - 2 * (Derive_n g 1) x + g x = 2 * exp x /\ Derive_n g 1 x > 0) + -> forall (x: R), g x > 0) + <-> snd putnam_1987_a3_solution). Proof. Admitted. diff --git a/coq/src/putnam_1987_b4.v b/coq/src/putnam_1987_b4.v index 310f37a0..a7485bee 100644 --- a/coq/src/putnam_1987_b4.v +++ b/coq/src/putnam_1987_b4.v @@ -1,16 +1,17 @@ Require Import Reals Coquelicot.Coquelicot. Open Scope R. -Definition putnam_1987_b4_solution := (-1, PI). +Definition putnam_1987_b4_solution := (True, -1, True, 0). Theorem putnam_1987_b4 - (A := fix a (i j: nat) : (R * R):= - match (i, j) with - | (O, O) => (0.8, 0.6) - | (S i', S j') => - let xn := fst (a i' j') in - let yn := snd (a i' j') in - (xn * cos yn - yn * sin yn,xn * sin yn + yn * cos yn) - | (_, _) => (0, 0) + (A := fix a (n: nat) : (R * R) := + match n with + | O => (0.8, 0.6) + | (S n') => + let (xn, yn) := a n' in + (xn * cos yn - yn * sin yn, xn * sin yn + yn * cos yn) end) - : Lim_seq (fun n => fst (A n 0%nat)) = fst putnam_1987_b4_solution /\ - Lim_seq (fun n => snd (A 0%nat n)) = snd putnam_1987_b4_solution. + : let '(existsx, limx, existsy, limy) := putnam_1987_b4_solution in + (ex_lim_seq (fun n => fst (A n)) <-> existsx) /\ + (existsx -> Lim_seq (fun n => fst (A n)) = limx) /\ + (ex_lim_seq (fun n => snd (A n)) <-> existsy) /\ + (existsy -> Lim_seq (fun n => snd (A n)) = limy). Proof. Admitted. diff --git a/coq/src/putnam_1988_a2.v b/coq/src/putnam_1988_a2.v index 2761e3f8..67a6adb9 100644 --- a/coq/src/putnam_1988_a2.v +++ b/coq/src/putnam_1988_a2.v @@ -4,7 +4,8 @@ Open Scope R. Definition putnam_1988_a2_solution := True. Theorem putnam_1988_a2 (f : R -> R := fun x => exp (pow x 2)) - : exists (a b: R) (g: R -> R), - forall (x: R), a < x < b -> Derive (compose f g) = compose (Derive f) (Derive g) + : (exists (a b: R) (g: R -> R), a < b /\ + (exists x: R, a < x < b /\ g x <> 0) /\ + forall (x: R), a < x < b -> ex_derive g x /\ Derive (fun y => f y * g y) x = (Derive f x) * (Derive g x)) <-> putnam_1988_a2_solution. Proof. Admitted. diff --git a/coq/src/putnam_1988_a3.v b/coq/src/putnam_1988_a3.v index ab62744f..b9ffe697 100644 --- a/coq/src/putnam_1988_a3.v +++ b/coq/src/putnam_1988_a3.v @@ -2,5 +2,5 @@ Require Import Reals Coquelicot.Coquelicot. Open Scope R. Definition putnam_1988_a3_solution (a: R) := a > 1/2. Theorem putnam_1988_a3 - : forall (a: R), ex_finite_lim_seq (fun m => sum_n (fun n => Rpower (1/INR n * (1 / sin (1/INR n) - 1)) a) m) <-> putnam_1988_a3_solution a. + : forall (a: R), ex_finite_lim_seq (fun m => sum_n_m (fun n => Rpower (1/INR n * (1 / sin (1/INR n)) - 1) a) 1 m) <-> putnam_1988_a3_solution a. Proof. Admitted. diff --git a/coq/src/putnam_1988_a4.v b/coq/src/putnam_1988_a4.v index 6510ec3d..aeb4428f 100644 --- a/coq/src/putnam_1988_a4.v +++ b/coq/src/putnam_1988_a4.v @@ -1,6 +1,6 @@ Require Import Reals Coquelicot.Coquelicot. From mathcomp Require Import fintype. Definition putnam_1988_a4_solution : Prop * Prop := (True, False). Theorem putnam_1988_a4 - (p : nat -> Prop := fun n : nat => (forall color : (R * R) -> 'I_n, exists p q : R * R, color p = color q /\ norm (fst p - fst q, snd p - snd q) = 1)) + (p : nat -> Prop := fun n : nat => (forall color : (R * R) -> 'I_n, exists p q : R * R, color p = color q /\ norm (fst p - fst q, snd p - snd q) = 1)) : let (a, b) := putnam_1988_a4_solution in ((p 3%nat) <-> a) /\ ((p 9%nat) <-> b). -Proof. Admitted. \ No newline at end of file +Proof. Admitted. diff --git a/coq/src/putnam_1988_a5.v b/coq/src/putnam_1988_a5.v index a3ce2330..01084f78 100644 --- a/coq/src/putnam_1988_a5.v +++ b/coq/src/putnam_1988_a5.v @@ -2,6 +2,7 @@ Require Import Basics Reals. Open Scope R. Theorem putnam_1988_a5 : exists! (f: R -> R), - forall (x: R), (x > 0 -> f x > 0) -> - (compose f f) x = 6 * x - f x. + (forall (x: R), x <= 0 -> f x = 0) /\ + forall (x: R), x > 0 -> + (f x > 0 /\ (compose f f) x = 6 * x - f x). Proof. Admitted. diff --git a/coq/src/putnam_1988_b2.v b/coq/src/putnam_1988_b2.v index 5f80cd71..4d6032ac 100644 --- a/coq/src/putnam_1988_b2.v +++ b/coq/src/putnam_1988_b2.v @@ -2,6 +2,6 @@ Require Import Reals Coquelicot.Coquelicot. Open Scope R. Definition putnam_1988_b2_solution := True. Theorem putnam_1988_b2 - : forall (a: R), a >= 0 -> forall (x: R), pow (x + 1) 2 >= a * (a + 1) -> - pow x 2 >= a * (a - 1) <-> putnam_1988_b2_solution. + : (forall (a: R), a >= 0 -> forall (x: R), pow (x + 1) 2 >= a * (a + 1) -> + pow x 2 >= a * (a - 1)) <-> putnam_1988_b2_solution. Proof. Admitted. diff --git a/coq/src/putnam_1988_b3.v b/coq/src/putnam_1988_b3.v index cb906588..e898cb2d 100644 --- a/coq/src/putnam_1988_b3.v +++ b/coq/src/putnam_1988_b3.v @@ -2,6 +2,6 @@ Require Import Reals Coquelicot.Coquelicot. Definition putnam_1988_b3_solution := (1 + sqrt 3) / 2. Theorem putnam_1988_b3 (r : Z -> R) - (hr : forall (n: Z), Z.ge n 1 -> (exists c d : Z, (Z.ge c 0 /\ Z.ge d 0) /\ Z.eq (Z.add c d) n /\ r n = Rabs (IZR c - IZR d * sqrt 3)) /\ (forall c d : Z, (Z.ge c 0 /\ Z.ge d 0 /\ (Z.add c d) = n) -> Rabs (IZR c - IZR d * sqrt 3) >= r n)) - : putnam_1988_b3_solution > 0 /\ (forall n : Z, Z.ge n 1 -> r n <= putnam_1988_b3_solution) /\ (forall (g: R), g > 0 -> (forall (n: Z), Z.ge n 1 /\ r n <= g) -> g >= putnam_1988_b3_solution). + (hr : forall (n: Z), Z.ge n 1 -> (exists c d : Z, Z.ge c 0 /\ Z.ge d 0 /\ (Z.add c d) = n /\ r n = Rabs (IZR c - IZR d * sqrt 3)) /\ (forall c d : Z, (Z.ge c 0 /\ Z.ge d 0 /\ (Z.add c d) = n) -> Rabs (IZR c - IZR d * sqrt 3) >= r n)) + : putnam_1988_b3_solution > 0 /\ (forall n : Z, Z.ge n 1 -> r n <= putnam_1988_b3_solution) /\ (forall (g: R), g > 0 -> (forall (n: Z), Z.ge n 1 -> r n <= g) -> g >= putnam_1988_b3_solution). Proof. Admitted. diff --git a/coq/src/putnam_1988_b4.v b/coq/src/putnam_1988_b4.v index 42c792be..ddbfe3fd 100644 --- a/coq/src/putnam_1988_b4.v +++ b/coq/src/putnam_1988_b4.v @@ -1,7 +1,9 @@ Require Import Reals Coquelicot.Coquelicot. Open Scope R. Theorem putnam_1988_b4 - (b : nat -> (nat -> R) -> R := fun n a => Rpower (a n) (INR n/(INR n + 1))) - : forall (a: nat -> R), (forall (n: nat), a n > 0) -> - ex_finite_lim_seq (fun n => sum_n a n) -> ex_finite_lim_seq (fun n => sum_n (fun m => (b m a)) n). + (a : nat -> R) + (appos : (nat -> R) -> Prop := fun a' : nat -> R => forall n : nat, ge n 1 -> a' n > 0) + (apconv : (nat -> R) -> Prop := fun a' : nat -> R => ex_finite_lim_seq (fun N => sum_n_m a' 1 N)) + (apposconv : (nat -> R) -> Prop := fun a' => appos a' /\ apconv a') + : apposconv a -> apposconv (fun n => Rpower (a n) (INR n/(INR n + 1))). Proof. Admitted. diff --git a/coq/src/putnam_1988_b6.v b/coq/src/putnam_1988_b6.v index f794b7a3..6b774030 100644 --- a/coq/src/putnam_1988_b6.v +++ b/coq/src/putnam_1988_b6.v @@ -1,6 +1,7 @@ -Require Import Ensembles Finite_sets. +Require Import Ensembles Finite_sets ZArith. +Open Scope Z. Theorem putnam_1988_b6 - (triangular : nat -> Prop := fun n => exists (m: nat), n = Nat.div (m * (m + 1)) 2) - (E: Ensemble (nat*nat) := fun '(a, b) => exists (m: nat), triangular m <-> triangular (Nat.mul a m + b)) - : ~ exists (n: nat), cardinal (nat*nat) E n. + (triangular : Z -> Prop := fun n => exists (m: Z), m >= 0 /\ n = (m * (m + 1)) / 2) + (E: Ensemble (Z*Z) := fun '(a, b) => forall (m: Z), m > 0 -> (triangular m <-> triangular (Z.mul a m + b))) + : ~ exists (n: nat), cardinal (Z*Z) E n. Proof. Admitted. diff --git a/coq/src/putnam_1989_a1.v b/coq/src/putnam_1989_a1.v index 2f91de60..f0ee0af5 100644 --- a/coq/src/putnam_1989_a1.v +++ b/coq/src/putnam_1989_a1.v @@ -1,7 +1,7 @@ -Require Import Nat Reals ZArith Znumtheory Coquelicot.Coquelicot. +Require Import Nat Reals ZArith Znumtheory Coquelicot.Coquelicot Finite_sets. Open Scope R. -Definition putnam_1989_a1_solution (x: R) := x = INR 101. +Definition putnam_1989_a1_solution := 1%nat. Theorem putnam_1989_a1 - (a : nat -> R := fun n => sum_n (fun n => if odd n then INR (10^(n-1)) else R0) (2*n+2)) - : forall (n: nat), prime (floor (a n)) -> putnam_1989_a1_solution (a n). + (a : nat -> R := fun n => sum_n (fun i => if odd i then INR (10^(i-1)) else R0) (2*n+2)) + : cardinal nat (fun n => prime (floor (a n))) putnam_1989_a1_solution. Proof. Admitted. diff --git a/coq/src/putnam_1989_a2.v b/coq/src/putnam_1989_a2.v index f135c9e1..4593eb9e 100644 --- a/coq/src/putnam_1989_a2.v +++ b/coq/src/putnam_1989_a2.v @@ -3,6 +3,7 @@ Open Scope R. Definition putnam_1989_a2_solution (a b: R) := (exp (pow (a*b) 2) - 1)/(a * b). Theorem putnam_1989_a2 (a b: R) + (abpos : a > 0 /\ b > 0) (f : R -> R -> R := fun x y => Rmax (pow (b*x) 2) (pow (a*y) 2)) : RInt (fun x => (RInt (fun y => exp (f x y)) 0 b)) 0 a = putnam_1989_a2_solution a b. Proof. Admitted. diff --git a/coq/src/putnam_1989_a3.v b/coq/src/putnam_1989_a3.v index cf291113..6e253e2e 100644 --- a/coq/src/putnam_1989_a3.v +++ b/coq/src/putnam_1989_a3.v @@ -2,5 +2,5 @@ Require Import Reals Coquelicot.Coquelicot. From Coqtail Require Import Cpow. Open Scope C. Theorem putnam_1989_a3 (f : C -> C := fun z => 11 * Cpow z 10 + 10 * Ci * Cpow z 9 + 10 * Ci * z - 11) - : forall (x: C), f x = 0 <-> Cmod x = R1. + : forall (x: C), f x = 0 -> Cmod x = R1. Proof. Admitted. diff --git a/coq/src/putnam_1990_a1.v b/coq/src/putnam_1990_a1.v index e5ec62f0..61f77fef 100644 --- a/coq/src/putnam_1990_a1.v +++ b/coq/src/putnam_1990_a1.v @@ -8,6 +8,5 @@ Theorem putnam_1990_a1 | S (S O) => 6 | S (S (S n''' as n'') as n') => (n + 4) * a n' - 4 * n * a n'' + (4 * n - 8) * a n''' end) - : exists (b c: nat -> nat), forall (n: nat), A n = b n + c n <-> - (b,c) = putnam_1990_a1_solution. + : let (b,c) := putnam_1990_a1_solution in forall (n: nat), A n = b n + c n. Proof. Admitted. diff --git a/coq/src/putnam_1990_a2.v b/coq/src/putnam_1990_a2.v index e8a0319d..750d4343 100644 --- a/coq/src/putnam_1990_a2.v +++ b/coq/src/putnam_1990_a2.v @@ -2,6 +2,6 @@ Require Import Reals Coquelicot.Coquelicot. Open Scope R. Definition putnam_1990_a2_solution := True. Theorem putnam_1990_a2 - (numform : R -> Prop := fun x => exists (n m: nat), x = pow (INR n) (1/3) - pow (INR m) (1/3)) - : exists (s: nat -> R), forall (i: nat), numform (s i) /\ Lim_seq s = sqrt 2 <-> putnam_1990_a2_solution. -Proof. Admitted. \ No newline at end of file + (numform : R -> Prop := fun x => exists (n m: nat), x = Rpower (INR n) (1/3) - Rpower (INR m) (1/3)) + : (exists (s: nat -> R), (forall (i: nat), numform (s i)) /\ is_lim_seq s (sqrt 2)) <-> putnam_1990_a2_solution. +Proof. Admitted. diff --git a/coq/src/putnam_1990_a5.v b/coq/src/putnam_1990_a5.v index 232e4ba2..32bf9d64 100644 --- a/coq/src/putnam_1990_a5.v +++ b/coq/src/putnam_1990_a5.v @@ -1,9 +1,6 @@ From mathcomp Require Import matrix ssralg. Open Scope ring_scope. +Definition putnam_1990_a5_solution := False. Theorem putnam_1990_a5 - (R : ringType) - (n : nat) - (A B : 'M[R]_n) - : mulmx (mulmx (mulmx A B) A) B = 0 -> - mulmx (mulmx (mulmx B A) B) A = 0. + : (forall (R : ringType) (n: nat) (A B : 'M[R]_n), n >= 1 -> mulmx (mulmx (mulmx A B) A) B = 0 -> mulmx (mulmx (mulmx B A) B) A = 0) <-> putnam_1990_a5_solution. Proof. Admitted. diff --git a/coq/src/putnam_1990_b1.v b/coq/src/putnam_1990_b1.v index 1d2a3b98..0d602fc0 100644 --- a/coq/src/putnam_1990_b1.v +++ b/coq/src/putnam_1990_b1.v @@ -1,9 +1,9 @@ Require Import Reals Coquelicot.Coquelicot. Open Scope R. -Definition putnam_1990_b1_solution (f: R -> R) := f = (fun x => sqrt 1990 * exp x) /\ f = (fun x => -sqrt 1990 * exp x). +Definition putnam_1990_b1_solution (f: R -> R) := f = (fun x => sqrt 1990 * exp x) \/ f = (fun x => -sqrt 1990 * exp x). Theorem putnam_1990_b1 (f : R -> R) - : continuity f /\ forall x, ex_derive_n f 1 x -> - forall x, pow (f x) 2 = RInt (fun t => pow (f t) 2 + pow ((Derive f) t) 2) 0 x + 1990 -> + (fderiv : (forall x : R, ex_derive f x) /\ continuity (Derive f)) + : (forall x, pow (f x) 2 = RInt (fun t => pow (f t) 2 + pow ((Derive f) t) 2) 0 x + 1990) <-> putnam_1990_b1_solution f. Proof. Admitted. diff --git a/coq/src/putnam_1990_b2.v b/coq/src/putnam_1990_b2.v index 5702bf27..cae46349 100644 --- a/coq/src/putnam_1990_b2.v +++ b/coq/src/putnam_1990_b2.v @@ -1,8 +1,13 @@ Require Import Reals Coquelicot.Coquelicot. Open Scope R. Theorem putnam_1990_b2 + (prod_n : (nat -> R) -> nat -> R := fix P (a: nat -> R) (n : nat) : R := + match n with + | O => 1 + | S n' => a n' * P a n' + end) (x z : R) (hxz : Rabs x < 1 /\ Rabs z > 1) - (P : nat -> R := fun j => (sum_n (fun i => 1 - z * x ^ i) j) / (sum_n (fun i => z - x ^ i) j+1)) - : 1 + Series (fun j => 1 + x ^ (j+1) * P j) = 0. + (P : nat -> R := fun j => (prod_n (fun i => 1 - z * x ^ i) j) / (prod_n (fun i => z - x ^ (i + 1)) j)) + : 1 + Series (fun j => (1 + x ^ (j+1)) * P (j+1)%nat) = 0. Proof. Admitted. diff --git a/coq/src/putnam_1990_b3.v b/coq/src/putnam_1990_b3.v index 0fadfbec..bf48b8c6 100644 --- a/coq/src/putnam_1990_b3.v +++ b/coq/src/putnam_1990_b3.v @@ -1,14 +1,9 @@ Require Import Ensembles Finite_sets Reals Coquelicot.Coquelicot. Open Scope R. Theorem putnam_1990_b3 - (Mmult_n := - fix Mmult_n {T : Ring} (A : matrix 2 2) (p : nat) := - match p with - | O => A - | S p' => @Mmult T 2 2 2 A (Mmult_n A p') - end) - (E : Ensemble (matrix 2 2) := fun (A: matrix 2 2) => + (E : Ensemble (matrix 2 2)) + (hE : forall (A: matrix 2 2), E A -> forall (i j: nat), and (le 0 i) (lt i 2) /\ and (le 0 j) (lt j 2) -> (coeff_mat 0 A i j) <= 200 /\ exists (m: nat), coeff_mat 0 A i j = INR m ^ 2) - : exists (sz : nat), gt sz 50387 /\ cardinal (matrix 2 2) E sz -> exists (A B: matrix 2 2), E A /\ E B /\ Mmult A B = Mmult B A. + : (exists (sz : nat), gt sz 50387 /\ cardinal (matrix 2 2) E sz) -> exists (A B: matrix 2 2), E A /\ E B /\ A <> B /\ Mmult A B = Mmult B A. Proof. Admitted. diff --git a/coq/src/putnam_1990_b5.v b/coq/src/putnam_1990_b5.v index 6358c5a5..d1a40d89 100644 --- a/coq/src/putnam_1990_b5.v +++ b/coq/src/putnam_1990_b5.v @@ -2,8 +2,7 @@ Require Import Reals Ensembles Finite_sets Coquelicot.Coquelicot. Definition putnam_1990_b5_solution := True. Open Scope R. Theorem putnam_1990_b5 - (a : nat -> R) - (pn : nat -> R -> R := fun n x => sum_n (fun i => a i * pow x i) n) - : forall (n: nat), gt n 0 -> exists (roots: Ensemble R), cardinal R roots n /\ forall (r: R), roots r <-> pn n r = 0 <-> + (pn : (nat -> R) -> nat -> R -> R := fun a n x => sum_n (fun i => a i * pow x i) n) + : (exists (a : nat -> R), forall (n: nat), gt n 0 -> exists (roots: Ensemble R), cardinal R roots n /\ forall (r: R), roots r <-> pn a n r = 0) <-> putnam_1990_b5_solution. Proof. Admitted. diff --git a/isabelle/putnam_1987_a1.thy b/isabelle/putnam_1987_a1.thy index 7f2b0a61..49e5dbe5 100644 --- a/isabelle/putnam_1987_a1.thy +++ b/isabelle/putnam_1987_a1.thy @@ -4,8 +4,8 @@ begin theorem putnam_1987_a1: fixes A B C D :: "(real \ real) set" - defines "A \ {(x, y). x ^ 2 - y ^ 2 = x / (x ^ 2 + y ^ 2)}" - defines "B \ {(x, y). 2 * x * y + y / (x ^ 2 + y ^ 2) = 3}" + defines "A \ {(x, y). x ^ 2 + y ^ 2 \ 0 \ x ^ 2 - y ^ 2 = x / (x ^ 2 + y ^ 2)}" + defines "B \ {(x, y). x ^ 2 + y ^ 2 \ 0 \ 2 * x * y + y / (x ^ 2 + y ^ 2) = 3}" defines "C \ {(x, y). x ^ 3 - 3 * x * y ^ 2 + 3 * y = 1}" defines "D \ {(x, y). 3 * x ^ 2 * y - 3 * x - y ^ 3 = 0}" shows "A \ B = C \ D" diff --git a/isabelle/putnam_1987_a5.thy b/isabelle/putnam_1987_a5.thy index 4491890a..1190618e 100644 --- a/isabelle/putnam_1987_a5.thy +++ b/isabelle/putnam_1987_a5.thy @@ -16,7 +16,7 @@ theorem putnam_1987_a5: and "contdiff \ \ (Fi :: real^3 \ real) (j :: 3) (v :: real^3). (\ vj :: real. Fi (vrepl v j vj)) differentiable at (v$j) \ continuous (at (v$j)) (deriv (\ vj :: real. Fi (vrepl v j vj)))" and "partderiv \ \ (Fi :: real^3 \ real) (j :: 3). \ v :: real^3. deriv (\ vj :: real. Fi (vrepl v j vj)) (v$j)" and "Fprop1 \ \ F :: (real^3 \ real)^3. \ i :: 3. \ j :: 3. \ v \ 0. contdiffv (F$i) j v" - and "Fprop2 \ \ F :: (real^3 \ real)^3. \ v \ 0. vector [(partderiv (F$3) 2 - partderiv (F$2) 3) v, (partderiv (F$1) 3 - partderiv (F$3) 1) v, (partderiv (F$2) 1 - partderiv (F$1) 2) v] = 0" + and "Fprop2 \ \ F :: (real^3 \ real)^3. \ v \ 0. (vector [(partderiv (F$3) 2 - partderiv (F$2) 3) v, (partderiv (F$1) 3 - partderiv (F$3) 1) v, (partderiv (F$2) 1 - partderiv (F$1) 2) v] :: real^3) = 0" and "Fprop3 \ \ F :: (real^3 \ real)^3. \ x y :: real. (\ i :: 3. (F$i) (vector [x, y, 0])) = G (vector [x, y])" shows "(\ F :: (real^3 \ real)^3. Fprop1 F \ Fprop2 F \ Fprop3 F) \ putnam_1987_a5_solution" sorry diff --git a/isabelle/putnam_1987_b5.thy b/isabelle/putnam_1987_b5.thy index 59d9d33e..5056904f 100644 --- a/isabelle/putnam_1987_b5.thy +++ b/isabelle/putnam_1987_b5.thy @@ -5,7 +5,7 @@ theorem putnam_1987_b5: fixes n::nat and M::"complex^'a^'b" assumes matsize : "CARD('a) = n \ CARD('b) = 2 * n" and npos : "n > 0" - and hM : "\z::(complex^'b^1). (let prod = z ** M in (\i. prod$i = 0)) + and hM : "\z::(complex^'b^1). (\ i. (z ** M)$1$i = 0) \ (\(\i. z$1$i = 0)) \ (\i. Im (z$1$i) \ 0)" shows "\r::(real^1^'b). \w::(complex^1^'a). \i. Re ((M**w)$i$1) = r$i$1" sorry diff --git a/isabelle/putnam_1987_b6.thy b/isabelle/putnam_1987_b6.thy index 802a28ef..8ec32fb4 100644 --- a/isabelle/putnam_1987_b6.thy +++ b/isabelle/putnam_1987_b6.thy @@ -6,10 +6,11 @@ theorem putnam_1987_b6: assumes podd : "odd p \ prime p" and Ffield : "field F" and Fcard : "finite (carrier F) \ card (carrier F) = p^2" + and Ssub : "S \ carrier F" and Snz : "\x \ S. x \ \\<^bsub>F\<^esub>" and Scard : "real_of_nat (card S) = (p^2 - 1::real) / 2" and hS : "\a::'a. a \ carrier F \ a \ \\<^bsub>F\<^esub> \ \((a \ S) \ ((\\<^bsub>F\<^esub> a) \ S))" - shows "even (card (S \ {x. (\a \ S. x = a \\<^bsub>F\<^esub> a)}))" + shows "even (card (S \ {x \ carrier F. (\a \ S. x = a \\<^bsub>F\<^esub> a)}))" sorry end \ No newline at end of file diff --git a/isabelle/putnam_1988_a6.thy b/isabelle/putnam_1988_a6.thy index 5fe2aee8..64a3ff8d 100644 --- a/isabelle/putnam_1988_a6.thy +++ b/isabelle/putnam_1988_a6.thy @@ -16,7 +16,7 @@ theorem putnam_1988_a6: scale a (x \\<^bsub>V\<^esub> y) = scale a x \\<^bsub>V\<^esub> scale a y \ scale (a \\<^bsub>F\<^esub> b) x = scale a x \\<^bsub>V\<^esub> scale b x \ scale a (scale b x) = scale (a \\<^bsub>F\<^esub> b) x \ scale \\<^bsub>F\<^esub> x = x \ A (scale a x \\<^bsub>V\<^esub> scale b y) = scale a (A x) \\<^bsub>V\<^esub> scale b (A y)) \ - n = (GREATEST k :: nat. \ s :: 'b list. set s \ carrier V \ length s = k \ card (set s) = k \ + n = (GREATEST k :: nat. \ s :: 'b list. set s \ carrier V \ length s = k \ card (set s) = k \ (\ coeffs :: 'a list. set coeffs \ carrier F \ length coeffs = n \ (\\<^bsub>V\<^esub> i \ {0..\<^bsub>V\<^esub> \ (\ i \ {0..\<^bsub>F\<^esub>))) \ (\ evecs \ ((carrier V) - {\\<^bsub>V\<^esub>}). card evecs = n + 1 \ (\ evec \ evecs. \ a \ carrier F. A evec = scale a evec) \ diff --git a/isabelle/putnam_1989_a1.thy b/isabelle/putnam_1989_a1.thy index 1dc2caef..cf8877b5 100644 --- a/isabelle/putnam_1989_a1.thy +++ b/isabelle/putnam_1989_a1.thy @@ -6,7 +6,7 @@ definition putnam_1989_a1_solution::nat where "putnam_1989_a1_solution \ theorem putnam_1989_a1: fixes pdigalt::"(nat list) \ bool" defines "pdigalt \ \pdig. odd (length pdig) \ (\i \ {0..<(length pdig)}. pdig!i = (if (even i) then 1 else 0))" - shows "putnam_1989_a1_solution = card {p::nat. p > 0 \ prime p \ (\dig. (foldr (\a b. a + 10 * b) dig 0) = p \ pdigalt dig)}" + shows "putnam_1989_a1_solution = card {p::nat. p > 0 \ prime p \ (\ dig. (foldr (\a b. a + 10 * b) dig 0) = p \ pdigalt dig)}" sorry end \ No newline at end of file diff --git a/isabelle/putnam_1989_b1.thy b/isabelle/putnam_1989_b1.thy index 0c8a6ef7..c3926fbb 100644 --- a/isabelle/putnam_1989_b1.thy +++ b/isabelle/putnam_1989_b1.thy @@ -14,7 +14,7 @@ theorem putnam_1989_b1: and "edges \ {p \ square. p$1 = 0 \ p$1 = 1 \ p$2 = 0 \ p$2 = 1}" and "center \ \ i :: 2. (1 :: real) / 2" and "Scloser \ {p \ square. \ q \ edges. dist p center < dist p q}" - shows "let (a, b, c, d) = putnam_1989_b1_solution in b > 0 \ d > 0 \ (\(\ n :: int. n^2 = b)) \ + shows "let (a, b, c, d) = putnam_1989_b1_solution in b > 0 \ d > 0 \ (\(\ n :: int. (n^2) dvd b)) \ (Gcd {a, c, d} = 1) \ measure lebesgue Scloser / measure lebesgue square = (a * sqrt (real_of_int b) + c) / d" sorry diff --git a/isabelle/putnam_1990_a4.thy b/isabelle/putnam_1990_a4.thy index ec47786e..cca26b14 100644 --- a/isabelle/putnam_1990_a4.thy +++ b/isabelle/putnam_1990_a4.thy @@ -5,7 +5,7 @@ begin definition putnam_1990_a4_solution :: "nat" where "putnam_1990_a4_solution \ undefined" (* 3 *) theorem putnam_1990_a4: - shows "(LEAST n :: nat. n > 0 \ (\ S :: (real^2) set. card S = n \ (\ Q :: real^2. \ P \ S. \(\ q :: rat. (real_of_rat) q = dist P Q)))) = putnam_1990_a4_solution" + shows "(LEAST n :: nat. (\ S :: (real^2) set. card S = n \ (\ Q :: real^2. \ P \ S. \(\ q :: rat. real_of_rat q = dist P Q)))) = putnam_1990_a4_solution" sorry end \ No newline at end of file diff --git a/isabelle/putnam_1990_a5.thy b/isabelle/putnam_1990_a5.thy deleted file mode 100644 index 7bcae1b3..00000000 --- a/isabelle/putnam_1990_a5.thy +++ /dev/null @@ -1,13 +0,0 @@ -theory putnam_1990_a5 imports Complex_Main "HOL-Analysis.Finite_Cartesian_Product" -begin - -definition putnam_1990_a5_solution::bool where "putnam_1990_a5_solution \ undefined" -(* False *) -theorem putnam_1990_a5: - fixes A B::"real^'a^'a" and n::nat - assumes matsize : "CARD('a) = n \ n \ 1" - and habab : "A ** B ** A ** B = mat 0" - shows "(B ** A ** B ** A = mat 0) \ putnam_1990_a5_solution" - sorry - -end \ No newline at end of file diff --git a/isabelle/putnam_1990_b2.thy b/isabelle/putnam_1990_b2.thy index f1fc86c3..fe110445 100644 --- a/isabelle/putnam_1990_b2.thy +++ b/isabelle/putnam_1990_b2.thy @@ -6,7 +6,7 @@ theorem putnam_1990_b2: defines "P \ \j. (\i=0..i=1..j. (z - x^i))" assumes xlt1 : "abs(x) < 1" and zgt1 : "abs(z) > 1" - shows "1 + (\j::nat. (1 + x^(j+1)) * P j) = 0" + shows "1 + (\j::nat. (1 + x^(j+1)) * P (j+1)) = 0" sorry end \ No newline at end of file diff --git a/isabelle/putnam_1990_b3.thy b/isabelle/putnam_1990_b3.thy index 22a98089..7306b5c7 100644 --- a/isabelle/putnam_1990_b3.thy +++ b/isabelle/putnam_1990_b3.thy @@ -2,8 +2,8 @@ theory putnam_1990_b3 imports Complex_Main "HOL-Analysis.Finite_Cartesian_Produc begin theorem putnam_1990_b3: - fixes S::"(nat^2^2) set" - assumes hS : "\A \ S. (\i \ {1..2}. \j \ {1..2}. ((\x::nat. A$i$j = x^2) \ A$i$j \ 200))" + fixes S::"(nat^2^2) set" + assumes hS : "\A \ S. (\i j :: 2. ((\x::nat. A$i$j = x^2) \ A$i$j \ 200))" shows "card S > 50387 \ (\A \ S. \B \ S. A \ B \ A ** B = B ** A)" sorry diff --git a/isabelle/putnam_1990_b4.thy b/isabelle/putnam_1990_b4.thy index 47ab0823..0f6edf49 100644 --- a/isabelle/putnam_1990_b4.thy +++ b/isabelle/putnam_1990_b4.thy @@ -1,15 +1,12 @@ theory putnam_1990_b4 imports Complex_Main "HOL-Algebra.Multiplicative_Group" begin -(* Note: Boosted domain to infinite set *) -definition putnam_1990_b4_solution::bool where "putnam_1990_b4_solution \ undefined" -(* True *) theorem putnam_1990_b4: - fixes G (structure) and n::nat and a b::"'a" - assumes hG : "Group.group G \ finite (carrier G) \ card (carrier G) = n" - and abgen : "generate G {a, b} = carrier G \ a \ b" - shows "(\g::nat\'a. (\x \ carrier G. card {i::nat. i < 2 * n \ g i = x} = 2) \ - (\i \ {0..<(2*n)}. (g ((i+1) mod (2*n)) = g i \ a) \ (g ((i+1) mod (2*n)) = g i \ b))) \ putnam_1990_b4_solution" + assumes pacard: "\ pamap :: 'a \ nat. surj pamap" + shows "(\ (G :: 'a monoid) (n :: nat) (a :: 'a) (b :: 'a). Group.group G \ finite (carrier G) \ card (carrier G) = n \ + (generate G {a, b} = carrier G \ generate G {a} \ carrier G \ generate G {b} \ carrier G) \ + (\g::nat\'a. (\x \ carrier G. card {i::nat. i < 2 * n \ g i = x} = 2) \ + (\i \ {0..<(2*n)}. (g ((i+1) mod (2*n)) = g i \\<^bsub>G\<^esub> a) \ (g ((i+1) mod (2*n)) = g i \\<^bsub>G\<^esub> b)))) \ putnam_1990_b4_solution" sorry end \ No newline at end of file diff --git a/lean4/src/putnam_1987_a1.lean b/lean4/src/putnam_1987_a1.lean index 62b7120a..d039be71 100644 --- a/lean4/src/putnam_1987_a1.lean +++ b/lean4/src/putnam_1987_a1.lean @@ -3,8 +3,8 @@ open BigOperators theorem putnam_1987_a1 (A B C D : Set (ℝ × ℝ)) -(hA : A = {(x, y) : ℝ × ℝ | x ^ 2 - y ^ 2 = x / (x ^ 2 + y ^ 2)}) -(hB : B = {(x, y) : ℝ × ℝ | 2 * x * y + y / (x ^ 2 + y ^ 2) = 3}) +(hA : A = {(x, y) : ℝ × ℝ | x ^ 2 + y ^ 2 ≠ 0 ∧ x ^ 2 - y ^ 2 = x / (x ^ 2 + y ^ 2)}) +(hB : B = {(x, y) : ℝ × ℝ | x ^ 2 + y ^ 2 ≠ 0 ∧ 2 * x * y + y / (x ^ 2 + y ^ 2) = 3}) (hC : C = {(x, y) : ℝ × ℝ | x ^ 3 - 3 * x * y ^ 2 + 3 * y = 1}) (hD : D = {(x, y) : ℝ × ℝ | 3 * x ^ 2 * y - 3 * x - y ^ 3 = 0}) : A ∩ B = C ∩ D := sorry diff --git a/lean4/src/putnam_1990_b4.lean b/lean4/src/putnam_1990_b4.lean index f948b1f3..d1beba7e 100644 --- a/lean4/src/putnam_1990_b4.lean +++ b/lean4/src/putnam_1990_b4.lean @@ -7,6 +7,6 @@ open Filter Topology Nat abbrev putnam_1990_b4_solution : Prop := sorry -- True theorem putnam_1990_b4 -: (∀ (G : Type*) (_ : Fintype G) (_ : Group G) (n : ℕ) (a b : G), (n = Fintype.card G ∧ a ≠ b ∧ G = Subgroup.closure {a, b}) → (∃ g : ℕ → G, (∀ x : G, {i : Fin (2 * n) | g i = x}.encard = 2) +: (∀ (G : Type*) (_ : Fintype G) (_ : Group G) (n : ℕ) (a b : G), (n = Fintype.card G ∧ G = Subgroup.closure {a, b} ∧ G ≠ Subgroup.closure {a} ∧ G ≠ Subgroup.closure {b}) → (∃ g : ℕ → G, (∀ x : G, {i : Fin (2 * n) | g i = x}.encard = 2) ∧ (∀ i : Fin (2 * n), (g ((i + 1) % (2 * n)) = g i * a) ∨ (g ((i + 1) % (2 * n)) = g i * b))) ↔ putnam_1990_b4_solution) := sorry