diff --git a/coq/src/commented_problems.v b/coq/src/commented_problems.v
index 288456a9..0a52aade 100644
--- a/coq/src/commented_problems.v
+++ b/coq/src/commented_problems.v
@@ -133,3 +133,36 @@ Theorem putnam_2003_b5
     Triangle A' B' C' /\ dist A' B' = a /\ dist B' C' = b /\ dist C' A' = c /\
     F_to_R (signed_area A' B' C' D A' B' C') = (putnam_2003_b5_solution pt_to_R dist P Op).
 Proof. Admitted. *)
+
+(* Require Import Reals Rgeom ZArith 
+GeoCoq.Main.Tarski_dev.Ch16_coordinates_with_functions 
+GeoCoq.Main.Annexes.midpoint_theorems
+GeoCoq.Main.Highschool.circumcenter.
+Context `{T2D:Tarski_2D} `{TE:@Tarski_euclidean Tn TnEQD}.
+Open Scope R.
+Definition putnam_1997_a1_solution := 28.
+Theorem putnam_1997_a1
+    (pt_to_R : Tpoint -> (R * R))
+    (dist : Tpoint -> Tpoint -> R := fun A B => let (a, b) := pt_to_R A in let (c, d) := pt_to_R B in dist_euc a b c d)
+    (A B C : Tpoint)
+    (Hp Op Mp Fp : Tpoint)
+    (l1 : dist Hp Op = 11)
+    (l2 : dist Op Mp = 5)
+    (s : Rectangle Hp Op Mp Fp)
+    (hHp : Bet A Fp Hp)
+    (hOp : is_circumcenter Op A B C)
+    (hMp : Midpoint B C Mp)
+    (hFp : Perp A C B Fp /\ Col A C Fp)
+    : dist B C = putnam_1997_a1_solution.
+Proof. Admitted. *)
+
+(* Require Import Nat Reals Coquelicot.Coquelicot ZArith.
+Theorem putnam_1997_b4
+    (a : nat -> nat -> Z)
+    (max_degree : nat -> nat)
+    (coeff : nat -> (nat -> R))
+    (hpoly : forall (m : nat) (x : R), sum_n (fun i => (coeff m i) * (x^i)) (max_degree m) = (1 + x + x^2)^m)
+    (ha : forall m n : nat, IZR (a m n) = coeff m n)
+    : forall k : nat, ge k 0 -> 0 <= (sum_n (fun i => (-1)^i * (IZR (a (Nat.sub k i) i))) (Z.to_nat (Coquelicot.Rcomplements.floor (2 * INR k / 3)))) <= 1.
+Proof. Admitted. *)
+
diff --git a/coq/src/putnam_1994_b4.v b/coq/src/putnam_1994_b4.v
index e00f0544..7c3c6b63 100644
--- a/coq/src/putnam_1994_b4.v
+++ b/coq/src/putnam_1994_b4.v
@@ -8,8 +8,7 @@ Theorem putnam_1994_b4
     end)
     (Mmultn := fix Mmult_n {T : Ring} {n : nat} (A : matrix n n) (p : nat) :=
         match p with
-        | O => A
-        | S O => A
+        | O => mk_matrix n n (fun i j : nat => if Nat.eqb i j then one else zero)
         | S p' => @Mmult T n n n A (Mmult_n A p')
     end)
     (A := mk_matrix 2 2 (fun i j => 
diff --git a/coq/src/putnam_1996_a1.v b/coq/src/putnam_1996_a1.v
index 8b1b3627..d448279f 100644
--- a/coq/src/putnam_1996_a1.v
+++ b/coq/src/putnam_1996_a1.v
@@ -1,10 +1,8 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1996_a1_solution := (1 + sqrt 2) / 2.
-Theorem putnam_1996_a1 
-    (minA : R)
-    (packable : R -> R -> R -> R -> Prop := fun n1 n2 a1 a2 => (n1 + n2) <= Rmax a1 a2 /\ Rmax n1 n2 <= Rmin a1 a2)
-    (hminA : R -> R -> R -> R -> Prop := fun n1 n2 a1 a2 => a1 * a2 = minA /\ packable n1 n2 a1 a2)
-    (hminAlb : R -> R -> R -> R -> Prop :=  fun n1 n2 a1 a2 => forall (A: R), a1 * a2 = A /\ (packable n1 n2 a1 a2 -> minA <= A))
-    : (forall (n1 n2: R), pow n1 2 + pow n2 2 = 1 -> exists a1 a2 : R, hminA n1 n2 a1 a2 /\ hminAlb n1 n2 a1 a2) <-> minA =putnam_1996_a1_solution.
+Theorem putnam_1996_a1
+    (packable : R -> R -> R -> R -> Prop := (fun n1 n2 a1 a2 : R => (n1 + n2) <= Rmax a1 a2 /\ Rmax n1 n2 <= Rmin a1 a2))
+    (Aprop : R -> Prop := (fun A : R => forall n1 n2 : R, (n1 > 0 /\ n2 > 0 /\ pow n1 2 + pow n2 2 = 1) -> exists a1 a2 : R, a1 > 0 /\ a2 > 0 /\ a1 * a2 = A /\ packable n1 n2 a1 a2))
+    : Aprop putnam_1996_a1_solution /\ (forall A : R, Aprop A -> A >= putnam_1996_a1_solution).
 Proof. Admitted.
diff --git a/coq/src/putnam_1996_a3.v b/coq/src/putnam_1996_a3.v
index d3f33624..dbb9e677 100644
--- a/coq/src/putnam_1996_a3.v
+++ b/coq/src/putnam_1996_a3.v
@@ -1,10 +1,11 @@
 Require Import Nat Ensembles Finite_sets. From mathcomp Require Import fintype.
 Definition putnam_1996_a3_solution : Prop := False.
 Theorem putnam_1996_a3
-    (student_choices : nat -> Ensemble nat)
-    (hinrange : forall n : nat, Included _ (student_choices n) (fun i : nat => le 1 i /\ le i 6))
-    : putnam_1996_a3_solution <-> (exists S : Ensemble nat, Included _ S (fun i : nat => le 1 i /\ le i 20) /\ cardinal _ S 5 /\ 
-        (exists c1 c2 : nat, Included _ (fun i : nat => i = c1 \/ i = c2) (fun i : nat => le 1 i /\ le i 6) /\ 
-        (Included _ (fun i : nat => i = c1 \/ i = c2) (fun i : nat => (forall s : nat, In _ S s -> In _ (student_choices s) i)
-        \/ Included _ (fun i : nat => i = c1 \/ i = c2) (fun i : nat => forall s : nat, In _ S s -> ~ (In _ (student_choices s) i)))))).
+    (studentchoicesinrange : (nat -> Ensemble nat) -> Prop := (fun studentchoices : (nat -> Ensemble nat) => forall n : nat, Included _ (studentchoices n) (fun i : nat => le 1 i /\ le i 6)))
+    (studentchoicesprop : (nat -> Ensemble nat) -> Prop := (fun studentchoices : (nat -> Ensemble nat) =>
+        exists S : Ensemble nat, Included _ S (fun i : nat => le 1 i /\ le i 20) /\ cardinal _ S 5 /\ 
+        (exists c1 c2 : nat, (le 1 c1 /\ le c1 6) /\ (le 1 c2 /\ le c2 6) /\ c1 <> c2 /\
+        ((Included _ (fun i : nat => i = c1 \/ i = c2) (fun i : nat => forall s : nat, In _ S s -> In _ (studentchoices s) i))
+        \/ (Included _ (fun i : nat => i = c1 \/ i = c2) (fun i : nat => forall s : nat, In _ S s -> ~ (In _ (studentchoices s) i)))))))
+    : (forall studentchoices : (nat -> Ensemble nat), studentchoicesinrange studentchoices -> studentchoicesprop studentchoices) <-> putnam_1996_a3_solution.
 Proof. Admitted.
diff --git a/coq/src/putnam_1996_a4.v b/coq/src/putnam_1996_a4.v
index 0210b854..d7f832ea 100644
--- a/coq/src/putnam_1996_a4.v
+++ b/coq/src/putnam_1996_a4.v
@@ -2,10 +2,10 @@ Require Import Basics FinFun Reals Ensembles Finite_sets. From mathcomp Require
 Local Open Scope R_scope.
 Theorem putnam_1996_a4
     (A : finType)
-    (S : Ensemble (A * A * A))
-    (hSdistinct: forall a b c : A, In _ S (a, b, c) -> a <> b /\ b <> c /\ c <> a)
-    (hS1 : forall a b c : A, In _ S (a, b, c) -> In _ S (b, c, a))
-    (hS2 : forall a b c : A, In _ S (a, b, c) -> ~ (In _ S (c, b, a)))
-    (hS3 : forall a b c d : A, (In _ S (a, b, c)) /\ (In _ S (c, d, a)) <-> (In _ S (b, c, d) /\ In _ S (d, a, b)))
-    : exists g : A -> R, Injective g /\ (forall a b c : A, g a < g b /\ g b < g c -> In _ S (a, b, c)).
+    (SS : Ensemble (A * A * A))
+    (hSdistinct: forall a b c : A, In _ SS (a, b, c) -> a <> b /\ b <> c /\ c <> a)
+    (hS1 : forall a b c : A, In _ SS (a, b, c) <-> In _ SS (b, c, a))
+    (hS2 : forall a b c : A, In _ SS (a, b, c) <-> ~ (In _ SS (c, b, a)))
+    (hS3 : forall a b c d : A, (In _ SS (a, b, c) /\ In _ SS (c, d, a)) <-> (In _ SS (b, c, d) /\ In _ SS (d, a, b)))
+    : exists g : A -> R, Injective g /\ (forall a b c : A, g a < g b /\ g b < g c -> In _ SS (a, b, c)).
 Proof. Admitted.
diff --git a/coq/src/putnam_1996_a5.v b/coq/src/putnam_1996_a5.v
index edc80c37..895b0cc4 100644
--- a/coq/src/putnam_1996_a5.v
+++ b/coq/src/putnam_1996_a5.v
@@ -1,8 +1,8 @@
 Require Import Binomial Reals Znumtheory Coquelicot.Coquelicot. From mathcomp Require Import div.
 Open Scope R.
 Theorem putnam_1996_a5 
-    (p: nat)
+    (p : nat)
     (hp : prime (Z.of_nat p) /\ gt p 3)
-    (k := floor (2 * INR p / 3))
-    : exists (m: nat), sum_n (fun i => Binomial.C p (i+1)) (Z.to_nat k) = INR m * pow (INR p) 2.
+    (k : nat := Z.to_nat (floor (2 * INR p / 3)))
+    : exists (m : nat), sum_n_m (fun i => Binomial.C p i) 1 k = INR m * pow (INR p) 2.
 Proof. Admitted.
diff --git a/coq/src/putnam_1996_a6.v b/coq/src/putnam_1996_a6.v
index 01659a35..4b4b260b 100644
--- a/coq/src/putnam_1996_a6.v
+++ b/coq/src/putnam_1996_a6.v
@@ -1,8 +1,8 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1996_a6_solution (c: R) (f: R -> R) :=  if Rle_dec c (1/4) then exists (d: R), f = (fun _ => d) else forall (x: R), 0 <= x <= c -> continuity_pt f x /\ f 0 = f c /\ forall (x: R), x > 0 -> f x = f (pow x 2 + c) /\ (forall (x: R), x < 0 -> f x = f (-x)).
+Definition putnam_1996_a6_solution (c: R) (f: R -> R) :=  if Rle_dec c (1/4) then (exists (d: R), f = (fun _ => d)) else ((forall (x: R), 0 <= x <= c -> continuity_pt f x) /\ f 0 = f c /\ (forall (x: R), x > 0 -> f x = f (pow x 2 + c)) /\ (forall (x: R), x < 0 -> f x = f (-x))).
 Theorem putnam_1996_a6
     (c: R)
     (hc : c > 0)
-    : forall (f: R -> R), continuity f /\ forall (x: R), f x = pow x 2 + c <-> putnam_1996_a6_solution c f.
+    : forall (f: R -> R), (continuity f /\ (forall (x: R), f x = pow x 2 + c)) <-> putnam_1996_a6_solution c f.
 Proof. Admitted.
diff --git a/coq/src/putnam_1996_b2.v b/coq/src/putnam_1996_b2.v
index bcf6d855..e2c0be2d 100644
--- a/coq/src/putnam_1996_b2.v
+++ b/coq/src/putnam_1996_b2.v
@@ -1,10 +1,8 @@
-Require Import Reals Coquelicot.Coquelicot.
+Require Import Reals Coquelicot.Coquelicot. From mathcomp Require Import bigop.
 Open Scope R.
 Theorem putnam_1996_b2
-    (oddfact := fix odd_fact (n : nat) : R :=
-        match n with
-        | O => 1 
-        | S n' => (2 * INR n - 1) * odd_fact n'
-    end)
-    : forall (n: nat), gt n 0 -> pow ((2 * INR n - 1) / exp 1) ((2 * n - 1) / 2) < oddfact n < pow ((2 * INR n + 1) / exp 1) ((2 * n + 1) / 2).
+    (n : nat)
+    (prododd : R := INR (\prod_(1 <= i < (n + 1)) (2 * i - 1)))
+    (npos : gt n 0)
+    : Rpower ((2 * INR n - 1) / exp 1) ((2 * INR n - 1) / 2) < prododd < Rpower ((2 * INR n + 1) / exp 1) ((2 * INR n + 1) / 2).
 Proof. Admitted.
diff --git a/coq/src/putnam_1996_b3.v b/coq/src/putnam_1996_b3.v
index e595f532..1edebeaf 100644
--- a/coq/src/putnam_1996_b3.v
+++ b/coq/src/putnam_1996_b3.v
@@ -1,11 +1,9 @@
-Require Import Nat List Reals Coquelicot.Coquelicot.
-Open Scope R.
-Definition putnam_1996_b3_solution : nat -> R := fun n => (2 * INR n ^ 3 + 3 * INR n ^ 2 - 11 * INR n + 18) / 6.
+Require Import Reals Coquelicot.Hierarchy Nat.
+Definition putnam_1996_b3_solution : nat -> R := (fun n => (2 * INR n ^ 3 + 3 * INR n ^ 2 - 11 * INR n + 18) / 6).
 Theorem putnam_1996_b3
-    (m: nat -> R)
-    (n: nat)
-    (hn : ge n 2)
-    (hmub : sum_n (fun i => INR ((nth i (seq 1 (S n)) 0%nat) * (nth ((i + 1) mod n) (seq 1 (S n)) 0%nat))) n <= m n)
-    (hm : sum_n (fun i => INR ((nth i (seq 1 (S n)) 0%nat) * (nth ((i + 1) mod n) (seq 1 (S n))) 0%nat)) n = m n)
-    : m = putnam_1996_b3_solution.
+    (n : nat)
+    (xset : (nat -> nat) -> Prop := (fun x : nat -> nat => forall y : nat, (le 1 y /\ le y n) -> exists! i, (le 0 i /\ le i (n - 1)) /\ x i = y))
+    (xsum : (nat -> nat) -> R := (fun x : nat -> nat => sum_n (fun i : nat => INR (x i) * INR (x ((i + 1) mod n))) (n - 1)))
+    (nge2 : ge n 2)
+    : (exists x : nat -> nat, xset x /\ xsum x = putnam_1996_b3_solution n) /\ (forall x : nat -> nat, xset x -> xsum x <= putnam_1996_b3_solution n).
 Proof. Admitted.
diff --git a/coq/src/putnam_1996_b4.v b/coq/src/putnam_1996_b4.v
index 2e2d1ff5..35d927e3 100644
--- a/coq/src/putnam_1996_b4.v
+++ b/coq/src/putnam_1996_b4.v
@@ -4,15 +4,15 @@ Definition putnam_1996_b4_solution := False.
 Theorem putnam_1996_b4
     (Mmultn := fix Mmult_n {T : Ring} {n : nat} (A : matrix n n) (p : nat) :=
         match p with
-        | O => A
+        | O => mk_matrix n n (fun i j : nat => if Nat.eqb i j then one else zero)
         | S p' => @Mmult T n n n A (Mmult_n A p')
     end)
     (scale_c : R -> matrix 2 2 -> matrix 2 2 := fun c A =>  mk_matrix 2 2 (fun i j => c * coeff_mat 0 A i j))
     (sinA_mat : nat -> matrix 2 2 -> matrix 2 2 := fun n A => scale_c ((pow (-1) n) / INR (fact (2 * n + 1))) (Mmultn A (Nat.add (Nat.mul 2 n) 1)))
-    : exists (A: matrix 2 2), 
+    : (exists (A: matrix 2 2), 
     Series (fun n => coeff_mat 0 (sinA_mat n A) 0 0) = 1    /\
     Series (fun n => coeff_mat 0 (sinA_mat n A) 0 1) = 1996 /\
     Series (fun n => coeff_mat 0 (sinA_mat n A) 1 0) = 0    /\
-    Series (fun n => coeff_mat 0 (sinA_mat n A) 1 1) = 1    <->
+    Series (fun n => coeff_mat 0 (sinA_mat n A) 1 1) = 1)   <->
     putnam_1996_b4_solution.
 Proof. Admitted.
diff --git a/coq/src/putnam_1997_a1.v b/coq/src/putnam_1997_a1.v
deleted file mode 100644
index dc226746..00000000
--- a/coq/src/putnam_1997_a1.v
+++ /dev/null
@@ -1,21 +0,0 @@
-Require Import Reals Rgeom ZArith 
-GeoCoq.Main.Tarski_dev.Ch16_coordinates_with_functions 
-GeoCoq.Main.Annexes.midpoint_theorems
-GeoCoq.Main.Highschool.circumcenter.
-Context `{T2D:Tarski_2D} `{TE:@Tarski_euclidean Tn TnEQD}.
-Open Scope R.
-Definition putnam_1997_a1_solution := 28.
-Theorem putnam_1997_a1
-    (pt_to_R : Tpoint -> (R * R))
-    (dist : Tpoint -> Tpoint -> R := fun A B => let (a, b) := pt_to_R A in let (c, d) := pt_to_R B in dist_euc a b c d)
-    (A B C : Tpoint)
-    (Hp Op Mp Fp : Tpoint)
-    (l1 : dist Hp Op = 11)
-    (l2 : dist Op Mp = 5)
-    (s : Rectangle Hp Op Mp Fp)
-    (hHp : Bet A Fp Hp)
-    (hOp : is_circumcenter Op A B C)
-    (hMp : Midpoint B C Mp)
-    (hFp : Perp A C B Fp /\ Col A C Fp)
-    : dist B C = putnam_1997_a1_solution.
-Proof. Admitted.
diff --git a/coq/src/putnam_1997_a3.v b/coq/src/putnam_1997_a3.v
index 757637c9..c4801a3a 100644
--- a/coq/src/putnam_1997_a3.v
+++ b/coq/src/putnam_1997_a3.v
@@ -1,6 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1997_a3_solution := sqrt (exp 1).
+Definition putnam_1997_a3_solution : R := sqrt (exp 1).
 Theorem putnam_1997_a3
     (evenfact := fix even_fact (n : nat) : R :=
         match n with
@@ -10,9 +10,9 @@ Theorem putnam_1997_a3
     (evenfactsqr := fix even_fact_sqr (n : nat) : R :=
         match n with
         | O => 1 
-        | S n' => pow (2 * INR n) 2 * evenfact n'
+        | S n' => pow (2 * INR n) 2 * even_fact_sqr n'
     end)
     (f : R -> R := fun x => Series (fun n => pow (-1) n * pow x (2 * n + 1) / evenfact n))
     (g : R -> R := fun x => Series (fun n => pow x (2 * n) / evenfactsqr n))
-    : Lim_seq (fun n => sum_n (fun m => RInt (fun x => f x * g x) 0 (INR m)) n) = putnam_1997_a3_solution.
+    : Lim_seq (fun t : nat => RInt (fun x => f x * g x) 0 (INR t)) = putnam_1997_a3_solution.
 Proof. Admitted.
diff --git a/coq/src/putnam_1997_a4.v b/coq/src/putnam_1997_a4.v
index 3798d379..5f8a03d6 100644
--- a/coq/src/putnam_1997_a4.v
+++ b/coq/src/putnam_1997_a4.v
@@ -1,4 +1,4 @@
-(* Note: This formalization is only a statement finite groups (due to mathcomp), but the idea ot the problem does not rely on the cardinal of the group, so we include it*)
+(* Note: This formalization is only a statement finite groups (due to mathcomp), but the idea of the problem does not rely on the cardinal of the group, so we include it*)
 Require Import Basics. From mathcomp Require Import fingroup.
 Open Scope group_scope.
 Variable T : finGroupType.
diff --git a/coq/src/putnam_1997_a5.v b/coq/src/putnam_1997_a5.v
index d6404dfd..dfd754f0 100644
--- a/coq/src/putnam_1997_a5.v
+++ b/coq/src/putnam_1997_a5.v
@@ -2,7 +2,7 @@ Require Import Nat Ensembles Finite_sets List Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1997_a5_solution := True.
 Theorem putnam_1997_a5
-    (E: Ensemble (list nat) := fun l => length l = 10%nat /\ sum_n (fun i => 1/ INR (nth i l 0%nat)) 10 = 1)
+    (E: Ensemble (list nat) := fun l => length l = 10%nat /\ (forall i : nat, lt i 10 -> gt (nth i l 0%nat) 0) /\ sum_n (fun i => 1/ INR (nth i l 0%nat)) 9 = 1)
     (m: nat)
-    : cardinal (list nat) E m /\ odd m = true <-> putnam_1997_a5_solution.
+    : cardinal (list nat) E m -> (odd m = true <-> putnam_1997_a5_solution).
 Proof. Admitted.
diff --git a/coq/src/putnam_1997_a6.v b/coq/src/putnam_1997_a6.v
index df96f5da..d4ed81b6 100644
--- a/coq/src/putnam_1997_a6.v
+++ b/coq/src/putnam_1997_a6.v
@@ -1,15 +1,16 @@
 Require Import Binomial Nat Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1997_a6_solution (n k: nat) := Binomial.C (n - 1) (k - 1).
+Definition putnam_1997_a6_solution : nat -> nat -> R := (fun n k : nat => Binomial.C (n - 1) (k - 1)).
 Theorem putnam_1997_a6
-    (X := fix x (n: nat) (c: R) (k: nat) : R :=
+    (n : nat)
+    (maxc : R)
+    (X := fix x (c: R) (k: nat) : R :=
         match k with
         | O => 0 
         | S O => 1 
-        | S ((S k'') as k') => (c * x n c k' - INR (n - k) * x n c k'') / INR k'
+        | S ((S k'') as k') => (c * x c k' - INR (n - k) * x c k'') / INR k'
     end)
-    : forall (n: nat), exists (maxc: R), forall (c: R),
-    X n c (S n) = 0 /\ X n maxc (S n) = 0 -> c <= maxc ->
-    forall (k: nat), and (le 1 k) (le k n) -> 
-    X n c k = putnam_1997_a6_solution n k.
+    (npos : gt n 0)
+    (hmaxc : X maxc (add n 1) = 0 /\ (forall c : R, X c (add n 1) = 0 -> c <= maxc))
+    : forall (k: nat), (le 1 k /\ le k n) -> X maxc k = putnam_1997_a6_solution n k.
 Proof. Admitted.
diff --git a/coq/src/putnam_1997_b1.v b/coq/src/putnam_1997_b1.v
index 0d29d7c8..6b1f602f 100644
--- a/coq/src/putnam_1997_b1.v
+++ b/coq/src/putnam_1997_b1.v
@@ -1,7 +1,7 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1997_b1_solution (n: nat) := INR n.
+Definition putnam_1997_b1_solution : nat -> R := (fun n : nat => INR n).
 Theorem putnam_1997_b1
     (rnd : R -> R := fun x => Rmin (Rabs (IZR (floor x) - x)) (Rabs (IZR (floor (x + 1)) - x)))
-    : forall (n: nat), gt n 0 -> sum_n (fun m => Rmin (rnd ((INR m + 1) / (6 * INR n))) (rnd ((INR m + 1) / (3 * INR n)))) (6 * n - 1) = putnam_1997_b1_solution n.
+    : forall (n: nat), gt n 0 -> sum_n_m (fun m => Rmin (rnd (INR m / (6 * INR n))) (rnd (INR m / (3 * INR n)))) 1 (6 * n - 1) = putnam_1997_b1_solution n.
 Proof. Admitted.
diff --git a/coq/src/putnam_1997_b2.v b/coq/src/putnam_1997_b2.v
index 0a2cbe66..9ae3c651 100644
--- a/coq/src/putnam_1997_b2.v
+++ b/coq/src/putnam_1997_b2.v
@@ -1,7 +1,9 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1997_b2 
-    (f g: R -> R)
-    (habsbdd : R -> Prop := fun m => forall x, -m <= abs (f x) <= m)
-    : exists (M: R), forall (x: R), ex_derive_n f 2 x /\ g x >= 0 /\ f x + Derive_n f 2 x = -x * g x * Derive f x -> habsbdd M.
+    (f g : R -> R)
+    (hg : forall x : R, g x >= 0)
+    (hfdiff : forall x : R, ex_derive f x /\ ex_derive_n f 2 x)
+    (hfg : forall x : R, f x + Derive_n f 2 x = -x * g x * Derive f x)
+    : exists M : R, (forall x : R, -M <= abs (f x) <= M).
 Proof. Admitted.
diff --git a/coq/src/putnam_1997_b3.v b/coq/src/putnam_1997_b3.v
index 507fc747..d69d930d 100644
--- a/coq/src/putnam_1997_b3.v
+++ b/coq/src/putnam_1997_b3.v
@@ -1,7 +1,10 @@
 Require Import Reals Coquelicot.Coquelicot. From mathcomp Require Import div.
 Open Scope R.
-Definition putnam_1997_b3_solution (n: nat) := and (le 1 n) (le n 4) \/ and (le 20 n) (le n 24)  \/ and (le 100 n) (le n 104) \/ and (le 120 n) (le n 124).
+Definition putnam_1997_b3_solution : nat -> Prop := (fun n : nat => (le 1 n /\ le n 4) \/ (le 20 n /\ le n 24) \/ (le 100 n /\ le n 104) \/ (le 120 n /\ le n 124)).
 Theorem putnam_1997_b3
-    : forall (n: nat), gt n 0 -> exists (p q: nat), gt p 0 /\ gt q 0 /\ coprime p q = true /\
-    sum_n (fun m => 1 / INR (m + 1)) n = INR p / INR q -> neq (q mod 5) 0 -> putnam_1997_b3_solution n.
+    (n : nat)
+    (p q : nat)
+    (hn : gt n 0)
+    (hpq : gt p 0 /\ gt q 0 /\ coprime p q = true /\ sum_n_m (fun m => 1 / INR m) 1 n = INR p / INR q)
+    : neq (q mod 5) 0 <-> putnam_1997_b3_solution n.
 Proof. Admitted.
diff --git a/coq/src/putnam_1997_b4.v b/coq/src/putnam_1997_b4.v
deleted file mode 100644
index f1bbfb47..00000000
--- a/coq/src/putnam_1997_b4.v
+++ /dev/null
@@ -1,9 +0,0 @@
-Require Import Nat Reals Coquelicot.Coquelicot ZArith.
-Theorem putnam_1997_b4
-    (a : nat -> nat -> Z)
-    (max_degree : nat -> nat)
-    (coeff : nat -> (nat -> R))
-    (hpoly : forall (m : nat) (x : R), sum_n (fun i => (coeff m i) * (x^i)) (max_degree m) = (1 + x + x^2)^m)
-    (ha : forall n m : nat, IZR (a n m) = coeff m n)
-    : forall k : nat, ge k 0 -> 0 <= (sum_n (fun i => (-1)^i * (IZR (a (Nat.sub k i) i))) (Z.to_nat (Coquelicot.Rcomplements.floor (2 * INR k / 3)))) <= 1.
-Proof. Admitted.
diff --git a/coq/src/putnam_1997_b5.v b/coq/src/putnam_1997_b5.v
index b5573e3a..d6a5dbd5 100644
--- a/coq/src/putnam_1997_b5.v
+++ b/coq/src/putnam_1997_b5.v
@@ -1,9 +1,11 @@
 Require Import Nat.
-Theorem putnam_1997_b5 
-    (pown := fix pow_n (b n: nat) : nat :=
-      match n with
+Theorem putnam_1997_b5
+    (tetration := fix tetration' (b m: nat) : nat :=
+      match m with
       | O => 1
-      | S n' => b * pow_n b n'
+      | S m' => b ^ (tetration' b m')
     end)
-    : forall (n: nat), n >= 2 -> pown 2 n-1 mod n = pown 2 n-2.
+    (n : nat)
+    (hn : n >= 2)
+    : (tetration 2 n) mod n = (tetration 2 (n-1)) mod n.
 Proof. Admitted.
diff --git a/coq/src/putnam_1998_a3.v b/coq/src/putnam_1998_a3.v
index 2795812f..d974a3a7 100644
--- a/coq/src/putnam_1998_a3.v
+++ b/coq/src/putnam_1998_a3.v
@@ -1,6 +1,7 @@
-Require Import Reals Coquelicot.Derive.
+Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1998_a3
-    (f: R -> R)
-    : continuity (Derive_n f 3) -> exists (a: R), (Derive_n f 0) a * (Derive_n f 1) a * (Derive_n f 2) a * (Derive_n f 3) a >= 0.
+    (f : R -> R)
+    (hf : (forall x : R, ex_derive f x /\ ex_derive_n f 2 x /\ ex_derive_n f 3 x) /\ continuity (Derive_n f 3))
+    : exists (a: R), (Derive_n f 0) a * (Derive_n f 1) a * (Derive_n f 2) a * (Derive_n f 3) a >= 0.
 Proof. Admitted.
diff --git a/coq/src/putnam_1998_a4.v b/coq/src/putnam_1998_a4.v
index 86ef84c5..6a2f4284 100644
--- a/coq/src/putnam_1998_a4.v
+++ b/coq/src/putnam_1998_a4.v
@@ -1,13 +1,13 @@
 Require Import Nat ZArith Reals Coquelicot.Coquelicot.
 Open Scope nat_scope.
-Definition putnam_1998_a4_solution (n: nat) := exists (k: nat), n = 6 * k + 1.
+Definition putnam_1998_a4_solution : nat -> Prop := (fun n : nat => exists k : nat, n = 6 * k + 1).
 Theorem putnam_1998_a4
     (concatenate : nat -> nat -> nat := fun x y => Nat.pow 10 (Z.to_nat (floor (Rdiv (ln (INR y)) (ln 10))) + 1) * x + y)
     (a := fix A (n: nat) :=
         match n with
         | O => O
         | S O => 1
-        | S ((S n'') as n') => concatenate (A n') (A n'')
+        | S ((S n'') as n') => if eqb n'' O then 10 else (concatenate (A n') (A n''))
     end)
-    : forall (n: nat), a (n+1) mod 11 = 0 <-> putnam_1998_a4_solution n.
+    : forall (n: nat), n >= 1 -> ((a (n-1)) mod 11 = 0 <-> putnam_1998_a4_solution n).
 Proof. Admitted.
diff --git a/coq/src/putnam_1998_b1.v b/coq/src/putnam_1998_b1.v
index bab0f5ba..435d4ae2 100644
--- a/coq/src/putnam_1998_b1.v
+++ b/coq/src/putnam_1998_b1.v
@@ -1,10 +1,10 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1998_b1_solution := 1.
+Definition putnam_1998_b1_solution : R := 6.
 Theorem putnam_1998_b1
-    (f : R -> R := fun x => ((x + 1 / x) ^ 6 - (x ^ 6 + 1 / (x ^ 6)) - 2) / (x + 1 / x) ^ 3 + (x ^ 3 + 1 / (x ^ 3)))
+    (f : R -> R := fun x => ((x + 1 / x) ^ 6 - (x ^ 6 + 1 / (x ^ 6)) - 2) / ((x + 1 / x) ^ 3 + (x ^ 3 + 1 / (x ^ 3))))
     (m : R)
-    (hm : exists (x: R), x > 0 -> f x = m) 
+    (hm : exists (x: R), x > 0 /\ f x = m) 
     (hmub : forall (x: R), x > 0 -> f x >= m) 
     : m = putnam_1998_b1_solution.
 Proof. Admitted.
diff --git a/coq/src/putnam_1998_b4.v b/coq/src/putnam_1998_b4.v
index 6e5b137b..1aa7c323 100644
--- a/coq/src/putnam_1998_b4.v
+++ b/coq/src/putnam_1998_b4.v
@@ -1,5 +1,6 @@
 Require Import Nat ZArith Reals Coquelicot.Coquelicot.
-Definition putnam_1998_b4_solution (m n: nat) := exists (m2 n2: nat), m mod (2 ^ m2) = 0%nat /\ m mod (2 ^ (m2 + 1)) <> 0%nat /\ n mod (2 ^ n2) = 0%nat /\ n mod (2 ^ n2 + 1) <> 0%nat.
+Definition putnam_1998_b4_solution : nat -> nat -> Prop := (fun m n : nat => forall m2 n2 : nat, (m mod (2 ^ m2) = 0%nat /\ m mod (2 ^ (m2 + 1)) <> 0%nat /\ n mod (2 ^ n2) = 0%nat /\ n mod (2 ^ n2 + 1) <> 0%nat) -> m2 <> n2).
 Theorem putnam_1998_b4
-    : forall (m n: nat), sum_n (fun i =>  Rpower (-1) (IZR (floor (INR i / INR m)) + IZR (floor (INR i / INR n)))) (m * n - 1) = 0 <-> putnam_1998_b4_solution m n.
+    (hsum : nat -> nat -> R := (fun m n : nat => sum_n (fun i =>  Rpower (-1) (IZR (floor (INR i / INR m)) + IZR (floor (INR i / INR n)))) (m * n - 1)))
+    : forall (m n: nat), (gt m 0 /\ gt n 0) -> (hsum m n = 0 <-> putnam_1998_b4_solution m n).
 Proof. Admitted.
diff --git a/coq/src/putnam_1998_b5.v b/coq/src/putnam_1998_b5.v
index 43328c2e..ed5413da 100644
--- a/coq/src/putnam_1998_b5.v
+++ b/coq/src/putnam_1998_b5.v
@@ -2,6 +2,6 @@ Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1998_b5_solution : nat := 1.
 Theorem putnam_1998_b5
-    (N := sum_n (fun i => 10^i) 1998)
+    (N : R := sum_n (fun i => 10^i) 1997)
     : Z.to_nat (floor (10^1000 * sqrt N)) mod 10 = putnam_1998_b5_solution.
 Proof. Admitted.
diff --git a/coq/src/putnam_1998_b6.v b/coq/src/putnam_1998_b6.v
index 8f1426de..02abb8db 100644
--- a/coq/src/putnam_1998_b6.v
+++ b/coq/src/putnam_1998_b6.v
@@ -1,5 +1,6 @@
 Require Import Reals.
 Open Scope Z.
 Theorem putnam_1998_b6
-    : forall (a b c: Z), exists (n: Z), n > 0 -> forall (m : Z), n * n * n + a * n * n + b * n + c <> m * m.
+    (a b c : Z)
+    : exists (n: Z), n > 0 /\ (forall (m : Z), n * n * n + a * n * n + b * n + c <> m * m).
 Proof. Admitted.
diff --git a/isabelle/putnam_1996_a3.thy b/isabelle/putnam_1996_a3.thy
index 4a40223e..aefa598e 100644
--- a/isabelle/putnam_1996_a3.thy
+++ b/isabelle/putnam_1996_a3.thy
@@ -6,9 +6,11 @@ definition putnam_1996_a3_solution :: "bool" where
 "putnam_1996_a3_solution \<equiv> undefined"
 (* False *)
 theorem putnam_1996_a3:
-  fixes student_choices :: "nat \<Rightarrow> (nat set)"
-  assumes hinrange : "\<forall> n :: nat. student_choices n \<subseteq> {1..6}"
-  shows "putnam_1996_a3_solution \<longleftrightarrow> (\<exists> S :: nat set. S \<subseteq> {1::nat..20} \<and> card S = 5 \<and> (\<exists> c1 \<in> {1 :: nat..6}. \<exists> c2 \<in> {1 :: nat..6}. c1 \<noteq> c2 \<and> ({c1, c2} \<subseteq> (\<Inter> s \<in> S. student_choices s) \<or> {c1, c2} \<subseteq> (\<Inter> s \<in> S. UNIV - (student_choices s))) ))"
+  fixes studentchoicesinrange :: "(nat \<Rightarrow> (nat set)) \<Rightarrow> bool"
+  and studentchoicesprop :: "(nat \<Rightarrow> (nat set)) \<Rightarrow> bool"
+  defines "studentchoicesinrange \<equiv> (\<lambda>studentchoices::nat\<Rightarrow>(nat set). (\<forall>n::nat. studentchoices n \<subseteq> {1..6}))"
+  and "studentchoicesprop \<equiv> (\<lambda>studentchoices::nat\<Rightarrow>(nat set). (\<exists> S :: nat set. S \<subseteq> {1::nat..20} \<and> card S = 5 \<and> (\<exists> c1 \<in> {1 :: nat..6}. \<exists> c2 \<in> {1 :: nat..6}. c1 \<noteq> c2 \<and> ({c1, c2} \<subseteq> (\<Inter> s \<in> S. studentchoices s) \<or> {c1, c2} \<subseteq> (\<Inter> s \<in> S. (UNIV - studentchoices s))))))"
+  shows "(\<forall>studentchoices::nat\<Rightarrow>(nat set). studentchoicesinrange studentchoices \<longrightarrow> studentchoicesprop studentchoices) \<longleftrightarrow> putnam_1996_a3_solution"
   sorry
 
 end
\ No newline at end of file
diff --git a/isabelle/putnam_1996_a4.thy b/isabelle/putnam_1996_a4.thy
index ced9d8af..5b947aeb 100644
--- a/isabelle/putnam_1996_a4.thy
+++ b/isabelle/putnam_1996_a4.thy
@@ -1,15 +1,17 @@
 theory putnam_1996_a4 imports Complex_Main
+"HOL-Library.Cardinality"
 
 begin
 
 theorem putnam_1996_a4: 
-  fixes S :: "('A \<times> 'A \<times> 'A) set"
+  fixes S :: "('A::finite \<times> 'A \<times> 'A) set"
     and n :: "nat"
   assumes hA : "CARD('A) = n"
+    and hSdistinct: "\<forall>a b c::'A. ((a, b, c) \<in> S \<longrightarrow> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c))"
     and hS1 : " \<forall> a b c :: 'A. (a, b, c) \<in> S \<longleftrightarrow> (b, c, a) \<in> S"
     and hS2 : " \<forall> a b c :: 'A. (a, b, c) \<in> S \<longleftrightarrow> (c, b, a) \<notin> S"
     and hS3 : " \<forall> a b c d :: 'A. ((a, b, c) \<in> S \<and> (c, d, a) \<in> S) \<longleftrightarrow> ((b, c, d) \<in> S \<and> (d, a, b) \<in> S)"
-  shows "\<exists> g :: 'A \<Rightarrow> real. inj g \<and> (\<forall> a b c :: 'A. (g a < g b \<and> g c < g c) \<longrightarrow> (a, b, c) \<in> S)"
+  shows "\<exists> g :: 'A \<Rightarrow> real. inj g \<and> (\<forall> a b c :: 'A. (g a < g b \<and> g b < g c) \<longrightarrow> (a, b, c) \<in> S)"
   sorry
 
 end
\ No newline at end of file
diff --git a/isabelle/putnam_1996_a5.thy b/isabelle/putnam_1996_a5.thy
index 462cca65..2a355e31 100644
--- a/isabelle/putnam_1996_a5.thy
+++ b/isabelle/putnam_1996_a5.thy
@@ -1,5 +1,5 @@
 theory putnam_1996_a5 imports Complex_Main
-
+"HOL-Computational_Algebra.Primes"
 begin
 
 theorem putnam_1996_a5:
@@ -7,7 +7,7 @@ theorem putnam_1996_a5:
   defines "k \<equiv> nat \<lfloor>2 * p / 3\<rfloor>"
   assumes hpprime : "prime p"
     and hpge3 : "p > 3"
-  shows "p^2 dvd (\<Sum> i \<in> {1 :: nat..k}. p choose i)"
+  shows "(p^2) dvd (\<Sum> i \<in> {1 :: nat..k}. p choose i)"
   sorry
 
 end
\ No newline at end of file
diff --git a/isabelle/putnam_1996_b1.thy b/isabelle/putnam_1996_b1.thy
index 84749bff..00871feb 100644
--- a/isabelle/putnam_1996_b1.thy
+++ b/isabelle/putnam_1996_b1.thy
@@ -12,7 +12,7 @@ theorem putnam_1996_b1:
   and n :: nat
   defines "selfish \<equiv> \<lambda> s. card s \<in> s"
   assumes npos: "n \<ge> 1"
-  shows "card {s :: nat set. s \<subseteq> {1..n} \<and> selfish s \<and> (\<forall> ss :: nat set. ss \<subseteq> s \<longrightarrow> \<not>selfish ss)} = putnam_1996_b1_solution n"
+  shows "card {s :: nat set. s \<subseteq> {1..n} \<and> selfish s \<and> (\<forall> ss :: nat set. ss \<subset> s \<longrightarrow> \<not>selfish ss)} = putnam_1996_b1_solution n"
   sorry
 
 end
\ No newline at end of file
diff --git a/isabelle/putnam_1996_b3.thy b/isabelle/putnam_1996_b3.thy
index 38a88845..1d5893e8 100644
--- a/isabelle/putnam_1996_b3.thy
+++ b/isabelle/putnam_1996_b3.thy
@@ -3,7 +3,7 @@ Complex_Main
 begin
 
 definition putnam_1996_b3_solution :: "nat \<Rightarrow> nat" where "putnam_1996_b3_solution \<equiv> undefined"
-(* \<lambda> n :: nat. (2 * n ^ 3 + 3 * n ^ 2 - 11 * n + 18) div 6 *) 
+(* \<lambda> n :: nat. (2 * n ^ 3 + 3 * n ^ 2 + 18 - 11 * n) div 6 *)
 theorem putnam_1996_b3:
   fixes n :: nat
   and xset :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
diff --git a/isabelle/putnam_1996_b4.thy b/isabelle/putnam_1996_b4.thy
index 53c06dff..1bbe06c9 100644
--- a/isabelle/putnam_1996_b4.thy
+++ b/isabelle/putnam_1996_b4.thy
@@ -11,7 +11,7 @@ theorem putnam_1996_b4:
   and matpow :: "real^2^2 \<Rightarrow> nat \<Rightarrow> real^2^2"
   defines "matsin \<equiv> \<lambda> A :: real^2^2. \<Sum> n :: nat. ((-1) ^ n / fact (2 * n + 1)) *\<^sub>R (matpow A (2 * n + 1))"
   and "mat1996 \<equiv> \<chi> i j. if i = 1 then (if j = 1 then 1 else 1996) else (if j = 1 then 0 else 1)"  
-  assumes hmatpow: "\<forall> A :: real^2^2. matpow A 0 = mat 1 \<and> (\<forall> k :: nat. matpow A (k + 1) = A * (matpow A k))"
+  assumes hmatpow: "\<forall> A :: real^2^2. matpow A 0 = mat 1 \<and> (\<forall> k :: nat. matpow A (k + 1) = A ** (matpow A k))"
   shows "(\<exists> A :: real^2^2. matsin A = mat1996) \<longleftrightarrow> putnam_1996_b4_solution"
   sorry
 
diff --git a/isabelle/putnam_1997_a5.thy b/isabelle/putnam_1997_a5.thy
index ca372927..2d353e29 100644
--- a/isabelle/putnam_1997_a5.thy
+++ b/isabelle/putnam_1997_a5.thy
@@ -5,8 +5,7 @@ definition putnam_1997_a5_solution where "putnam_1997_a5_solution \<equiv> undef
 (* True *)
 theorem putnam_1997_a5:
   fixes N::"nat\<Rightarrow>nat"
-  defines "N \<equiv> \<lambda>n. card {t::nat list. (size t = n) \<and> (\<forall>i \<in> {0..<n}. t!i > 0) \<and> (\<forall>i \<in> {0..<n}. \<forall>j \<in> {0..<n}. i < j \<longrightarrow> t!i \<le> t!j) 
-    \<and> (\<Sum>i=0..<n. 1 / (t!i)) = 1}"
+  defines "N \<equiv> \<lambda>n. card {t::nat list. (size t = n) \<and> (\<forall>i \<in> {0..<n}. t!i > 0) \<and> (\<Sum>i=0..<n. 1 / (t!i)) = 1}"
   shows "odd (N 10) \<longleftrightarrow> putnam_1997_a5_solution"
   sorry
 
diff --git a/isabelle/putnam_1997_a6.thy b/isabelle/putnam_1997_a6.thy
index 7f02a57f..47108332 100644
--- a/isabelle/putnam_1997_a6.thy
+++ b/isabelle/putnam_1997_a6.thy
@@ -2,13 +2,13 @@ theory putnam_1997_a6 imports Complex_Main
 
 begin
 
-definition putnam_1997_a6_solution :: "int \<Rightarrow> int \<Rightarrow> real" where
+definition putnam_1997_a6_solution :: "nat \<Rightarrow> nat \<Rightarrow> real" where
 "putnam_1997_a6_solution \<equiv> undefined"
-(* \<lambda> n k. (nat n-1) choose (nat k-1) *)
+(* \<lambda> n k. (n-1) choose (k-1) *)
 theorem putnam_1997_a6:
-  fixes n :: "int"
+  fixes n :: "nat"
     and C :: "real"
-    and x :: "real \<Rightarrow> (int \<Rightarrow> real)"
+    and x :: "real \<Rightarrow> (nat \<Rightarrow> real)"
     and S :: "real set"
   defines "S \<equiv> {c :: real. x c (n + 1) = 0}"
   assumes hx0 : "\<forall> c :: real. x c 0 = 0"
diff --git a/isabelle/putnam_1997_b2.thy b/isabelle/putnam_1997_b2.thy
index 3a189eda..158db71b 100644
--- a/isabelle/putnam_1997_b2.thy
+++ b/isabelle/putnam_1997_b2.thy
@@ -6,9 +6,9 @@ begin
 theorem putnam_1997_b2:
   fixes f g :: "real \<Rightarrow> real"
   assumes hg : "\<forall> x :: real. g x \<ge> 0"
-    and hfdiff : "(f differentiable_on UNIV) \<and> (deriv f) differentiable_on UNIV"
+    and hfdiff : "(f C1_differentiable_on UNIV) \<and> (deriv f) differentiable_on UNIV"
     and hfg : "\<forall> x :: real. f x + (deriv^^2) f x = -x * g x * (deriv f x)"
-  shows "bounded (image f UNIV)"
+  shows "bounded (image (\<lambda>x::real. \<bar>f x\<bar>) UNIV)"
   sorry
 
 end
diff --git a/isabelle/putnam_1997_b4.thy b/isabelle/putnam_1997_b4.thy
index 16d43ce3..0f7d1526 100644
--- a/isabelle/putnam_1997_b4.thy
+++ b/isabelle/putnam_1997_b4.thy
@@ -5,8 +5,8 @@ begin
 
 theorem putnam_1997_b4:
   fixes a :: "nat \<Rightarrow> nat \<Rightarrow> int"
-  assumes ha : "\<forall> n m :: nat. a n m = coeff ((monom 1 0 + monom 1 1 + monom 1 2)^m) n"
-  shows "\<forall> k :: nat \<ge> 0. (\<Sum> i \<in> {0..nat \<lfloor>((2*(rat_of_nat k)))/(rat_of_nat 3)\<rfloor>}. (-1)^(i) * (a (k-i) i)) \<in> {0 :: real..1}" 
+  assumes ha : "\<forall> m n :: nat. a m n = coeff ((monom 1 0 + monom 1 1 + monom 1 2)^m) n"
+  shows "\<forall> k :: nat \<ge> 0. (\<Sum> i \<in> {0..nat \<lfloor>(2*(rat_of_nat k))/(rat_of_nat 3)\<rfloor>}. (-1)^i * (a (k-i) i)) \<in> {0 :: real..1}" 
   sorry
 
 end
\ No newline at end of file
diff --git a/isabelle/putnam_1997_b5.thy b/isabelle/putnam_1997_b5.thy
index 0ab9f2ba..16b69d1f 100644
--- a/isabelle/putnam_1997_b5.thy
+++ b/isabelle/putnam_1997_b5.thy
@@ -8,7 +8,7 @@ theorem putnam_1997_b5:
     and tetration :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   assumes hn : "n \<ge> 2"
     and htetrationbase : "\<forall> a :: nat. tetration a 0 = 1"
-    and htetration : "\<forall> a n :: nat. tetration a (n+1) = a^(tetration a n)"
+    and htetration : "\<forall> a m :: nat. tetration a (m+1) = a^(tetration a m)"
   shows "[tetration 2 n = tetration 2 (n-1)] (mod n)"
   sorry
 
diff --git a/isabelle/putnam_1998_a3.thy b/isabelle/putnam_1998_a3.thy
index 20ec53d7..c43dbb58 100644
--- a/isabelle/putnam_1998_a3.thy
+++ b/isabelle/putnam_1998_a3.thy
@@ -4,7 +4,7 @@ begin
 
 theorem putnam_1998_a3:
   fixes f :: "real \<Rightarrow> real"
-  assumes hf : "continuous_on UNIV ((deriv^^3) f)"
+  assumes hf : "\<forall>n::nat\<in>{0..2}. ((deriv^^n) f) C1_differentiable_on UNIV"
   shows "\<exists> a :: real. f a * deriv f a * (deriv^^2) f a * (deriv^^3) f a \<ge> 0"
   sorry
 
diff --git a/isabelle/putnam_1998_a4.thy b/isabelle/putnam_1998_a4.thy
index df39cb3a..f934ca44 100644
--- a/isabelle/putnam_1998_a4.thy
+++ b/isabelle/putnam_1998_a4.thy
@@ -12,7 +12,7 @@ theorem putnam_1998_a4:
   assumes hA1 : "A 1 = 0"
     and hA2 : "A 2 = 1"
     and hA : "\<forall>n::nat > 2. A n = from_digits (digits (A (n-2)) @ digits (A (n-1)))"
-  shows "putnam_1998_a4_solution = {n::nat. 11 dvd (A n)}"
+  shows "putnam_1998_a4_solution = {n::nat. n \<ge> 1 \<and> 11 dvd (A n)}"
   sorry
 
 end
\ No newline at end of file
diff --git a/isabelle/putnam_1998_a5.thy b/isabelle/putnam_1998_a5.thy
index 66e45d94..ccda9151 100644
--- a/isabelle/putnam_1998_a5.thy
+++ b/isabelle/putnam_1998_a5.thy
@@ -6,7 +6,8 @@ theorem putnam_1998_a5:
   fixes k::nat and c::"nat \<Rightarrow> (real \<times> real)" and r::"nat \<Rightarrow> real" and E::"(real \<times> real) set"
   assumes hr : "\<forall>i \<in> {0..<k}. r i  > 0"
     and hE : "E \<subseteq> (\<Union> i \<in> {0..<k}. ball (c i) (r i))"
-  shows "\<exists>n::nat. \<exists>t::nat\<Rightarrow>nat. (\<forall>i \<in> {0..<n}. \<forall>j \<in> {0..<n}. i \<noteq> j \<longrightarrow> ((ball (c (t i)) (r (t i)) \<inter> (ball (c (t j)) (r (t j))) = {}))) 
+  shows "\<exists>n::nat. \<exists>t::nat\<Rightarrow>nat. n \<le> k \<and> t ` {0..<n} \<subseteq> {0..<k}
+    \<and> (\<forall>i \<in> {0..<n}. \<forall>j \<in> {0..<n}. i \<noteq> j \<longrightarrow> ((ball (c (t i)) (r (t i)) \<inter> (ball (c (t j)) (r (t j))) = {}))) 
     \<and> E \<subseteq> (\<Union> i \<in> {0..<n}. ball (c (t i)) (3 * (r (t i))))"
   sorry
 
diff --git a/isabelle/putnam_1998_b1.thy b/isabelle/putnam_1998_b1.thy
index d9b2207c..e60510b2 100644
--- a/isabelle/putnam_1998_b1.thy
+++ b/isabelle/putnam_1998_b1.thy
@@ -4,7 +4,7 @@ begin
 definition putnam_1998_b1_solution::real where "putnam_1998_b1_solution \<equiv> undefined"
 (* 6 *)
 theorem putnam_1998_b1:
-  shows "putnam_1998_b1_solution = (LEAST y. (\<exists>x::real > 0. y = ((x+1/x)^6 - (x^6 + 1/x^6) - 2) / ((x+1/x)^3 + (x^3 +1/x^3))))"
+  shows "putnam_1998_b1_solution = (LEAST y. (\<exists>x::real > 0. y = ((x+1/x)^6 - (x^6 + 1/x^6) - 2) / ((x+1/x)^3 + (x^3 + 1/x^3))))"
   sorry
 
 end
\ No newline at end of file
diff --git a/isabelle/putnam_1998_b2.thy b/isabelle/putnam_1998_b2.thy
index aff1fab6..48cae443 100644
--- a/isabelle/putnam_1998_b2.thy
+++ b/isabelle/putnam_1998_b2.thy
@@ -6,7 +6,7 @@ definition putnam_1998_b2_solution::"real\<Rightarrow>real\<Rightarrow>real" whe
 theorem putnam_1998_b2:
   fixes a b::real
   assumes hab : "0 < b \<and> b < a"
-  shows "putnam_1998_b2_solution a b = (LEAST p. \<exists>c x::real. p = dist (a, b) (c, 0) + dist (c, 0) (x, x) + dist (a, b) (x, x) \<and> 
+  shows "putnam_1998_b2_solution a b = (LEAST p::real. \<exists>c x::real. p = dist (a, b) (c, 0) + dist (c, 0) (x, x) + dist (a, b) (x, x) \<and> 
     dist (a, b) (c, 0) + dist (c, 0) (x, x) > dist (a, b) (x, x) \<and>
     dist (a, b) (c, 0) + dist (a, b) (x, x) > dist (c, 0) (x, x) \<and>
     dist (c, 0) (x, x) + dist (a, b) (x, x) > dist (a, b) (c, 0))"
diff --git a/isabelle/putnam_1998_b4.thy b/isabelle/putnam_1998_b4.thy
index 282c2a73..41a33573 100644
--- a/isabelle/putnam_1998_b4.thy
+++ b/isabelle/putnam_1998_b4.thy
@@ -2,11 +2,11 @@ theory putnam_1998_b4 imports Complex_Main "HOL-Computational_Algebra.Factorial_
 begin
 
 definition putnam_1998_b4_solution::"nat\<Rightarrow>nat\<Rightarrow>bool" where "putnam_1998_b4_solution \<equiv> undefined"
-(* \<lambda>n. \<lambda>m. multiplicity 2 n \<noteq> multiplicity 2 m *)
+(* (\<lambda>m n::nat. (GREATEST i::nat. 2^i dvd m) \<noteq> (GREATEST i::nat. 2^i dvd n)) *)
 theorem putnam_1998_b4:
   fixes hsum::"nat\<Rightarrow>nat\<Rightarrow>int"
-  defines "hsum \<equiv> \<lambda>n. \<lambda>m. (\<Sum>i=0..<m*n. (-1)^(i div m + i div n))"
-  shows "\<forall>n m::nat. n > 0 \<and> m > 0 \<longrightarrow> (hsum n m = 0 \<longleftrightarrow> putnam_1998_b4_solution n m)"
+  defines "hsum \<equiv> \<lambda>m. \<lambda>n. (\<Sum>i::nat=0..<m*n. (-1)^(i div m + i div n))"
+  shows "\<forall>m n::nat. m > 0 \<and> n > 0 \<longrightarrow> (hsum m n = 0 \<longleftrightarrow> putnam_1998_b4_solution m n)"
   sorry
 
 end
\ No newline at end of file
diff --git a/lean4/src/putnam_1996_a3.lean b/lean4/src/putnam_1996_a3.lean
index 5a450a97..759398d4 100644
--- a/lean4/src/putnam_1996_a3.lean
+++ b/lean4/src/putnam_1996_a3.lean
@@ -4,6 +4,6 @@ open BigOperators
 abbrev putnam_1996_a3_solution : Prop := sorry
 -- False
 theorem putnam_1996_a3
-(student_choices : Finset.range 20 → Set (Finset.range 6))
-: putnam_1996_a3_solution ↔ ∃ S : Set (Finset.range 20), ∃ c1 c2 : Finset.range 6, c1 ≠ c2 ∧ S.ncard = 5 ∧ ({c1, c2} ⊆ ⋂ s ∈ S, student_choices s ∨ ({c1, c2} ⊆ ⋂ s ∈ S, (student_choices s)ᶜ)) :=
+(studentchoicesprop : (Finset.range 20 → Set (Finset.range 6)) → Prop := (fun studentchoices : (Finset.range 20 → Set (Finset.range 6)) => ∃ S : Set (Finset.range 20), ∃ c1 c2 : Finset.range 6, c1 ≠ c2 ∧ S.encard = 5 ∧ ({c1, c2} ⊆ (⋂ s ∈ S, studentchoices s) ∨ {c1, c2} ⊆ (⋂ s ∈ S, (studentchoices s)ᶜ))))
+: (∀ studentchoices : (Finset.range 20 → Set (Finset.range 6)), studentchoicesprop studentchoices) ↔ putnam_1996_a3_solution :=
 sorry
diff --git a/lean4/src/putnam_1997_b5.lean b/lean4/src/putnam_1997_b5.lean
index 0f5bcc79..e9e15a7a 100644
--- a/lean4/src/putnam_1997_b5.lean
+++ b/lean4/src/putnam_1997_b5.lean
@@ -5,7 +5,7 @@ open Filter Topology Bornology Set Polynomial
 
 def tetration : ℕ → ℕ → ℕ
   | _, 0 => 1
-  | m, (n + 1) => m^(tetration m n)
+  | b, (m + 1) => b^(tetration b m)
 theorem putnam_1997_b5
 (n : ℕ)
 (hn : n ≥ 2)
diff --git a/lean4/src/putnam_1998_a4.lean b/lean4/src/putnam_1998_a4.lean
index ea0902e4..52c41954 100644
--- a/lean4/src/putnam_1998_a4.lean
+++ b/lean4/src/putnam_1998_a4.lean
@@ -9,5 +9,5 @@ theorem putnam_1998_a4
 (hA1 : A 1 = 0)
 (hA2 : A 2 = 1)
 (hA : ∀ n : ℕ, n > 2 → A n = Nat.ofDigits 10 (Nat.digits 10 (A (n - 2)) ++ Nat.digits 10 (A (n - 1))))
-: putnam_1998_a4_solution = {n | 11 ∣ A n} :=
+: putnam_1998_a4_solution = {n | n ≥ 1 ∧ (11 ∣ A n)} :=
 sorry
diff --git a/lean4/src/putnam_2019_b1.lean b/lean4/src/putnam_2019_b1.lean
index ce85b109..916eb5c6 100644
--- a/lean4/src/putnam_2019_b1.lean
+++ b/lean4/src/putnam_2019_b1.lean
@@ -8,10 +8,10 @@ abbrev putnam_2019_b1_solution : ℕ → ℕ := sorry
 theorem putnam_2019_b1
 (n : ℕ)
 (Pn : Set (Fin 2 → ℤ))
-(pZtoR : (Fin 2 → ℤ) → (Fin 2 → ℝ))
+(pZtoR : (Fin 2 → ℤ) → EuclideanSpace ℝ (Fin 2))
 (sPnsquare : Finset (Fin 2 → ℤ) → Prop)
 (hPn : Pn = {p : Fin 2 → ℤ | (p 0 = 0 ∧ p 1 = 0) ∨ (∃ k ≤ n, (p 0) ^ 2 + (p 1) ^ 2 = 2 ^ k)})
 (hpZtoR : ∀ p : Fin 2 → ℤ, ∀ i : Fin 2, (pZtoR p) i = p i)
-(hsPnsquare : ∀ sPn : Finset (Fin 2 → ℤ), sPnsquare sPn = (sPn.card = 4 ∧ ∃ p4 : Fin 4 → (Fin 2 → ℤ), Set.range p4 = sPn ∧ (∃ s > 0, ∀ i : Fin 4, Euclidean.dist (pZtoR (p4 i)) (pZtoR (p4 (i + 1))) = s) ∧ (Euclidean.dist (pZtoR (p4 0)) (pZtoR (p4 2)) = Euclidean.dist (pZtoR (p4 1)) (pZtoR (p4 3)))))
+(hsPnsquare : ∀ sPn : Finset (Fin 2 → ℤ), sPnsquare sPn = (sPn.card = 4 ∧ ∃ p4 : Fin 4 → (Fin 2 → ℤ), Set.range p4 = sPn ∧ (∃ s > 0, ∀ i : Fin 4, dist (pZtoR (p4 i)) (pZtoR (p4 (i + 1))) = s) ∧ (dist (pZtoR (p4 0)) (pZtoR (p4 2)) = dist (pZtoR (p4 1)) (pZtoR (p4 3)))))
 : {sPn : Finset (Fin 2 → ℤ) | (sPn : Set (Fin 2 → ℤ)) ⊆ Pn ∧ sPnsquare sPn}.encard = putnam_2019_b1_solution n :=
 sorry