1994 Isabelle & Coq verifications

coq/src/putnam_1994_a1.v

@@ -1,6 +1,7 @@
 Require Import Nat Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1994_a1
-    : exists (a: nat -> R), forall (n: nat), gt n 0 -> 0 < a n <= a (mul 2 n) + a (add (mul 2 n) 1) ->
-    ~ ex_lim_seq (fun n => sum_n (fun m => a m) n).
+    (a : nat -> R)
+    (ha : forall n : nat, gt n 0 -> 0 < a n <= a (mul 2 n) + a (add (mul 2 n) 1))
+    : ~ ex_finite_lim_seq (fun n => sum_n (fun m => a m) n).
 Proof. Admitted.

coq/src/putnam_1994_b1.v

@@ -2,7 +2,7 @@ Require Import Ensembles Finite_sets ZArith.
 Open Scope Z.
 Definition putnam_1994_b1_solution (n: Z) := 315 <= n <= 325 \/ 332 <= n <= 350.
 Theorem putnam_1994_b1
-    : forall (n: Z), exists (E: Ensemble Z), cardinal Z E 15 -> 
-    forall (m: Z), E m -> Z.abs (m * m - n) <= 250 ->
-    putnam_1994_b1_solution n.
+    (n : Z)
+    (nwithin : Prop := cardinal nat (fun m => Z.abs (n - (Z.of_nat m) ^ 2) <= 250) 15)
+    : (n > 0 /\ nwithin) <-> putnam_1994_b1_solution n.
 Proof. Admitted.

coq/src/putnam_1994_b2.v

@@ -1,9 +1,7 @@
-Require Import List Reals Coquelicot.Coquelicot.
+Require Import Ensembles Reals Finite_sets Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1994_b2_solution (c: R) := c < 243 / 8.
 Theorem putnam_1994_b2
-    (f : R -> R -> R := fun c x => pow x 4 + 9 * pow x 3 + c * pow x 2 + 9 * x + 4)
-    (g : R -> R -> R -> R := fun m x b  => m * x + b)
-    (hintersect : R -> Prop := fun c => exists(m b: R), exists (l: list R), eq (length l) 4%nat /\ NoDup l /\ forall (r: R), In r l -> f c r = g m b r)
+    (hintersect : R -> Prop := fun c => exists(m b: R), cardinal R (fun x => m * x + b = pow x 4 + 9 * pow x 3 + c * pow x 2 + 9 * x + 4) 4)
     : forall (c: R), hintersect c <-> putnam_1994_b2_solution c.
 Proof. Admitted.

coq/src/putnam_1994_b3.v

@@ -1,7 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1994_b3_solution (k: R) := k <= 1.
+Definition putnam_1994_b3_solution (k: R) := k < 1.
 Theorem putnam_1994_b3
-    : forall (k: R) (f: R -> R) (x: R), f x > 0 /\ ex_derive f x /\ (Derive f) x > f x ->
-    exists (N: R), x > N -> f x > exp (k * x) <-> putnam_1994_b3_solution k.
+    : forall k : R, (forall f : R -> R, (forall x : R, f x > 0 /\ ex_derive f x /\ (Derive f) x > f x) -> exists N : R, forall x : R, x > N -> f x > exp (k * x)) <-> putnam_1994_b3_solution k.
 Proof. Admitted.

coq/src/putnam_1994_b4.v

@@ -1,6 +1,5 @@
 Require Import Nat List Reals Coquelicot.Coquelicot. 
 Import ListNotations.
-Open Scope R.
 Theorem putnam_1994_b4 
     (gcdn := fix gcd_n (args : list nat) : nat :=
         match args with
@@ -10,6 +9,7 @@ Theorem putnam_1994_b4
     (Mmultn := fix Mmult_n {T : Ring} {n : nat} (A : matrix n n) (p : nat) :=
         match p with
         | O => A
+        | S O => A
         | S p' => @Mmult T n n n A (Mmult_n A p')
     end)
     (A := mk_matrix 2 2 (fun i j => 
@@ -29,5 +29,5 @@ Theorem putnam_1994_b4
                               Z.to_nat (floor (coeff_mat 0 (dn_mat n) 0 1)); 
                               Z.to_nat (floor (coeff_mat 0 (dn_mat n) 1 0)); 
                               Z.to_nat (floor (coeff_mat 0 (dn_mat n) 1 1))])
-    : ~ ex_lim_seq (fun n => INR (dn n)).
+    : forall k : nat, exists N : nat, forall n : nat, ge n N -> ge (dn n) k.
 Proof. Admitted.

coq/src/putnam_1994_b5.v

@@ -1,11 +1,11 @@
 Require Import Basics ZArith Zpower Reals Coquelicot.Coquelicot.
+Open Scope Z_scope.
 Theorem putnam_1994_b5
     (composen := fix compose_n {A: Type} (f : A -> A) (n : nat) :=
         match n with
         | O => fun x => x
         | S n' => compose f (compose_n f n')
     end)
-    (fa : R -> R -> R := fun a x => IZR (floor (a * x)))
-    : forall (n: Z), Z.gt n 0 ->
-    exists (a: R), forall (k: Z), and (Z.ge 1 k) (Z.ge k n) -> (composen (fa a) (Z.to_nat k)) (IZR (Z.pow n 2)) = IZR (Z.pow n 2 - k) /\ IZR (Z.pow n 2 - k) = fa (Rpower a (IZR k)) (IZR (Z.pow n 2)).
+    (fa : R -> Z -> Z := fun a x => floor (a * IZR x))
+    : forall (n: Z), n > 0 -> exists (a: R), forall (k: Z), 1 <= k <= n -> (composen (fa a) (Z.to_nat k)) n^2 = n^2 - k /\ n^2 - k = fa (Rpower a (IZR k)) n^2.
 Proof. Admitted.

coq/src/putnam_1994_b6.v

@@ -1,6 +1,7 @@
-Require Import Nat.
+Require Import ZArith.
+Open Scope Z_scope.
 Theorem putnam_1994_b6
-    (n : nat -> nat := fun a => 101 * a -  100 * pow 2 a)
-    : forall a b c d : nat, 0 <= a <= 99 /\ 0 <= b <= 99 /\  0 <= c <= 99 /\  0 <= d <= 99 /\ n a + n b mod 10100 = n c + n d ->
-    (a,b) = (c,d).
+    (n : Z -> Z := fun a => 101 * a - 100 * 2^a)
+    : forall a b c d : Z, 0 <= a <= 99 /\ 0 <= b <= 99 /\ 0 <= c <= 99 /\ 0 <= d <= 99 /\ 
+    (n a + n b) mod 10100 = (n c + n d) mod 10100 -> (a = c /\ b = d) \/ (a = d /\ b = c).
 Proof. Admitted.

isabelle/putnam_1994_a3.thy

@@ -7,7 +7,7 @@ theorem putnam_1994_a3:
   fixes T :: "(real^2) set"
     and Tcolors :: "(real^2) \<Rightarrow> 4"
   defines "T \<equiv> convex hull {vector [0, 0], vector [1, 0], vector [0, 1]}"
-  shows "\<exists> p \<in> T. \<exists> q \<in> T. Tcolors p = Tcolors q \<and> dist p q \<ge> 2 - sqrt (2 :: real)"
-  sorry
+  shows "\<exists> p \<in> T. \<exists> q \<in> T. Tcolors p = Tcolors q \<and> dist p q \<ge> 2 - sqrt 2"
+  sorry                                                               
 
 end

isabelle/putnam_1994_b5.thy

@@ -2,11 +2,11 @@ theory putnam_1994_b5 imports Complex_Main
 begin
 
 theorem putnam_1994_b5:
-  fixes f :: "real \<Rightarrow> nat \<Rightarrow> int"
+  fixes f :: "real \<Rightarrow> int \<Rightarrow> int"
   and n :: nat
-  assumes hf: "\<forall>(\<alpha>::real)(x::nat). f \<alpha> x = \<lfloor>\<alpha>*x\<rfloor>"
+  assumes hf: "\<forall>(\<alpha>::real)(x::int). f \<alpha> x = \<lfloor>\<alpha>*x\<rfloor>"
   and npos: "n > 0"
-  shows "\<exists>\<alpha>::real. \<forall>k::nat\<in>{1..n}. ((f \<alpha> (n^2))^k = n^2 - k) \<and> (f (\<alpha>^k) (n^2) = n^2 - k)"
+  shows "\<exists>\<alpha>::real. \<forall>k::nat\<in>{1..n}. (((f \<alpha>)^^k) (n^2) = n^2 - k) \<and> (f (\<alpha>^k) (n^2) = n^2 - k)"
   sorry
 
 end

lean4/src/putnam_1994_b5.lean

@@ -4,9 +4,9 @@ open BigOperators
 open Filter Topology
 
 theorem putnam_1994_b5
-(f : ℝ → ℕ → ℤ)
+(f : ℝ → ℤ → ℤ)
 (n : ℕ)
-(hf : ∀ (α : ℝ) (x : ℕ), f α x = Int.floor (α * x))
+(hf : ∀ (α : ℝ) (x : ℤ), f α x = Int.floor (α * x))
 (npos : n > 0)
-: ∃ α : ℝ, ∀ k ∈ Set.Icc 1 n, (((f α) ^ k) (n ^ 2) = n ^ 2 - k) ∧ (f (α ^ k) (n ^ 2) = n ^ 2 - k) :=
+: ∃ α : ℝ, ∀ k ∈ Set.Icc 1 n, ((f α)^[k] (n ^ 2) = n ^ 2 - k) ∧ (f (α ^ k) (n ^ 2) = n ^ 2 - k) :=
 sorry