diff --git a/coq/src/commented_problems.v b/coq/src/commented_problems.v
index dae049dc..288456a9 100644
--- a/coq/src/commented_problems.v
+++ b/coq/src/commented_problems.v
@@ -78,6 +78,37 @@ Theorem putnam_2010_a5:
 Proof. Admitted.
 End putnam_2010_a5. *)
 
+(* From mathcomp Require Import matrix ssralg ssrbool.
+Open Scope ring_scope.
+Definition putnam_1991_a2_solution := False.
+Theorem putnam_1991_a2
+    (R : comUnitRingType) 
+    (n : nat) 
+    (npos : n >= 1)
+    : (exists A B : 'M[R]_n, A <> B /\ mulmx (mulmx A A) A = mulmx (mulmx B B) B /\
+    mulmx (mulmx A A) B = mulmx (mulmx B B) A /\
+    (mulmx A A + mulmx B B) \in unitmx) <-> putnam_1991_a2_solution.
+Proof. Admitted. *)
+
+(* From mathcomp Require Import ssrnat ssrnum ssralg poly polydiv seq.
+Open Scope ring_scope.
+Definition putnam_1992_b4_solution := 3984%nat.
+Theorem putnam_1992_b4
+    (R : numDomainType)
+    (itercomp := fix iter (f : {poly R} * {poly R} -> {poly R} * {poly R}) (n : nat) (p : {poly R} * {poly R}) : {poly R} * {poly R} :=
+        match n with
+        | O => p
+        | S n' => f (iter f n' p)
+    end)
+    (qr : {poly R} * {poly R} -> {poly R} * {poly R} := fun duple => (deriv (fst duple) * snd duple - deriv (snd duple) * fst duple, snd duple * snd duple))
+    (valid : {poly R} -> Prop := fun p => p <> 0 /\ lt (size p) 1992 /\ exists c : R, gcdp_rec p ('X^3 - 'X) = polyC c)
+    (twople : {poly R} -> {poly R} -> Prop := fun p f => exists g : {poly R}, g * fst (itercomp qr 1992%nat (p, 'X^3 - 'X)) = f * snd (itercomp qr 1992%nat (p, 'X^3 - 'X)))
+    (min : nat)
+    (hmineq : exists p f : {poly R}, (valid p /\ twople p f) /\ size f = min)
+    (hminlb : forall p f : {poly R}, (valid p /\ twople p f) -> ge (size f) min)
+    : min = putnam_1992_b4_solution.
+Proof. Admitted. *)
+
 (* Require Import Reals 
 GeoCoq.Main.Tarski_dev.Ch16_coordinates_with_functions
 GeoCoq.Axioms.Definitions
diff --git a/coq/src/putnam_1991_a2.v b/coq/src/putnam_1991_a2.v
deleted file mode 100644
index e5ccf5e0..00000000
--- a/coq/src/putnam_1991_a2.v
+++ /dev/null
@@ -1,12 +0,0 @@
-From mathcomp Require Import matrix ssralg ssrbool.
-Open Scope ring_scope.
-Definition putnam_1991_a2_solution := False.
-Theorem putnam_1991_a2
-    (R : comUnitRingType) 
-    (n : nat) 
-    (A B : 'M[R]_n) 
-    (hAB : A <> B)
-    : mulmx (mulmx A A) A = mulmx (mulmx B B) B /\
-    mulmx (mulmx A A) B = mulmx (mulmx B B) A ->
-    (mulmx A A + mulmx B B) \in unitmx <-> putnam_1991_a2_solution.
-Proof. Admitted.
diff --git a/coq/src/putnam_1991_a3.v b/coq/src/putnam_1991_a3.v
index b0533016..c5ae4639 100644
--- a/coq/src/putnam_1991_a3.v
+++ b/coq/src/putnam_1991_a3.v
@@ -1,11 +1,14 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1991_a3_solution (coeff: nat -> R) (n: nat) : Prop := exists (A r1 r2: R), coeff = (fun x => match x with | O => A * r1 * r2 | S O => -A * (r1 + r2) | S (S O) => A | _ => 0 end) /\ n = 2%nat.
+Definition poly (coeff : nat -> R) (deg : nat) : R -> R := fun x : R => sum_n (fun i => coeff i * x ^ i) deg.
+Definition putnam_1991_a3_solution (coeff: nat -> R) : Prop := (forall n : nat, gt n 2 -> coeff n = 0) /\ exists (r1 r2 : R), r1 <> r2 /\ poly coeff 2 r1 = 0 /\ poly coeff 2 r2 = 0.
 Theorem putnam_1991_a3
-    (p: (nat -> R) -> nat -> (R -> R) := fun coeff n => (fun x => sum_n (fun i => coeff i * x ^ i) (n + 1)))
-    : forall (coeff: nat -> R) (n: nat), ge n 2 ->
-    (exists (r: nat -> R), 
-    (forall (i j: nat), lt i j -> r i < r j) /\
-    forall (i: nat), lt i n -> p coeff n (r i) = 0 /\ lt i (n - 1) -> (Derive (p coeff n)) ((r i + r (S i)) / 2) = 0) <->
-    putnam_1991_a3_solution coeff n.
+    (coeff : nat -> R)
+    (n : nat)
+    (hn : coeff n <> 0 /\ forall m : nat, gt m n -> coeff m = 0)
+    (hge : ge n 2)
+    : (exists (r: nat -> R), (forall i : nat, lt i (n - 1) -> r i < r (S i)) /\
+    (forall i : nat, lt i n -> poly coeff n (r i) = 0) /\ 
+    (forall i : nat, lt i (n - 1) -> (Derive (poly coeff n)) ((r i + r (S i)) / 2) = 0)) <->
+    putnam_1991_a3_solution coeff.
 Proof. Admitted.
diff --git a/coq/src/putnam_1991_a5.v b/coq/src/putnam_1991_a5.v
index c1634449..a1b7ea92 100644
--- a/coq/src/putnam_1991_a5.v
+++ b/coq/src/putnam_1991_a5.v
@@ -2,8 +2,6 @@ Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1991_a5_solution := 1/3.
 Theorem putnam_1991_a5
-    (m: R)
-    (hm : exists (y: R), 0 <= y <= 1 -> m >= RInt (fun x => sqrt (pow x 4 + pow (y - pow y 2) 2)) 0 y)
-    (hmub : forall (y: R), 0 <= y <= 1 -> m >= RInt (fun x => sqrt (pow x 4 + pow (y - pow y 2) 2)) 0 y)
-    : m = putnam_1991_a5_solution.
+    (f : R -> R := fun y : R => RInt (fun x => sqrt (pow x 4 + pow (y - pow y 2) 2)) 0 y)
+    : (exists (y : R), 0 <= y <= 1 /\ putnam_1991_a5_solution = f y) /\ (forall (y : R), 0 <= y <= 1 -> putnam_1991_a5_solution >= f y).
 Proof. Admitted.
diff --git a/coq/src/putnam_1991_b1.v b/coq/src/putnam_1991_b1.v
index 0a6ac09a..a4b3abdf 100644
--- a/coq/src/putnam_1991_b1.v
+++ b/coq/src/putnam_1991_b1.v
@@ -1,4 +1,4 @@
-Require Import Nat Coquelicot.Coquelicot.
+Require Import Nat.
 Open Scope nat_scope.
 Definition putnam_1991_b1_solution (A: nat) := exists (m: nat), A = pow m 2.
 Theorem putnam_1991_b1
@@ -8,5 +8,7 @@ Theorem putnam_1991_b1
         | O => A
         | S k' => a A k' + eS (a A k')
     end)
-    : forall (A: nat), A > 0 -> Lim_seq (fun k => Raxioms.INR (a_seq A k)) = Rdefinitions.R0 <-> putnam_1991_b1_solution A.
+    (A : nat)
+    (hA : gt A 0)
+    : (exists K c : nat, forall k : nat, k >= K -> a_seq A k = c) <-> putnam_1991_b1_solution A.
 Proof. Admitted.
diff --git a/coq/src/putnam_1991_b2.v b/coq/src/putnam_1991_b2.v
index c2800470..dfa31fa6 100644
--- a/coq/src/putnam_1991_b2.v
+++ b/coq/src/putnam_1991_b2.v
@@ -1,8 +1,10 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1991_b2
-    (f g: R -> R)
-    (hfg : ~ exists (c: R), f = (fun _ => c) \/ g = (fun _ => c) /\ forall x, ex_derive_n f 1 x /\ forall x, ex_derive_n g 1 x)
-    : forall (x y: R), f (x + y) = f x * f y - g x * g y /\ g (x + y) = f x * g y - g x * f y ->
-    Derive f 0 = 0 -> forall (x: R), pow (f x) 2 + pow (g x) 2 = 1.
+    (f g : R -> R)
+    (fgnconst : ~ exists (c : R), f = (fun _ => c) \/ g = (fun _ => c))
+    (fgdiff : forall x : R, ex_derive f x /\ ex_derive g x)
+    (fadd : forall x y : R, f (x + y) = f x * f y - g x * g y)
+    (gadd : forall x y : R, g (x + y) = f x * g y + g x * f y)
+    : Derive f 0 = 0 -> forall x : R, pow (f x) 2 + pow (g x) 2 = 1.
 Proof. Admitted.
diff --git a/coq/src/putnam_1991_b5.v b/coq/src/putnam_1991_b5.v
index 66c34012..202eee5d 100644
--- a/coq/src/putnam_1991_b5.v
+++ b/coq/src/putnam_1991_b5.v
@@ -4,8 +4,8 @@ Definition putnam_1991_b5_solution (p: nat) : nat := p / 4 + 1.
 Theorem putnam_1991_b5 
     (p: nat)
     (hp : odd p = true /\ prime (Z.of_nat p))
-    (A: Ensemble Z := fun z => exists (m: 'I_p), z = Z.of_nat (pow (nat_of_ord m) 2))
-    (B: Ensemble Z := fun z => exists (m: 'I_p), z = Z.of_nat (pow (nat_of_ord m) 2 + 1))
+    (A: Ensemble Z := fun z => exists (m: 'I_p), z = Z.of_nat (pow (nat_of_ord m) 2) mod (Z.of_nat p))
+    (B: Ensemble Z := fun z => exists (m: 'I_p), z = Z.of_nat (pow (nat_of_ord m) 2 + 1) mod (Z.of_nat p))
     (C : Ensemble Z := Intersection Z A B)
     : cardinal Z C (putnam_1991_b5_solution p).
 Proof. Admitted.
diff --git a/coq/src/putnam_1991_b6.v b/coq/src/putnam_1991_b6.v
index 42dcbdd3..5ad1af13 100644
--- a/coq/src/putnam_1991_b6.v
+++ b/coq/src/putnam_1991_b6.v
@@ -1,10 +1,10 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1991_b6_solution (a b : R) := IZR (floor (ln (a / b))). 
+Definition putnam_1991_b6_solution (a b : R) := Rabs (ln (a / b)). 
 Theorem putnam_1991_b6 
     (a b: R)
     (hab : a > 0 /\ b > 0)
-    (ineq_holds : R -> Prop := fun c => forall (u x: R), 0 < Rabs u <= c /\ 0 < x < 1 -> Rpower a x * Rpower b (1 - x) <= a * sinh (u * x) / sinh u + b * sinh (1 - x) / sinh u)
+    (ineq_holds : R -> Prop := fun c => forall (u x: R), 0 < Rabs u <= c /\ 0 < x < 1 -> Rpower a x * Rpower b (1 - x) <= a * sinh (u * x) / sinh u + b * sinh (u * (1 - x)) / sinh u)
     (c: R)
     (hc : ineq_holds c)
     (hcub : forall (x: R), ineq_holds x -> x <= c)
diff --git a/coq/src/putnam_1992_a1.v b/coq/src/putnam_1992_a1.v
index 9f227b69..39ba783f 100644
--- a/coq/src/putnam_1992_a1.v
+++ b/coq/src/putnam_1992_a1.v
@@ -1,6 +1,6 @@
-Require Import Basics.
+Require Import Basics ZArith.
+Open Scope Z_scope.
 Theorem putnam_1992_a1 
-    (f : nat -> nat) 
-    (hf : forall (n: nat), f (f n) = n /\ f (f (n + 2)) + 2 = n /\ f 0 = 1)
-    : f = (fun n => 1 - n).
+    (f : Z -> Z) 
+    : f = (fun n => 1 - n) <-> ((forall n : Z, f (f n) = n) /\ (forall n : Z, f (f (n + 2) + 2) = n) /\ f 0 = 1).
 Proof. Admitted.
diff --git a/coq/src/putnam_1992_a2.v b/coq/src/putnam_1992_a2.v
index c94fca1e..0a983be3 100644
--- a/coq/src/putnam_1992_a2.v
+++ b/coq/src/putnam_1992_a2.v
@@ -3,5 +3,5 @@ Open Scope R.
 Definition putnam_1992_a2_solution := 1992.
 Theorem putnam_1992_a2
     (C : R -> R := fun a => (Derive_n (fun x => Rpower (1 + x) a) 1992) 0 / INR (fact 1992))
-    : RInt (fun y => C( - y - 1 ) * (sum_n (fun k => 1 / (y + INR k)) 1992)) 0 1 = putnam_1992_a2_solution.
+    : RInt (fun y => C (-y - 1) * sum_n_m (fun k => 1 / (y + INR k)) 1 1992) 0 1 = putnam_1992_a2_solution.
 Proof. Admitted.
diff --git a/coq/src/putnam_1992_a3.v b/coq/src/putnam_1992_a3.v
index d813ae81..9174ec80 100644
--- a/coq/src/putnam_1992_a3.v
+++ b/coq/src/putnam_1992_a3.v
@@ -1,8 +1,8 @@
 Require Import Nat. From mathcomp Require Import div fintype perm ssrbool.
-Definition putnam_1992_a3_solution (x y n m: nat) := exists r, x = 2 ^ r /\ y = 2 ^ r /\ n = 2 * r /\ m = 2 * r + 1.
+Definition putnam_1992_a3_solution (x y n m: nat) := exists r, x = 2 ^ r /\ y = 2 ^ r /\ n = 2 * r + 1 /\ m = 2 * r.
 Theorem putnam_1992_a3
     (m : nat)
     (hm : m > 0)
-    (hnxy : nat -> nat -> nat -> Prop := fun n x y => n > 0 /\ x > 0 /\ y > 0 /\ coprime n m /\ pow (pow x 2 + pow y 2) m = pow (x * y) m)
-    : forall n x y, putnam_1992_a3_solution x y n m.
+    (hnxy : nat -> nat -> nat -> Prop := fun n x y => n > 0 /\ x > 0 /\ y > 0 /\ coprime n m /\ pow (pow x 2 + pow y 2) m = pow (x * y) n)
+    : forall n x y, putnam_1992_a3_solution x y n m <-> hnxy n x y.
 Proof. Admitted.
diff --git a/coq/src/putnam_1992_a4.v b/coq/src/putnam_1992_a4.v
index 49737e1f..710bc1dc 100644
--- a/coq/src/putnam_1992_a4.v
+++ b/coq/src/putnam_1992_a4.v
@@ -1,8 +1,9 @@
 Require Import Nat Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1992_a4_solution (k: nat) := if odd k then 0 else pow (-1) (k/2).
+Definition putnam_1992_a4_solution (k : nat) := if odd k then 0 else pow (-1) (k/2) * INR (fact k).
 Theorem putnam_1992_a4
-    (f : R -> R := fun n => (pow (1 / n) 2) / ((pow (1 / n) 2) + 1))
-    (df_0 : nat -> R := fun k => (Derive_n f k) 0)
-    : forall (k: nat), gt k 0 -> df_0 k = putnam_1992_a4_solution k.
+    (f : R -> R)
+    (hfdiff : forall k : nat, continuity (Derive_n f k) /\ forall x : R, ex_derive (Derive_n f k) x)
+    (hf : forall n : nat, gt n 0 -> f (1 / INR n) = (INR n)^2 / ((INR n)^2 + 1))
+    : forall (k : nat), gt k 0 -> (Derive_n f k) 0 = putnam_1992_a4_solution k.
 Proof. Admitted.
diff --git a/coq/src/putnam_1992_a5.v b/coq/src/putnam_1992_a5.v
index 640a7842..7034ce6c 100644
--- a/coq/src/putnam_1992_a5.v
+++ b/coq/src/putnam_1992_a5.v
@@ -1,5 +1,4 @@
 Require Import BinPos Nat ZArith.
-Definition putnam_1992_a5_solution := 1.
 Theorem putnam_1992_a5
     (k := fix count_ones (n : positive) : nat :=
         match n with
@@ -8,5 +7,5 @@ Theorem putnam_1992_a5
         | xI n' => 1 + count_ones n'
     end)
     (a : positive -> nat := fun n => (k n) mod 2)
-    : ~ exists (k m: nat), forall (j: nat), 0 <= j <= m - 1 -> a (Pos.of_nat (k + j)) = a (Pos.of_nat (k + m + j)) /\ a (Pos.of_nat (k + m + j)) = a (Pos.of_nat (k + 2 * m + j)).
+    : ~ exists (k m: nat), gt k 0 /\ gt m 0 /\ forall (j: nat), j <= m - 1 -> a (Pos.of_nat (k + j)) = a (Pos.of_nat (k + m + j)) /\ a (Pos.of_nat (k + m + j)) = a (Pos.of_nat (k + 2 * m + j)).
 Proof. Admitted.
diff --git a/coq/src/putnam_1992_b1.v b/coq/src/putnam_1992_b1.v
index 06255371..4b1ed442 100644
--- a/coq/src/putnam_1992_b1.v
+++ b/coq/src/putnam_1992_b1.v
@@ -2,10 +2,11 @@ Require Import Nat Ensembles Finite_sets Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1992_b1_solution (n: nat) := sub (mul 2 n) 3.
 Theorem putnam_1992_b1
-    (n : nat) 
-    (E : Ensemble R)
-    (AE_criterion : Ensemble R -> Ensemble R -> Prop := fun E AE => cardinal R E n /\ forall (m: R), AE m <-> exists (p q: R), E p /\ E q /\ m = (p + q) / 2)
-    : gt n 2 -> exists (minAE: nat), 
-    (forall (AE: Ensemble R) (szAE: nat), cardinal R AE szAE /\ cardinal R AE minAE -> ge szAE minAE) <->
-    minAE = putnam_1992_b1_solution n.
+    (n : nat)
+    (nge2 : ge n 2)
+    (A : Ensemble R -> Ensemble R := fun E : Ensemble R => fun x : R => exists a b : R, E a /\ E b /\ a <> b /\ (a + b) / 2 = x)
+    (min : nat)
+    (hmineq : exists E : Ensemble R, cardinal R E n /\ cardinal R (A E) min)
+    (hminlb : forall E : Ensemble R, cardinal R E n -> exists m : nat, le m min /\ cardinal R (A E) m)
+    : min = putnam_1992_b1_solution n.
 Proof. Admitted.
diff --git a/coq/src/putnam_1992_b4.v b/coq/src/putnam_1992_b4.v
deleted file mode 100644
index 113e7b7b..00000000
--- a/coq/src/putnam_1992_b4.v
+++ /dev/null
@@ -1,12 +0,0 @@
-From mathcomp Require Import ssrnat ssrnum ssralg poly polydiv seq.
-Open Scope ring_scope.
-Definition putnam_1992_b4_solution := 3984%nat.
-Theorem putnam_1992_b4
-    (R : numDomainType) 
-    (p : {poly R})
-    (cond : {poly R} -> {poly R} -> Prop := fun f g => derivn 1992 (p %/ ('X^3 - 'X)) = f %/ g)
-    : gt (size p) 1992 /\ exists c: R, gcdp_rec p ('X^3 - 'X) = polyC c ->
-    exists mindeg, ((forall (f g: {poly R}), cond f g /\ ge (size f) mindeg) /\ 
-    (exists (f g: {poly R}), cond f g /\ size f = mindeg)) <->
-    mindeg = putnam_1992_b4_solution.
-Proof. Admitted.
diff --git a/coq/src/putnam_1993_a2.v b/coq/src/putnam_1993_a2.v
index fdaee54c..d01051fa 100644
--- a/coq/src/putnam_1993_a2.v
+++ b/coq/src/putnam_1993_a2.v
@@ -2,8 +2,7 @@ Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1993_a2 
     (x : nat -> R)
-    (n : nat)
-    (hn : gt n 0)
-    : pow (x n) 2 - x (pred n) * x (S n) = 1 ->
-    exists (a: R), ge n 1 -> x (S n) = a * x n - x (pred n).
+    (xnonzero : forall n : nat, x n <> 0)
+    (hx : forall n : nat, ge n 1 -> pow (x n) 2 - x (pred n) * x (S n) = 1)
+    : exists a : R, forall n : nat, ge n 1 -> x (S n) = a * x n - x (pred n).
 Proof. Admitted.
diff --git a/coq/src/putnam_1993_a4.v b/coq/src/putnam_1993_a4.v
index 4e1c3c2b..7490d5a0 100644
--- a/coq/src/putnam_1993_a4.v
+++ b/coq/src/putnam_1993_a4.v
@@ -1,16 +1,13 @@
 Require Import List Bool Reals Peano_dec Coquelicot.Coquelicot.
 Open Scope nat_scope.
+Fixpoint s_sum (a : nat -> nat) (k : nat) (s : nat -> bool) : nat := 
+    match k with
+    | O => a 0
+    | S k' => (if s k then a k else 0) + s_sum a k' s
+    end.
 Theorem putnam_1993_a4 
-    (x y: list nat)
-    (hx : length x = 19)
-    (hy : length y = 93)
-    (hx2 : forall n : nat, In n x -> 1 < n <= 93)
-    (hy2 : forall n  : nat, In n y -> 1 < n <= 19)
-    : exists (presentx presenty : nat -> bool), 
-    sum_n (fun n => 
-        if ((existsb (fun i => if eq_nat_dec n i then true else false) x) && presentx n) 
-        then (INR n) else R0) 94 = 
-    sum_n (fun n => 
-        if ((existsb (fun i => if eq_nat_dec n i then true else false) y) && presenty n) 
-        then (INR n) else R0) 20. 
+    (x y : nat -> nat)
+    (hx : forall i : nat, i < 19 -> 1 <= x i <= 93)
+    (hy : forall j : nat, j < 93 -> 1 <= y j <= 19)
+    : exists (is js : nat -> bool), (exists i : nat, i < 19 /\ is i = true) /\ s_sum x 18 is = s_sum y 92 js.
 Proof. Admitted.
diff --git a/coq/src/putnam_1993_b1.v b/coq/src/putnam_1993_b1.v
index 667e1be7..291650f0 100644
--- a/coq/src/putnam_1993_b1.v
+++ b/coq/src/putnam_1993_b1.v
@@ -2,7 +2,6 @@ Require Import Reals.
 Open Scope R.
 Definition putnam_1993_b1_solution : nat := 3987.
 Theorem putnam_1993_b1
-    (cond : nat -> Prop := fun n => forall (m: nat), and (lt 0 m) (lt m 1993) -> exists (k: nat), INR m / 1993 < INR k / INR n < INR (m + 1) / 1994)
-    : exists (mn : nat), cond mn /\ forall (n: nat), cond n -> ge n mn <->
-    mn = putnam_1993_b1_solution.
+    (cond : nat -> Prop := fun n => gt n 0 /\ forall (m: nat), and (lt 0 m) (lt m 1993) -> exists (k: nat), INR m / 1993 < INR k / INR n < INR (m + 1) / 1994)
+    : cond putnam_1993_b1_solution /\ forall (n: nat), cond n -> ge n putnam_1993_b1_solution.
 Proof. Admitted.
diff --git a/coq/src/putnam_1993_b4.v b/coq/src/putnam_1993_b4.v
index aa5c28a2..b14cea59 100644
--- a/coq/src/putnam_1993_b4.v
+++ b/coq/src/putnam_1993_b4.v
@@ -1,12 +1,10 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1993_b4 
-    (K: (R * R) -> R) 
-    (f g: R -> R)
-    (hK : forall (xy : R * R), let (x, y) := xy in 0 <= x <= 1 /\ 0 <= y <= 1 /\ K xy > 0 /\ continuous K xy)
-    (hfg : forall (x: R), 0 <= x <= 1 /\ f x > 0 /\ g x > 0 /\ continuity f /\ continuity g ->
-        forall (x: R), 0 <= x <= 1 -> 
-        (RInt (fun y => f y * K (x, y)) 0 1) = g x /\
-        RInt (fun y => g y * K (x, y)) 0 1 = f x)
-    : forall (x: R), 0 <= x <= 1 -> f x = g x.
+    (K : (R * R) -> R) 
+    (f g : R -> R)
+    (hK : forall x y : R, 0 <= x <= 1 /\ 0 <= y <= 1 -> K (x, y) > 0 /\ continuous K (x, y))
+    (hfg : forall x : R, 0 <= x <= 1 -> f x > 0 /\ g x > 0 /\ continuous f x /\ continuous g x /\
+        RInt (fun y => f y * K (x, y)) 0 1 = g x /\ RInt (fun y => g y * K (x, y)) 0 1 = f x)
+    : forall x : R, 0 <= x <= 1 -> f x = g x.
 Proof. Admitted.
diff --git a/coq/src/putnam_1994_a1.v b/coq/src/putnam_1994_a1.v
index f9f94852..98dfc946 100644
--- a/coq/src/putnam_1994_a1.v
+++ b/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.
diff --git a/coq/src/putnam_1994_b1.v b/coq/src/putnam_1994_b1.v
index 65b192be..2f71e027 100644
--- a/coq/src/putnam_1994_b1.v
+++ b/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.
\ No newline at end of file
diff --git a/coq/src/putnam_1994_b2.v b/coq/src/putnam_1994_b2.v
index 89d7d8e9..92480aeb 100644
--- a/coq/src/putnam_1994_b2.v
+++ b/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.
diff --git a/coq/src/putnam_1994_b3.v b/coq/src/putnam_1994_b3.v
index 0f5d0c4f..a5b53c17 100644
--- a/coq/src/putnam_1994_b3.v
+++ b/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.
diff --git a/coq/src/putnam_1994_b4.v b/coq/src/putnam_1994_b4.v
index 403c8adb..e00f0544 100644
--- a/coq/src/putnam_1994_b4.v
+++ b/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.
diff --git a/coq/src/putnam_1994_b5.v b/coq/src/putnam_1994_b5.v
index f09d181a..c5af0915 100644
--- a/coq/src/putnam_1994_b5.v
+++ b/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.
diff --git a/coq/src/putnam_1994_b6.v b/coq/src/putnam_1994_b6.v
index a2949c22..db6e5a42 100644
--- a/coq/src/putnam_1994_b6.v
+++ b/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.
diff --git a/coq/src/putnam_1995_a1.v b/coq/src/putnam_1995_a1.v
index 816fbecc..c69c3024 100644
--- a/coq/src/putnam_1995_a1.v
+++ b/coq/src/putnam_1995_a1.v
@@ -1,11 +1,11 @@
 Require Import Reals Ensembles Coquelicot.Coquelicot.
 Theorem putnam_1995_a1
-    (S T U : Ensemble R)
-    (hS : forall a : R, forall b : R, In _ S a /\ In _ S b -> In _ S (a * b))
-    (hsub : Included _ T S /\ Included _ U S)
-    (hunion : Same_set _ (Union _ T U) S)
+    (E T U : Ensemble R)
+    (hE : forall a : R, forall b : R, In _ E a /\ In _ E b -> In _ E (a * b))
+    (hsub : Included _ T E /\ Included _ U E)
+    (hunion : Same_set _ (Union _ T U) E)
     (hdisj : Disjoint _ T U)
     (hT3 : forall a b c : R, In _ T a /\ In _ T b /\ In _ T c -> In _ T (a * b * c))
-    (hS3 : forall a b c : R, In _ S a /\ In _ S b /\ In _ S c -> In _ S (a * b * c))
+    (hU3 : forall a b c : R, In _ U a /\ In _ U b /\ In _ U c -> In _ U (a * b * c))
     : (forall a b : R, In _ T a /\ In _ T b -> In _ T (a * b)) \/ (forall a b : R, In _ U a /\ In _ U b -> In _ U (a * b)).
 Proof. Admitted.
diff --git a/coq/src/putnam_1995_a2.v b/coq/src/putnam_1995_a2.v
index cafa7f43..4262c924 100644
--- a/coq/src/putnam_1995_a2.v
+++ b/coq/src/putnam_1995_a2.v
@@ -2,5 +2,5 @@ Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1995_a2_solution : R -> R -> Prop := fun (a b: R) => a = b.
 Theorem putnam_1995_a2
-    : forall (a b: R), a > 0 /\ b > 0 /\ ex_finite_lim_seq (fun n => RInt (fun x => sqrt (sqrt (x + a) - sqrt x) - sqrt (sqrt x - (x - b))) b (INR n)) <-> putnam_1995_a2_solution a b.
+    : forall (a b: R), a > 0 /\ b > 0 -> ((exists limit : R, filterlim (fun n : R => RInt (fun x => sqrt (sqrt (x + a) - sqrt x) - sqrt (sqrt x - (x - b))) b n) (Rbar_locally p_infty) (locally limit)) <-> putnam_1995_a2_solution a b).
 Proof. Admitted.
diff --git a/coq/src/putnam_1995_a4.v b/coq/src/putnam_1995_a4.v
index 80ac1618..e30a0c8f 100644
--- a/coq/src/putnam_1995_a4.v
+++ b/coq/src/putnam_1995_a4.v
@@ -1,9 +1,14 @@
-Require Import Reals ZArith Coquelicot.Coquelicot.
+Require Import Nat ZArith Coquelicot.Coquelicot.
+Open Scope Z_scope.
+Fixpoint Z_sum (a : nat -> Z) (k : nat) : Z := 
+    match k with
+    | O => a O
+    | S k' => a k + Z_sum a k'
+    end.
 Theorem putnam_1995_a4
     (n : nat)
     (hn : gt n 0)
-    (necklace : nat -> R)
-    (hnecklaceint : forall i : nat, exists k : Z, necklace i = IZR k)
-    (hnecklacesum : sum_n necklace n = INR n - 1)
-    : exists cut : nat, le cut (n-1) /\ (forall k : nat, le k (n-1) -> (sum_n (fun i => necklace ((cut + i) mod n)) k) <= INR k).
+    (necklace : nat -> Z)
+    (hnecklacesum : Z_sum necklace (n - 1) = (Z.of_nat n) - 1)
+    : exists cut : nat, le cut (n-1) /\ (forall k : nat, le k (n-1) -> (Z_sum (fun i => necklace (Nat.modulo (cut + i) n)) k) <= Z.of_nat k).
 Proof. Admitted.
diff --git a/coq/src/putnam_1995_a5.v b/coq/src/putnam_1995_a5.v
index 5ca09564..d0312b61 100644
--- a/coq/src/putnam_1995_a5.v
+++ b/coq/src/putnam_1995_a5.v
@@ -1,9 +1,9 @@
 Require Import Nat Reals Coquelicot.Coquelicot. From mathcomp Require Import fintype.
 Definition putnam_1995_a5_solution : Prop := True.
 Theorem putnam_1995_a5
-    (hdiffx := fun (n : nat) (x : nat -> (R -> R)) => forall (i : nat) (t : R), ge i 0 /\ le i (Nat.sub n 1) -> ex_derive (x i) t)
-    (ha := fun (n : nat) (a : nat -> nat -> R) => forall i j : nat, ge i 0 /\ le i (Nat.sub n 1) -> a i j > 0)
-    (hcomb := fun (n : nat) (x : nat -> (R -> R)) (a : nat -> nat -> R) => (forall t : R, forall i : nat, ge i 0 /\ le i (Nat.sub n 1) -> Derive (x i) t = sum_n (fun j => a i j * ((x j) t)) n))
-    (hxlim := fun (n : nat) (x : nat -> (R -> R)) =>  (forall i : nat, (ge i 0 /\ le i (Nat.sub n 1)) -> filterlim (x i) (Rbar_locally p_infty) (locally 0)))
-    : putnam_1995_a5_solution <-> (forall (n : nat) (x : nat -> (R -> R)) (a : nat -> nat -> R), (ge n 0 /\ hdiffx n x /\ ha n a /\ hcomb n x a /\ hxlim n x) -> ~(forall b : nat -> R, (forall t : R, 0 = sum_n (fun i => (b i) * ((x i) t)) (Nat.sub n 1)) -> (forall i : nat, (ge i 0 /\ le i (Nat.sub n 1)) -> b i = 0) )).
+    (hdiffx := fun (n : nat) (x : nat -> (R -> R)) => forall (i : nat) (t : R), le i (Nat.sub n 1) -> ex_derive (x i) t)
+    (ha := fun (n : nat) (a : nat -> nat -> R) => forall i j : nat, le i (Nat.sub n 1) /\ le j (Nat.sub n 1) -> a i j > 0)
+    (hcomb := fun (n : nat) (x : nat -> (R -> R)) (a : nat -> nat -> R) => (forall t : R, forall i : nat, le i (Nat.sub n 1) -> Derive (x i) t = sum_n (fun j => a i j * ((x j) t)) (n - 1)))
+    (hxlim := fun (n : nat) (x : nat -> (R -> R)) => (forall i : nat, le i (Nat.sub n 1) -> filterlim (x i) (Rbar_locally p_infty) (locally 0)))
+    : putnam_1995_a5_solution <-> (forall (n : nat) (x : nat -> (R -> R)) (a : nat -> nat -> R), (gt n 0 /\ hdiffx n x /\ ha n a /\ hcomb n x a /\ hxlim n x) -> ~(forall b : nat -> R, (forall t : R, 0 = sum_n (fun i => (b i) * ((x i) t)) (n - 1)) -> (forall i : nat, le i (Nat.sub n 1) -> b i = 0))).
 Proof. Admitted.
diff --git a/coq/src/putnam_1995_b4.v b/coq/src/putnam_1995_b4.v
index 794c361f..89fbd543 100644
--- a/coq/src/putnam_1995_b4.v
+++ b/coq/src/putnam_1995_b4.v
@@ -1,6 +1,9 @@
 Require Import Reals ZArith Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1995_b4_solution (a b c d: Z) := (a, b, c, d) = (3%Z,1%Z,5%Z,2%Z).
+Definition putnam_1995_b4_solution : Z * Z * Z * Z := (3%Z,1%Z,5%Z,2%Z).
 Theorem putnam_1995_b4
-    : exists (a b c d: Z), exists (contfrac: R), contfrac = 2207 - 1 / contfrac -> pow contfrac (1 / 8) = (IZR a + IZR b * sqrt (IZR c))/IZR d <-> putnam_1995_b4_solution a b c d.
+    (contfrac : R)
+    (hcontfrac : contfrac = 2207 - 1/contfrac)
+    : let (abc, d) := putnam_1995_b4_solution in let (ab, c) := abc in let (a, b) := ab in 
+    pow contfrac (1 / 8) = (IZR a + IZR b * sqrt (IZR c))/IZR d.
 Proof. Admitted.
diff --git a/coq/src/putnam_1995_b6.v b/coq/src/putnam_1995_b6.v
index 48603752..681cc04c 100644
--- a/coq/src/putnam_1995_b6.v
+++ b/coq/src/putnam_1995_b6.v
@@ -1,5 +1,5 @@
 Require Import Reals Ensembles Coquelicot.Coquelicot.
 Theorem putnam_1995_b6
-    (S : R -> Ensemble nat := fun alpha => (fun x : nat => exists n : nat, ge n 1 /\ INR x = IZR (floor ((INR n) * alpha))))
-    : ~ exists alpha beta gamma : R, alpha > 0 /\ beta > 0 /\ gamma > 0 /\ (Disjoint _ (S alpha) (S beta) /\ Disjoint _ (S beta) (S gamma) /\ Disjoint _ (S gamma) (S alpha)) /\ (~ Same_set _ (fun x : nat => ge x 1) (Union _ (Union _ (S alpha) (S beta)) (S gamma))).
+    (E : R -> Ensemble nat := fun alpha => fun x : nat => exists n : nat, ge n 1 /\ Z.of_nat x = floor (INR n * alpha))
+    : ~ exists alpha beta gamma : R, alpha > 0 /\ beta > 0 /\ gamma > 0 /\ (Disjoint _ (E alpha) (E beta) /\ Disjoint _ (E beta) (E gamma) /\ Disjoint _ (E gamma) (E alpha)) /\ (Same_set _ (fun x : nat => ge x 1) (Union _ (Union _ (E alpha) (E beta)) (E gamma))).
 Proof. Admitted.
diff --git a/coq/src/putnam_2004_a3.v b/coq/src/putnam_2004_a3.v
index 81dda05c..c44771f5 100644
--- a/coq/src/putnam_2004_a3.v
+++ b/coq/src/putnam_2004_a3.v
@@ -1,11 +1,7 @@
 Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_2004_a3
-    (U := fix u (n: nat) : R:=
-        match n with
-        | O => 1
-        | S O => 1
-        | S (S O) => 1
-        | S ((S (S n''') as n'') as n') => (INR (fact n) + u n'' * u n') / u n'''
-    end) 
-    : forall (n: nat), U n = IZR (floor (U n)).
+    (u : nat -> R)
+    (hubase : u O = 1 /\ u (S O) = 1 /\ u (S (S O)) = 1)
+    (hudet : forall n : nat, u n * u (Nat.add n 3) - u (Nat.add n 1) * u (Nat.add n 2) = INR (fact n))
+    : forall n : nat, exists m : Z, u n = IZR m.
 Proof. Admitted.
diff --git a/coq/src/putnam_2004_a4.v b/coq/src/putnam_2004_a4.v
index fd1366e2..34a141d7 100644
--- a/coq/src/putnam_2004_a4.v
+++ b/coq/src/putnam_2004_a4.v
@@ -1,6 +1,9 @@
-Require Import List Reals Coquelicot.Coquelicot.
+Require Import List Reals QArith Coquelicot.Coquelicot.
 Theorem putnam_2004_a4
-    : forall (n: nat), exists (N: nat) (a: nat -> nat -> R) (c: R), (exists (p q: Z), c = IZR (p / q)) /\ (forall (i j: nat), a i j = -1 \/ a i j = 0 \/ a i j = 1) ->
-    forall (x: list R), length x = n ->
-    fold_left Rmult x 1 = sum_n (fun i => c * (sum_n (fun j => a i j * nth j x 0) n) ^ (1 / n)) N.
+    (n : nat)
+    (x : list R)
+    (avals : nat -> (nat -> nat -> R) -> Prop := fun (N : nat) (a : nat -> nat -> R) => forall i j : nat, lt i N /\ lt j n -> a i j = -1 \/ a i j = 0 \/ a i j = 1)
+    (npos : gt n 0)
+    (hx : length x = n)
+    : exists (N : nat) (c : nat -> Q) (a : nat -> nat -> R), avals N a /\ fold_left Rmult x 1 = sum_n (fun i : nat => Q2R (c i) * (sum_n (fun j : nat => a i j * nth j x 0) (n - 1)) ^ n) (N - 1).
 Proof. Admitted.
\ No newline at end of file
diff --git a/coq/src/putnam_2004_a6.v b/coq/src/putnam_2004_a6.v
index 2c15d513..98dd8795 100644
--- a/coq/src/putnam_2004_a6.v
+++ b/coq/src/putnam_2004_a6.v
@@ -1,8 +1,7 @@
 Require Import Basics Reals Coquelicot.Coquelicot.
 Theorem putnam_2004_a6
     (f: R -> R -> R) 
-    (hf : forall x y : R, 0 <= x <= 1 /\ 0 <= y <= 1 /\ continuity_2d_pt f x y)
-    : RInt (compose (fun y => RInt (fun x => f x y) 0 1) (fun x => RInt (fun y => f x y) 0 1)) 0 1 + 
-    RInt (compose (fun x => RInt (fun y => f x y) 0 1) (fun x => RInt (fun y => f x y) 0 1)) 0 1 <= 
+    (hf : forall x y : R, (0 <= x <= 1 /\ 0 <= y <= 1) -> continuity_2d_pt f x y)
+    : RInt (fun y => (RInt (fun x => f x y) 0 1)^2) 0 1 + RInt (fun x => (RInt (fun y => f x y) 0 1)^2) 0 1 <= 
     (RInt (fun x => RInt (fun y => f x y) 0 1) 0 1) ^ 2 + RInt (fun x => RInt (fun y => (f x y) ^ 2) 0 1) 0 1.
 Proof. Admitted.
diff --git a/coq/src/putnam_2004_b1.v b/coq/src/putnam_2004_b1.v
index c3e8caeb..4bea800e 100644
--- a/coq/src/putnam_2004_b1.v
+++ b/coq/src/putnam_2004_b1.v
@@ -1,8 +1,8 @@
-Require Import Nat Reals Coquelicot.Coquelicot.
+Require Import Nat Reals QArith Coquelicot.Coquelicot.
 Theorem putnam_2004_b1
-    (c: nat -> Z)
-    (n: nat)
-    (P : R -> R := fun x => sum_n (fun i => IZR (c i) * x ^ i) (n + 1))
-    : forall (p q: Z), P (IZR (p / q)) = 0 -> let r := IZR (p / q) in
-    forall (i: nat), and (le 1 i) (le i n) -> sum_n (fun j => IZR (c (sub n j)) * r ^ (i - j)) i = IZR (floor (sum_n (fun j => IZR (c (sub n j)) * r ^ (i - j)) i)). 
+    (c : nat -> Z)
+    (n : nat)
+    (r : Q)
+    (Preq0 : sum_n (fun i => IZR (c i) * (Q2R r) ^ i) n = 0)
+    : forall i : nat, lt i n -> exists m : Z, IZR m = sum_n (fun j => IZR (c (sub n j)) * (Q2R r) ^ (i + 1 - j)) i. 
 Proof. Admitted.
diff --git a/coq/src/putnam_2004_b2.v b/coq/src/putnam_2004_b2.v
index f0f4888c..baa1c689 100644
--- a/coq/src/putnam_2004_b2.v
+++ b/coq/src/putnam_2004_b2.v
@@ -1,7 +1,6 @@
-Require Import Factorial Reals Coquelicot.Coquelicot.
+Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_2004_b2
-    (m n: nat)
-    (hm : ge m 0)
-    (hn : ge n 0)
+    (m n : nat)
+    (mnpos : gt m 0 /\ gt n 0)
     : INR (fact (m + n)) / INR (m + n) ^ (m + n) < INR (fact m) / INR m ^ m * INR (fact n) / INR n ^ n.
 Proof. Admitted.
diff --git a/coq/src/putnam_2004_b5.v b/coq/src/putnam_2004_b5.v
index f7df9487..5844b7b2 100644
--- a/coq/src/putnam_2004_b5.v
+++ b/coq/src/putnam_2004_b5.v
@@ -3,8 +3,8 @@ Definition putnam_2004_b5_solution := 2 / exp 1.
 Theorem putnam_2004_b5
     (prodn := fix prod_n (m: nat -> R) (n : nat) : R :=
         match n with
-        | O => m 0%nat
+        | O => 1
         | S n' => m n' * prod_n m n'
     end)
-    : filterlim (fun x => (Lim_seq (fun nInc => prodn (fun n => Rpower ((1 + x ^ (n + 1)) / (1 + x ^ n)) (x ^ n) ) nInc))) (at_left 1) (locally 0).
+    : filterlim (fun x => (Lim_seq (fun nInc => prodn (fun n => Rpower ((1 + x ^ (n + 1)) / (1 + x ^ n)) (x ^ n) ) nInc))) (at_left 1) (locally putnam_2004_b5_solution).
 Proof. Admitted.
diff --git a/coq/src/putnam_2005_a1.v b/coq/src/putnam_2005_a1.v
index b26827b7..64690b89 100644
--- a/coq/src/putnam_2005_a1.v
+++ b/coq/src/putnam_2005_a1.v
@@ -1,4 +1,9 @@
 Require Import Nat List Coquelicot.Coquelicot.
+Fixpoint nat_sum (a : nat -> nat) (k : nat) : nat := 
+    match k with
+    | O => a 0
+    | S k' => a k + nat_sum a k'
+    end.
 Theorem putnam_2005_a1
-    : forall (n: nat), n > 0 -> exists (l: list nat), forall (p q: nat), In p l /\ In q l -> exists (r1 s1 r2 s2: nat), p = 2 ^ r1 * 3 ^ s1 /\ q = 2 ^ r2 * 3 ^ s2 /\ p mod q <> 0 /\ q mod p <> 0.
+    : forall n : nat, n > 0 -> exists k : nat, exists a : nat -> (nat * nat), n = nat_sum (fun i => 2^(fst (a i)) * 3^(snd(a i))) k /\ forall i j : nat, (i <= k /\ j <= k /\ i <> j) -> ~exists m : nat, (2^(fst (a i))*3^(snd (a i)) * m = 2^(fst (a j))*3^(snd (a j))).
 Proof. Admitted.
diff --git a/coq/src/putnam_2005_a3.v b/coq/src/putnam_2005_a3.v
index 1f1e594b..c40a1c39 100644
--- a/coq/src/putnam_2005_a3.v
+++ b/coq/src/putnam_2005_a3.v
@@ -1,9 +1,11 @@
 Require Import Reals Coquelicot.Coquelicot. From Coqtail Require Import Cpow.
 Theorem putnam_2005_a3
-    (c : nat -> Z)
+    (csqrt : C -> C)
+    (c : nat -> C)
     (n : nat)
-    (p := fun z : C => sum_n (fun i => IZR (c i) * Cpow z i) (n + 1))
-    : forall (r: C), p r = 0 ->  r = RtoC (-1) /\ r = RtoC 1 ->
-    let g (z: C) := p z / Cpow z (n / 2) in
-    forall (r: C), g r = 0 ->  r = RtoC (-1) /\ r = RtoC 1.
+    (p : C -> C := fun z : C => sum_n (fun i => c i * z^i) n)
+    (g : C -> C := fun z : C => p z / csqrt (z^n))
+    (pzeros : forall z : C, p z = 0 -> norm z = 1%R)
+    (hcsqrt : forall z : C, (csqrt z)^2 = z /\ Re (csqrt z) >= 0 /\ (Re (csqrt z) = 0%R -> Im (csqrt z) >= 0%R)) 
+    : forall z : C, C_derive g z = 0 -> norm z = 1%R.
 Proof. Admitted.
diff --git a/coq/src/putnam_2005_a5.v b/coq/src/putnam_2005_a5.v
index 226831be..a3cf2c1c 100644
--- a/coq/src/putnam_2005_a5.v
+++ b/coq/src/putnam_2005_a5.v
@@ -1,5 +1,5 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_2005_a5_solution := PI * (ln 2 / ln 10) / 8.
+Definition putnam_2005_a5_solution := PI * ln 2 / 8.
 Theorem putnam_2005_a5
     : RInt (fun x => ln (x + 1) / (x ^ 2 + 1)) 0 1 = putnam_2005_a5_solution.
 Proof. Admitted.
diff --git a/coq/src/putnam_2005_b1.v b/coq/src/putnam_2005_b1.v
index ca3a2187..592f6b7e 100644
--- a/coq/src/putnam_2005_b1.v
+++ b/coq/src/putnam_2005_b1.v
@@ -1,8 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_2005_b1_solution (c: nat -> nat -> R) (n m: nat) := n = 2%nat /\ m = 2%nat /\ c = fun x y => match x, y with | 0, 1 => -1 | 0, 2 => 1 | 1, 0 => 2 | 1, 1 => -4 | 2, 0 => 4 | _, _ => 0 end.
+Definition putnam_2005_b1_solution := (fun x y => match x, y with | 0, 1 => -1 | 0, 2 => 1 | 1, 0 => 2 | 1, 1 => -4 | 2, 0 => 4 | _, _ => 0 end, (2%nat, 2%nat)).
 Theorem putnam_2005_b1
-    (c: nat -> nat -> R)
-    (n m: nat)
-    (p : R -> R -> R := fun x y => sum_n (fun i => (sum_n (fun j => c i j * x ^ i * y ^ j) m)) (n + 1))
-    : forall (a: R), p (IZR (floor a)) (IZR (floor (2 * a))) = 0 <-> putnam_2005_b1_solution c n m.
+    (p : R -> R -> R := fun x y => sum_n (fun i => (sum_n (fun j => (fst putnam_2005_b1_solution) i j * x ^ i * y ^ j) (fst (snd putnam_2005_b1_solution)))) (snd (snd putnam_2005_b1_solution)))
+    : (~forall x y : R, p x y = 0) /\ forall (a : R), p (IZR (floor a)) (IZR (floor (2 * a))) = 0.
 Proof. Admitted.
diff --git a/coq/src/putnam_2005_b2.v b/coq/src/putnam_2005_b2.v
index 82fe39b6..60d94964 100644
--- a/coq/src/putnam_2005_b2.v
+++ b/coq/src/putnam_2005_b2.v
@@ -2,5 +2,5 @@ Require Import Nat List Reals Coquelicot.Coquelicot.
 Import ListNotations.
 Definition putnam_2005_b2_solution (n: nat) (k: list nat) := (n, k) = (1%nat, [1%nat]) \/ (n, k) = (3%nat, [2%nat; 3%nat; 6%nat]) \/ (n, k) = (3%nat, [2%nat; 6%nat; 3%nat]) \/ (n, k) = (3%nat, [3%nat; 2%nat; 6%nat]) \/ (n, k) = (3%nat, [3%nat; 6%nat; 2%nat]) \/ (n, k) = (3%nat, [6%nat; 2%nat; 3%nat]) \/ (n, k) = (3%nat, [6%nat; 3%nat; 2%nat]) \/ (n, k) = (4%nat, [4%nat; 4%nat; 4%nat; 4%nat]).
 Theorem putnam_2005_b2
-    : forall (n: nat) (k: list nat), forall (x: nat), fold_left add k 0%nat = sub (mul 5 n) 4 /\ sum_n (fun n => 1 / INR (nth n k 0%nat)) n = 1 <-> putnam_2005_b2_solution n k.
+    : forall (n: nat) (k: list nat), length k = n -> ((gt n 0 /\ (forall i : nat, In i k -> gt i 0) /\ fold_left add k 0%nat = sub (mul 5 n) 4 /\ sum_n (fun m => 1 / INR (nth m k 0%nat)) (n - 1) = 1) <-> putnam_2005_b2_solution n k).
 Proof. Admitted.
diff --git a/coq/src/putnam_2005_b3.v b/coq/src/putnam_2005_b3.v
index 60e2daeb..b546a2af 100644
--- a/coq/src/putnam_2005_b3.v
+++ b/coq/src/putnam_2005_b3.v
@@ -1,5 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_2005_b3_solution (f: R -> R) := exists (c d: R), c > 0 /\ d > 0 /\ f = (fun x => c * Rpower x d).
+Definition putnam_2005_b3_solution (f : R -> R) := exists c d : R, c > 0 /\ d > 0 /\ (d = 1 -> c = 1) /\ forall x : R, x > 0 -> f x = c * Rpower x d.
 Theorem putnam_2005_b3
-    : forall (f: R -> R) (x: R), x > 0 /\ f x > 0 /\ ex_derive f x -> exists (a: R), Derive f (a / x) = x  / f x <-> putnam_2005_b3_solution f.
+    (f : R -> R)
+    : ((forall (x : R), x > 0 -> ex_derive f x) /\ exists a : R, a > 0 /\ forall x : R, x > 0 -> Derive f (a / x) = x / f x) <-> putnam_2005_b3_solution f.
 Proof. Admitted.
diff --git a/coq/src/putnam_2005_b4.v b/coq/src/putnam_2005_b4.v
index e5bac0bc..15b9e6a1 100644
--- a/coq/src/putnam_2005_b4.v
+++ b/coq/src/putnam_2005_b4.v
@@ -1,11 +1,13 @@
 Require Import List Ensembles Finite_sets ZArith.
-Open Scope Z.
 Theorem putnam_2005_b4 
     (Absl := fix absl (l : list Z) : list Z :=
         match l with
         | nil => nil
-        | h :: t => Z.abs h :: t
+        | h :: t => Z.abs h :: absl t
     end)
-    : forall (m n: nat), forall (E1 E2: Ensemble (list Z)) (l1 l2: list Z),
-    length l1 = n /\ length l2 = m /\ (E1 l1 <-> fold_left Z.add (Absl l1) 0 <= Z.of_nat m) /\ (E2 l2 <-> fold_left Z.add (Absl l2) 0 <= Z.of_nat n) <-> exists (a: nat), cardinal (list Z) E1 a /\ cardinal (list Z) E2 a.
+    (m n : nat)
+    (mnpos : m > 0 /\ n > 0)
+    (f : nat -> nat -> nat)
+    (hf : forall m' n' : nat, (m' > 0 /\ n' > 0) -> cardinal (list Z) (fun x => length x = n' /\ Z.le (fold_left Z.add (Absl x) 0%Z) (Z.of_nat m')) (f m' n'))
+    : f m n = f n m.
 Proof. Admitted.
diff --git a/isabelle/putnam_1991_a3.thy b/isabelle/putnam_1991_a3.thy
index 66aa32e1..3ccd7b02 100644
--- a/isabelle/putnam_1991_a3.thy
+++ b/isabelle/putnam_1991_a3.thy
@@ -7,11 +7,10 @@ definition putnam_1991_a3_solution :: "real poly set" where "putnam_1991_a3_solu
 (* {p :: real poly. degree p = 2 \<and> (\<exists> r1 r2 :: real. r1 \<noteq> r2 \<and> poly p r1 = 0 \<and> poly p r2 = 0)} *)
 theorem putnam_1991_a3:
   fixes p :: "real poly"
-  and n :: nat
-  and pr :: bool
+    and n :: nat
   defines "n \<equiv> degree p"
-  and "pr \<equiv> \<exists> r :: nat \<Rightarrow> real. (\<forall> i \<in> {1 .. n - 1}. r i < r (i + 1)) \<and> (\<forall> i \<in> {1 .. n}. poly p (r i) = 0) \<and> (\<forall> i \<in> {1 .. n - 1}. poly (pderiv p) ((r i + r (i + 1)) / 2) = 0)"
-  shows "(n \<ge> 2 \<and> pr) \<longleftrightarrow> p \<in> putnam_1991_a3_solution" 
+  assumes hge : "n \<ge> 2"
+  shows "(\<exists> r :: nat \<Rightarrow> real. (\<forall> i \<in> {1 .. n - 1}. r i < r (i + 1)) \<and> (\<forall> i \<in> {1 .. n}. poly p (r i) = 0) \<and> (\<forall> i \<in> {1 .. n - 1}. poly (pderiv p) ((r i + r (i + 1)) / 2) = 0)) \<longleftrightarrow> p \<in> putnam_1991_a3_solution"
   sorry
 
 end
\ No newline at end of file
diff --git a/isabelle/putnam_1991_a6.thy b/isabelle/putnam_1991_a6.thy
index 5f978723..77ed428f 100644
--- a/isabelle/putnam_1991_a6.thy
+++ b/isabelle/putnam_1991_a6.thy
@@ -13,7 +13,7 @@ theorem putnam_1991_a6:
   and bg2 :: "nat \<times> (nat \<Rightarrow> nat) \<Rightarrow> bool"
   and B :: "nat \<Rightarrow> nat"
   defines "nabsum \<equiv> \<lambda> (n :: nat) (ab :: nat \<times> (nat \<Rightarrow> nat)). (fst ab) \<ge> 1 \<and> (\<forall> i < fst ab. (snd ab) i > 0) \<and> (\<forall> i \<ge> fst ab. (snd ab) i = 0) \<and> (\<Sum> i = 0 .. fst ab - 1. (snd ab) i) = n"
-  and "agt \<equiv> \<lambda> a :: nat \<times> (nat \<Rightarrow> nat). \<forall> i \<in> {0 .. fst a - 2}. (snd a) i > (snd a) (i + 1) + (snd a) (i + 2)"
+  and "agt \<equiv> \<lambda> a :: nat \<times> (nat \<Rightarrow> nat). (\<forall> i \<in> {0 .. fst a - 3}. (snd a) i > (snd a) (i + 1) + (snd a) (i + 2)) \<and> (snd a) (fst a - 2) > (snd a) (fst a - 1)"
   and "A \<equiv> \<lambda> n :: nat. card {a :: nat \<times> (nat \<Rightarrow> nat). nabsum n a \<and> agt a}"
   and "bge \<equiv> \<lambda> b :: nat \<times> (nat \<Rightarrow> nat). \<forall> i \<in> {0 .. fst b - 2}. (snd b) i \<ge> (snd b) (i + 1)"
   and "bg1 \<equiv> \<lambda> b :: nat \<times> (nat \<Rightarrow> nat). \<forall> i \<in> {0 .. fst b - 1}. \<exists> j :: nat. (snd b) i = g j"
diff --git a/isabelle/putnam_1991_b1.thy b/isabelle/putnam_1991_b1.thy
index 4a303497..1c12041e 100644
--- a/isabelle/putnam_1991_b1.thy
+++ b/isabelle/putnam_1991_b1.thy
@@ -6,13 +6,14 @@ definition putnam_1991_b1_solution :: "nat set" where "putnam_1991_b1_solution \
 (* {A :: nat. \<exists> x > 0. A = x ^ 2} *)
 theorem putnam_1991_b1:
   fixes m :: "nat \<Rightarrow> nat"
-  and S :: "nat \<Rightarrow> nat"
-  and A :: nat
-  and a :: "nat \<Rightarrow> nat"
+    and S :: "nat \<Rightarrow> nat"
+    and A :: nat
+    and a :: "nat \<Rightarrow> nat"
   defines "m \<equiv> \<lambda> n. GREATEST M :: nat. M ^ 2 \<le> n"
-  and "S \<equiv> \<lambda> n. n - (m n) ^ 2"
-  assumes ha: "a 0 = A \<and> (\<forall> k :: nat. a (k + 1) = a k + S (a k))"
-  shows "(A > 0 \<and> (\<exists> K c :: nat. \<forall> k \<ge> K. a k = c)) \<longleftrightarrow> A \<in> putnam_1991_b1_solution"
+    and "S \<equiv> \<lambda> n. n - (m n) ^ 2"
+  assumes ha : "a 0 = A \<and> (\<forall> k :: nat. a (k + 1) = a k + S (a k))"
+    and hA : "A > 0"  
+  shows "(\<exists> K c :: nat. \<forall> k \<ge> K. a k = c) \<longleftrightarrow> A \<in> putnam_1991_b1_solution"
   sorry
 
 end
\ No newline at end of file
diff --git a/isabelle/putnam_1993_b1.thy b/isabelle/putnam_1993_b1.thy
index 7218bfc1..c01e4af0 100644
--- a/isabelle/putnam_1993_b1.thy
+++ b/isabelle/putnam_1993_b1.thy
@@ -5,7 +5,7 @@ definition putnam_1993_b1_solution::nat where "putnam_1993_b1_solution \<equiv>
 (* 3987 *)
 theorem putnam_1993_b1:
   fixes nallmexk::"nat\<Rightarrow>bool"
-  defines "nallmexk \<equiv> \<lambda>n::nat. (n > 0 \<and> (\<forall>m \<in> {0<..<1993}. (\<exists>k::int. (m / 1993 < k / n) \<and> (k / n < (m+1) / 1994))))"
+  defines "nallmexk \<equiv> \<lambda>n::nat. (n > 0 \<and> (\<forall>m \<in> {(0::int)<..<1993}. (\<exists>k::int. (m / 1993 < k / n) \<and> (k / n < (m+1) / 1994))))"
   shows "putnam_1993_b1_solution = (LEAST n. nallmexk n)"
   sorry
 
diff --git a/isabelle/putnam_1993_b3.thy b/isabelle/putnam_1993_b3.thy
index f0774322..f208ba85 100644
--- a/isabelle/putnam_1993_b3.thy
+++ b/isabelle/putnam_1993_b3.thy
@@ -7,7 +7,7 @@ definition putnam_1993_b3_solution :: "rat \<times> rat" where "putnam_1993_b3_s
 (* (5/4, -1/4) *)
 theorem putnam_1993_b3:
   fixes S :: "(real^2) set"
-  defines "S \<equiv> {p :: real^2. (\<forall> i :: 2. p$i \<in> {0<..<1}) \<and> even (round (p$1 / p$2))}"
+  defines "S \<equiv> {p :: real^2. (\<forall> i :: 2. 0 < p$i \<and> p$i < 1) \<and> even (round (p$1 / p$2))}"
   shows "let (r, s) = putnam_1993_b3_solution in (measure lebesgue S) / 1 = real_of_rat r + real_of_rat s * pi"
   sorry
 
diff --git a/isabelle/putnam_1994_a3.thy b/isabelle/putnam_1994_a3.thy
index dec14f89..aa7031b7 100644
--- a/isabelle/putnam_1994_a3.thy
+++ b/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
\ No newline at end of file
diff --git a/isabelle/putnam_1994_b5.thy b/isabelle/putnam_1994_b5.thy
index d6d05dcf..7bf56621 100644
--- a/isabelle/putnam_1994_b5.thy
+++ b/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
diff --git a/isabelle/putnam_1995_a2.thy b/isabelle/putnam_1995_a2.thy
index 30458e02..13780fd1 100644
--- a/isabelle/putnam_1995_a2.thy
+++ b/isabelle/putnam_1995_a2.thy
@@ -7,7 +7,7 @@ definition putnam_1995_a2_solution :: "(real \<times> real) set" where "putnam_1
 theorem putnam_1995_a2:
   fixes habconv :: "(real \<times> real) \<Rightarrow> bool"
   defines "habconv \<equiv> (\<lambda>(a::real,b::real). (\<exists>limit::real. filterlim (\<lambda>t::real. interval_lebesgue_integral lebesgue b t (\<lambda>x::real. sqrt (sqrt (x+a) - sqrt x) - sqrt (sqrt x - sqrt (x-b)))) (nhds limit) at_top))"
-  shows "\<forall>ab::real\<times>real. habconv ab \<longleftrightarrow> ab \<in> putnam_1995_a2_solution"
+  shows "\<forall>ab::real\<times>real. fst ab > 0 \<and> snd ab > 0 \<longrightarrow> (habconv ab \<longleftrightarrow> ab \<in> putnam_1995_a2_solution)"
   sorry
 
 end
diff --git a/isabelle/putnam_2004_a4.thy b/isabelle/putnam_2004_a4.thy
index 1635dffd..01c5d43b 100644
--- a/isabelle/putnam_2004_a4.thy
+++ b/isabelle/putnam_2004_a4.thy
@@ -3,10 +3,12 @@ begin
 
 (* Note: Boosted domain to infinite set *)
 theorem putnam_2004_a4:
-  fixes n::nat and x::"nat\<Rightarrow>real" and avals::"nat \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> real) \<Rightarrow> bool"
-  defines "avals \<equiv> \<lambda>N. \<lambda>a. \<forall>i \<in> {0..<N}. \<forall>j \<in> {0..<n}. (a i j = -1 \<or> a i j = 0 \<or> a i j = 1)"
+  fixes n :: nat 
+    and x :: "nat\<Rightarrow>real" 
+    and avals :: "nat \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> real) \<Rightarrow> bool"
+  defines "avals \<equiv> \<lambda> N :: nat. \<lambda> a :: nat \<Rightarrow> nat \<Rightarrow> real. \<forall> i \<in> {0..<N}. \<forall> j \<in> {0..<n}. (a i j = -1 \<or> a i j = 0 \<or> a i j = 1)"
   assumes npos : "n > 0"
-  shows "\<exists>N::nat. \<exists>c::nat\<Rightarrow>rat. \<exists>a. avals N a \<and> ((\<Prod>i=0..<n. x i) = (\<Sum>i=0..<N. (c i * (\<Sum>j=0..<n. a i j * x j)^n)))"
+  shows "\<exists> N :: nat. \<exists> c :: nat \<Rightarrow> rat. \<exists> a :: nat \<Rightarrow> nat \<Rightarrow> real. avals N a \<and> ((\<Prod>i=0..<n. x i) = (\<Sum>i=0..<N. (c i * (\<Sum>j=0..<n. a i j * x j)^n)))"
   sorry
 
 end
diff --git a/isabelle/putnam_2004_a6.thy b/isabelle/putnam_2004_a6.thy
index 74082704..390e7b08 100644
--- a/isabelle/putnam_2004_a6.thy
+++ b/isabelle/putnam_2004_a6.thy
@@ -3,13 +3,12 @@ theory putnam_2004_a6 imports Complex_Main
 begin
 
 theorem putnam_2004_a6:
-  fixes f::"(real\<times>real)\<Rightarrow>real" and usquare::"(real\<times>real) set" and Fx Fy::"real\<Rightarrow>real\<Rightarrow>real"
+  fixes f :: "(real\<times>real)\<Rightarrow>real" 
+    and usquare :: "(real\<times>real) set" 
   defines "usquare \<equiv> {(x, y). x \<ge> 0 \<and> y \<ge> 0 \<and> x \<le> 1 \<and> y \<le> 1}"
   assumes fcont : "continuous_on usquare f"
-    and fxderiv : "\<forall>y::real \<in> {0<..<1}. \<forall>x::real \<in> {0<..<1}. ((Fx y) has_derivative (\<lambda>x. f (x, y))) (nhds x)"
-    and fyderiv : "\<forall>x::real \<in> {0<..<1}. \<forall>y::real \<in> {0<..<1}. ((Fy x) has_derivative (\<lambda>y. f (x, y))) (nhds y)"
-  shows "interval_lebesgue_integral lebesgue 0 1 (\<lambda>y. (Fx y 1 - Fx y 0)^2) + 
-    interval_lebesgue_integral lebesgue 0 1 (\<lambda>x. (Fy x 1 - Fy x 0)^2) \<le> 
+  shows "interval_lebesgue_integral lebesgue 0 1 (\<lambda>y. (interval_lebesgue_integral lebesgue 0 1 (\<lambda>x. f (x, y)))^2) + 
+    interval_lebesgue_integral lebesgue 0 1 (\<lambda>x. (interval_lebesgue_integral lebesgue 0 1 (\<lambda>y. f (x, y)))^2) \<le> 
     (set_lebesgue_integral lebesgue usquare f)^2 + set_lebesgue_integral lebesgue usquare (\<lambda>(x, y). f (x, y)^2)"
   sorry
 
diff --git a/isabelle/putnam_2004_b1.thy b/isabelle/putnam_2004_b1.thy
index e76cbc2e..8e275b68 100644
--- a/isabelle/putnam_2004_b1.thy
+++ b/isabelle/putnam_2004_b1.thy
@@ -4,11 +4,13 @@ begin
 
 (* Note: Boosted domain to infinite set *)
 theorem putnam_2004_b1:
-  fixes n::nat and P::"real poly" and r::rat
-  assumes Pdeg : "degree p = n"
-    and Pcoeff : "\<forall>i \<in> {0..n}. (coeff p i) \<in> \<int>"
-    and Preq0 : "poly p r = 0"
-  shows "\<forall>i \<in> {0..<n}. (\<Sum>j=0..i. (coeff p (n-j) * r^(i+1-j))) \<in> \<int>"
+  fixes n :: nat 
+    and P :: "rat poly"
+    and r :: rat
+  assumes Pdeg : "degree P = n"
+    and Pcoeff : "\<forall> i \<in> {0..n}. (coeff P i) \<in> \<int>"
+    and Preq0 : "poly P r = 0"
+  shows "\<forall>i \<in> {0..<n}. (\<Sum>j=0..i. (coeff P (n-j) * r^(i+1-j))) \<in> \<int>"
   sorry
 
 end
diff --git a/isabelle/putnam_2004_b6.thy b/isabelle/putnam_2004_b6.thy
index 1c5b69c8..998dd3fd 100644
--- a/isabelle/putnam_2004_b6.thy
+++ b/isabelle/putnam_2004_b6.thy
@@ -2,12 +2,14 @@ theory putnam_2004_b6 imports Complex_Main
 begin
 
 theorem putnam_2004_b6:
-  fixes A B::"nat set" and N::"real\<Rightarrow>nat" and b::"nat\<Rightarrow>nat"
+  fixes A B::"nat set" 
+    and N::"real\<Rightarrow>nat" 
+    and b::"nat\<Rightarrow>nat"
   defines "N \<equiv> \<lambda>x::real. card {a\<in>A. a \<le> x}"
     and "B \<equiv> {b'. b' > 0 \<and> (\<exists>a \<in> A. \<exists>a' \<in> A. b' = a - a')}"
   assumes Anempty : "card A > 0"
     and Apos : "\<forall>a \<in> A. a > 0"
-    and hbB : "B = image b {1..(card B)}"
+    and hbB : "B = image b UNIV"
     and hbasc : "\<forall>i::nat. b i < b (i+1)"
   shows "(\<forall>r::nat. \<exists>i::nat. (b (i+1) - b i) \<ge> r) \<longrightarrow> ((\<lambda>x::real. N x / x) \<longlongrightarrow> 0) at_top"
   sorry
diff --git a/isabelle/putnam_2005_a3.thy b/isabelle/putnam_2005_a3.thy
index e3aed1c8..4143b9c2 100644
--- a/isabelle/putnam_2005_a3.thy
+++ b/isabelle/putnam_2005_a3.thy
@@ -1,5 +1,6 @@
 theory putnam_2005_a3 imports Complex_Main
 "HOL-Computational_Algebra.Polynomial"
+"HOL-Analysis.Derivative"
 begin
 
 theorem putnam_2005_a3:
diff --git a/isabelle/putnam_2005_a5.thy b/isabelle/putnam_2005_a5.thy
index 9ec3bf04..f0409486 100644
--- a/isabelle/putnam_2005_a5.thy
+++ b/isabelle/putnam_2005_a5.thy
@@ -1,10 +1,9 @@
 theory putnam_2005_a5 imports Complex_Main
 "HOL-Analysis.Lebesgue_Measure"
-"HOL-Analysis.Set_Integral"
+"HOL-Analysis.Interval_Integral"
 begin
 
-definition putnam_2005_a5_solution :: "real" where
-"putnam_2005_a5_solution \<equiv> undefined"
+definition putnam_2005_a5_solution :: "real" where "putnam_2005_a5_solution \<equiv> undefined"
 (* pi * (ln 2) / 8 *)
 theorem putnam_2005_a5:
   shows "interval_lebesgue_integral lebesgue 0 1 (\<lambda> x :: real. (ln (x + 1))/(x^2 + 1)) = putnam_2005_a5_solution" 
diff --git a/isabelle/putnam_2005_b2.thy b/isabelle/putnam_2005_b2.thy
index 399d009b..974c95ff 100644
--- a/isabelle/putnam_2005_b2.thy
+++ b/isabelle/putnam_2005_b2.thy
@@ -2,18 +2,10 @@ theory putnam_2005_b2 imports Complex_Main
 begin
 
 (* uses (nat \<Rightarrow> nat) instead of (Fin n \<Rightarrow> nat) *)
-definition putnam_2005_b2_solution :: "(nat \<times> (nat \<Rightarrow> nat)) set" where "putnam_2005_b2_solution \<equiv> undefined"
-(* {(n::nat,k::nat\<Rightarrow>nat). (n = 1 \<and> k 0 = 1) \<or> (n = 3 \<and> k ` {0,1,2} = {2,3,6}) \<or> (n = 4 \<and> (\<forall>i::nat\<in>{0..3}. k i = 4))} *)
+definition putnam_2005_b2_solution :: "(nat \<times> (nat \<Rightarrow> int)) set" where "putnam_2005_b2_solution \<equiv> undefined"
+(* {(n::nat,k::nat\<Rightarrow>int). (n = 1 \<and> k 0 = 1) \<or> (n = 3 \<and> k ` {0,1,2} = {2,3,6}) \<or> (n = 4 \<and> (\<forall>i::nat\<in>{0..3}. k i = 4))} *)
 theorem putnam_2005_b2:
-  fixes n :: nat
-  and k :: "nat \<Rightarrow> nat"
-  and nkpos :: bool
-  and nkeq1 :: bool
-  and nkeq2 :: bool
-  assumes "nkpos \<equiv> (n > 0 \<and> (\<forall>i::nat\<in>{0..(n-1)}. k i > 0))"
-  and "nkeq1 \<equiv> ((\<Sum>i::nat=0..(n-1). k i) = 5*n - 4)"
-  and "nkeq2 \<equiv> ((\<Sum>i::nat=0..(n-1). (1 / k i)) = 1)"
-  shows "(nkpos \<and> nkeq1 \<and> nkeq2) \<longleftrightarrow> (n, k) \<in> putnam_2005_b2_solution"
+  shows "{(n::nat, k::nat\<Rightarrow>int). n > 0 \<and> (\<forall>i::nat\<in>{0..(n-1)}. k i > 0) \<and> ((\<Sum>i::nat=0..(n-1). k i) = 5*n - 4) \<and> ((\<Sum>i::nat=0..(n-1). (1 / k i)) = 1)} = putnam_2005_b2_solution"
   sorry
 
 end
diff --git a/isabelle/putnam_2005_b3.thy b/isabelle/putnam_2005_b3.thy
index f0b878e4..bc7e498b 100644
--- a/isabelle/putnam_2005_b3.thy
+++ b/isabelle/putnam_2005_b3.thy
@@ -7,9 +7,7 @@ definition putnam_2005_b3_solution :: "(real \<Rightarrow> real) set" where "put
 (* {f::real\<Rightarrow>real. (\<exists>c d::real. c > 0 \<and> d > 0 \<and> (d = 1 \<longrightarrow> c = 1) \<and> (\<forall>x::real\<in>{0<..}. f x = c * x powr d))} *)
 theorem putnam_2005_b3:
   fixes f :: "real \<Rightarrow> real"
-  and fexa :: bool
-  assumes hfexa: "fexa \<equiv> (\<exists>a::real>0. \<forall>x::real>0. deriv f (a/x) = x / f x)"
-  shows "(f differentiable_on {0<..} \<and> fexa) \<longleftrightarrow> f \<in> putnam_2005_b3_solution"
+  shows "(f differentiable_on {0<..} \<and> (\<exists>a::real>0. \<forall>x::real>0. deriv f (a/x) = x / f x)) \<longleftrightarrow> f \<in> putnam_2005_b3_solution"
   sorry
 
 end
diff --git a/isabelle/putnam_2005_b4.thy b/isabelle/putnam_2005_b4.thy
index 7be4a00f..8b253bbf 100644
--- a/isabelle/putnam_2005_b4.thy
+++ b/isabelle/putnam_2005_b4.thy
@@ -2,9 +2,10 @@ theory putnam_2005_b4 imports Complex_Main
 begin
 
 theorem putnam_2005_b4:
-  fixes m n::nat and f::"nat\<Rightarrow>nat\<Rightarrow>nat"
+  fixes m n::nat 
+    and f::"nat\<Rightarrow>nat\<Rightarrow>nat"
   assumes mnpos : "m > 0 \<and> n > 0"
-    and "\<forall>m' > 0. \<forall>n' > 0. f m' n' = card {x::int list. size x = n' \<and> (\<Sum>i=0..<n'. abs(x!i)) \<le> m'}"
+    and hf : "\<forall>m' > 0. \<forall>n' > 0. f m' n' = card {x::int list. size x = n' \<and> (\<Sum>i=0..<n'. abs(x!i)) \<le> m'}"
   shows "f m n = f n m"
   sorry
 
diff --git a/isabelle/putnam_2005_b5.thy b/isabelle/putnam_2005_b5.thy
index a07eaaca..9de6beb1 100644
--- a/isabelle/putnam_2005_b5.thy
+++ b/isabelle/putnam_2005_b5.thy
@@ -4,18 +4,18 @@ begin
 
 theorem putnam_2005_b5:
   fixes n :: nat
-  and P :: "('n::finite \<Rightarrow> real) \<Rightarrow> real"
-  and ispoly :: "(('n \<Rightarrow> real) \<Rightarrow> real) \<Rightarrow> bool"
-  and P2deriv :: "'n \<Rightarrow> ('n \<Rightarrow> real) \<Rightarrow> real"
-  and Psumsq :: "('n \<Rightarrow> real) \<Rightarrow> real"
-  assumes npos: "n > 0"
-  and pncard: "CARD('n) = n"
+    and P :: "('n::finite \<Rightarrow> real) \<Rightarrow> real"
+    and ispoly :: "(('n \<Rightarrow> real) \<Rightarrow> real) \<Rightarrow> bool"
+    and P2deriv :: "'n \<Rightarrow> ('n \<Rightarrow> real) \<Rightarrow> real"
+    and Psumsq :: "('n \<Rightarrow> real) \<Rightarrow> real"
   defines "ispoly \<equiv> (\<lambda>P'::('n\<Rightarrow>real)\<Rightarrow>real. (\<exists>l::(real\<times>('n\<Rightarrow>nat)) list. \<forall>x::'n\<Rightarrow>real. P' x = (\<Sum>j::nat=0..((length l)-1). (fst (l!j)) * (\<Prod>i::'n\<in>UNIV. (x i) ^ ((snd (l!j)) i)))))"
-  assumes Ppoly: "ispoly P"
-  defines "P2deriv \<equiv> (\<lambda>(i::'n)(x::'n\<Rightarrow>real). (deriv^^2) (\<lambda>xi::real. P (\<lambda>i'::'n \<Rightarrow> if i' = i then xi else x i')) (x i))"
-  assumes hderiv: "\<forall>x::'n\<Rightarrow>real. (\<Sum>i::'n\<in>UNIV. P2deriv i x) = 0"
-  defines "Psumsq \<equiv> (\<lambda>x::'n\<Rightarrow>real. (\<Sum>i::'n\<in>UNIV. (x i)^2))"
-  assumes hsumsq: "\<exists>Q::('n\<Rightarrow>real)\<Rightarrow>real. ispoly Q \<and> (\<forall>x::'n\<Rightarrow>real. (Psumsq x) * (Q x) = P x)"
+    and "P2deriv \<equiv> (\<lambda>(i::'n)(x::'n\<Rightarrow>real). (deriv^^2) (\<lambda>xi::real. P (\<lambda>i'::'n. if i' = i then xi else x i')) (x i))"
+    and "Psumsq \<equiv> (\<lambda>x::'n\<Rightarrow>real. (\<Sum>i::'n\<in>UNIV. (x i)^2))"
+  assumes npos: "n > 0"
+    and pncard: "CARD('n) = n"
+    and Ppoly: "ispoly P"
+    and hderiv: "\<forall>x::'n\<Rightarrow>real. (\<Sum>i::'n\<in>UNIV. P2deriv i x) = 0"
+    and hsumsq: "\<exists>Q::('n\<Rightarrow>real)\<Rightarrow>real. ispoly Q \<and> (\<forall>x::'n\<Rightarrow>real. (Psumsq x) * (Q x) = P x)"
   shows "P = (\<lambda>x::'n\<Rightarrow>real. 0)"
   sorry
 
diff --git a/isabelle/putnam_2005_b6.thy b/isabelle/putnam_2005_b6.thy
index 995ff9b0..0c58db75 100644
--- a/isabelle/putnam_2005_b6.thy
+++ b/isabelle/putnam_2005_b6.thy
@@ -3,7 +3,10 @@ theory putnam_2005_b6 imports Complex_Main
 begin
 
 theorem putnam_2005_b6:
-  fixes n::nat and S::"(nat\<Rightarrow>nat) set" and \<sigma>::"(nat\<Rightarrow>nat) \<Rightarrow> int" and v::"(nat\<Rightarrow>nat) \<Rightarrow> int" 
+  fixes n::nat 
+    and S::"(nat\<Rightarrow>nat) set" 
+    and \<sigma>::"(nat\<Rightarrow>nat) \<Rightarrow> int" 
+    and v::"(nat\<Rightarrow>nat) \<Rightarrow> int" 
   defines "S \<equiv> {p. p permutes {1..n}}"
     and "\<sigma> \<equiv> \<lambda>p. if (evenperm p) then 1 else -1"
     and "v \<equiv> \<lambda>p. card {x::nat. x > 0 \<and> x \<le> n \<and> p x = x}"
diff --git a/lean4/src/putnam_1991_a3.lean b/lean4/src/putnam_1991_a3.lean
index e09cb57b..303e22c5 100644
--- a/lean4/src/putnam_1991_a3.lean
+++ b/lean4/src/putnam_1991_a3.lean
@@ -9,8 +9,7 @@ abbrev putnam_1991_a3_solution : Set (Polynomial ℝ) := sorry
 theorem putnam_1991_a3
 (p : Polynomial ℝ)
 (n : ℕ)
-(pr : Prop)
 (hn : n = p.degree)
-(hpr : pr = ∃ r : ℕ → ℝ, (∀ i : Fin (n - 1), r i < r (i + 1)) ∧ (∀ i : Fin n, p.eval (r i) = 0) ∧ (∀ i : Fin (n - 1), (Polynomial.derivative p).eval ((r i + r (i + 1)) / 2) = 0))
-: (n ≥ 2 ∧ pr) ↔ p ∈ putnam_1991_a3_solution :=
+(hge : n ≥ 2)
+: (∃ r : ℕ → ℝ, (∀ i : Fin (n - 1), r i < r (i + 1)) ∧ (∀ i : Fin n, p.eval (r i) = 0) ∧ (∀ i : Fin (n - 1), (Polynomial.derivative p).eval ((r i + r (i + 1)) / 2) = 0)) ↔ p ∈ putnam_1991_a3_solution :=
 sorry
diff --git a/lean4/src/putnam_1991_a6.lean b/lean4/src/putnam_1991_a6.lean
index 486b5ef7..9678cfe4 100644
--- a/lean4/src/putnam_1991_a6.lean
+++ b/lean4/src/putnam_1991_a6.lean
@@ -14,7 +14,7 @@ theorem putnam_1991_a6
 (bg2 : ℕ × (ℕ → ℕ) → Prop)
 (B : ℕ → ℕ)
 (hnabsum : ∀ n ≥ 1, ∀ ab : ℕ × (ℕ → ℕ), nabsum n ab = (ab.1 ≥ 1 ∧ (∀ i < ab.1, ab.2 i > 0) ∧ (∀ i ≥ ab.1, ab.2 i = 0) ∧ (∑ i : Fin ab.1, ab.2 i) = n))
-(hagt : ∀ a : ℕ × (ℕ → ℕ), agt a = ∀ i : Fin (a.1 - 1), a.2 i > a.2 (i + 1) + a.2 (i + 2))
+(hagt : ∀ a : ℕ × (ℕ → ℕ), agt a = (∀ i : Fin (a.1 - 2), a.2 i > a.2 (i + 1) + a.2 (i + 2)) ∧ a.2 (a.1 - 2) > a.2 (a.1 - 1))
 (hA : ∀ n ≥ 1, A n = {a : ℕ × (ℕ → ℕ) | nabsum n a ∧ agt a}.encard)
 (hbge : ∀ b : ℕ × (ℕ → ℕ), bge b = ∀ i : Fin (b.1 - 1), b.2 i ≥ b.2 (i + 1))
 (hg : g 0 = 1 ∧ g 1 = 2 ∧ (∀ j ≥ 2, g j = g (j - 1) + g (j - 2) + 1))
diff --git a/lean4/src/putnam_1991_b1.lean b/lean4/src/putnam_1991_b1.lean
index c69f8c78..53a05b6b 100644
--- a/lean4/src/putnam_1991_b1.lean
+++ b/lean4/src/putnam_1991_b1.lean
@@ -13,5 +13,6 @@ theorem putnam_1991_b1
 (hm : ∀ n : ℤ, n ≥ 0 → (m n) ^ 2 ≤ n ∧ (∀ m' : ℤ, m' ^ 2 ≤ n → m' ≤ m n))
 (hS : ∀ n : ℤ, n ≥ 0 → S n = n - (m n) ^ 2)
 (ha : a 0 = A ∧ (∀ k : ℕ, a (k + 1) = a k + S (a k)))
-: (A > 0 ∧ (∃ (K : ℕ) (c : ℕ), ∀ k ≥ K, a k = c)) ↔ A ∈ putnam_1991_b1_solution :=
+(hA : A > 0)
+: (∃ (K : ℕ) (c : ℕ), ∀ k ≥ K, a k = c) ↔ A ∈ putnam_1991_b1_solution :=
 sorry
diff --git a/lean4/src/putnam_1993_b1.lean b/lean4/src/putnam_1993_b1.lean
index 9e1ad63c..3c38d7fa 100644
--- a/lean4/src/putnam_1993_b1.lean
+++ b/lean4/src/putnam_1993_b1.lean
@@ -5,6 +5,6 @@ abbrev putnam_1993_b1_solution : ℕ := sorry
 -- 3987
 theorem putnam_1993_b1
 (nallmexk : ℕ → Prop)
-(hnallmexk : ∀ n : ℕ, nallmexk n = (n > 0 ∧ ∀ m ∈ Set.Ioo 0 1993, ∃ k : ℤ, (m / 1993 < (k : ℝ) / n) ∧ ((k : ℝ) / n < (m + 1) / 1994)))
+(hnallmexk : ∀ n : ℕ, nallmexk n = (n > 0 ∧ ∀ m ∈ Set.Ioo (0 : ℤ) 1993, ∃ k : ℤ, (m / 1993 < (k : ℝ) / n) ∧ ((k : ℝ) / n < (m + 1) / 1994)))
 : nallmexk putnam_1993_b1_solution ∧ (∀ n : ℕ, nallmexk n → n ≥ putnam_1993_b1_solution) :=
 sorry
diff --git a/lean4/src/putnam_1994_b5.lean b/lean4/src/putnam_1994_b5.lean
index 60f606e1..6859bb12 100644
--- a/lean4/src/putnam_1994_b5.lean
+++ b/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
diff --git a/lean4/src/putnam_1995_a2.lean b/lean4/src/putnam_1995_a2.lean
index 40da99b0..daf4282e 100644
--- a/lean4/src/putnam_1995_a2.lean
+++ b/lean4/src/putnam_1995_a2.lean
@@ -8,5 +8,5 @@ abbrev putnam_1995_a2_solution : Set (ℝ × ℝ) := sorry
 theorem putnam_1995_a2
 (habconv : (ℝ × ℝ) → Prop := fun ⟨a,b⟩ =>
 ∃ limit : ℝ, Tendsto (fun t : ℝ => ∫ x in (Set.Icc b t), (sqrt (sqrt (x + a) - sqrt x) - sqrt (sqrt x - sqrt (x - b)))) atTop (𝓝 limit))
-: ∀ ab : ℝ × ℝ, habconv ab ↔ ab ∈ putnam_1995_a2_solution :=
+: ∀ ab : ℝ × ℝ, ab.1 > 0 ∧ ab.2 > 0 → (habconv ab ↔ ab ∈ putnam_1995_a2_solution) :=
 sorry
diff --git a/lean4/src/putnam_1995_a4.lean b/lean4/src/putnam_1995_a4.lean
index 801e1fff..4f8661a8 100644
--- a/lean4/src/putnam_1995_a4.lean
+++ b/lean4/src/putnam_1995_a4.lean
@@ -6,7 +6,7 @@ open Filter Topology Real
 theorem putnam_1995_a4
 (n : ℕ)
 (hn : n > 0)
-(necklace : Fin n → ℤ)
-(hnecklacesum : ∑ i : Fin n, necklace i = n - 1)
-: ∃ cut : Fin n, ∀ k : Fin n, ∑ i : {j : Fin n | j.1 ≤ k}, necklace (cut + i) ≤ k :=
+(necklace : ℕ → ℤ)
+(hnecklacesum : ∑ i ∈ Finset.range n, necklace i = n - 1)
+: ∃ cut ∈ Finset.range n, ∀ k ∈ Finset.range n, ∑ i ≤ k, necklace ((cut + i) % n) ≤ k :=
 sorry
diff --git a/lean4/src/putnam_1995_b6.lean b/lean4/src/putnam_1995_b6.lean
index 43c1da03..4f3da7c9 100644
--- a/lean4/src/putnam_1995_b6.lean
+++ b/lean4/src/putnam_1995_b6.lean
@@ -5,5 +5,5 @@ open Filter Topology Real Nat
 
 theorem putnam_1995_b6
 (S : ℝ → Set ℕ := fun α => {x : ℕ | ∃ n : ℕ, n ≥ 1 ∧ x = floor (n * α)})
-: ¬ ∃ α β γ : ℝ, α > 0 ∧ β > 0 ∧ γ > 0 ∧ (S α) ∩ (S β) = ∅ ∧ (S β) ∩ (S γ) = ∅ ∧ (S α) ∩ (S γ) = ∅ ∧ ℕ+ = (S α) ∪ (S β) ∪ (S γ) :=
+: ¬ ∃ α β γ : ℝ, α > 0 ∧ β > 0 ∧ γ > 0 ∧ (S α) ∩ (S β) = ∅ ∧ (S β) ∩ (S γ) = ∅ ∧ (S α) ∩ (S γ) = ∅ ∧ Set.Ici 1 = (S α) ∪ (S β) ∪ (S γ) :=
 sorry
diff --git a/lean4/src/putnam_2004_a3.lean b/lean4/src/putnam_2004_a3.lean
index 2344c052..a053ccfb 100644
--- a/lean4/src/putnam_2004_a3.lean
+++ b/lean4/src/putnam_2004_a3.lean
@@ -6,6 +6,6 @@ open Nat Topology Filter
 theorem putnam_2004_a3
 (u : ℕ → ℝ)
 (hubase : u 0 = 1 ∧ u 1 = 1 ∧ u 2 = 1)
-(hudet : ∀ n : ℕ, Matrix.det (fun i j : Finset.range 2 => u (n + i * 2 + j)) = (n)!)
-: ∀ n : ℕ, u n = round (u n) :=
+(hudet : ∀ n : ℕ, Matrix.det (fun i j : Fin 2 => u (n + i * 2 + j)) = (n)!)
+: ∀ n : ℕ, ∃ m : ℤ, u n = m :=
 sorry
diff --git a/lean4/src/putnam_2004_a6.lean b/lean4/src/putnam_2004_a6.lean
index c8e1c8fb..ff4f5435 100644
--- a/lean4/src/putnam_2004_a6.lean
+++ b/lean4/src/putnam_2004_a6.lean
@@ -4,7 +4,7 @@ open BigOperators
 open Nat Topology Filter
 
 theorem putnam_2004_a6
-(f : Set.Icc (0 : ℝ) 1 → Set.Icc (0 : ℝ) 1 → ℝ)
+(f : (Set.Icc (0 : ℝ) 1 × Set.Icc (0 : ℝ) 1) → ℝ)
 (fcont : Continuous f)
-: (∫ y : Set.Icc (0 : ℝ) 1, (∫ x : Set.Icc (0 : ℝ) 1, f x y) ^ 2) + (∫ x : Set.Icc (0 : ℝ) 1, (∫ y : Set.Icc (0 : ℝ) 1, f x y) ^ 2) ≤ (∫ y : Set.Icc (0 : ℝ) 1, (∫ x : Set.Icc (0 : ℝ) 1, f x y)) ^ 2 + (∫ y : Set.Icc (0 : ℝ) 1, (∫ x : Set.Icc (0 : ℝ) 1, (f x y) ^ 2)) :=
+: (∫ y : Set.Icc (0 : ℝ) 1, (∫ x : Set.Icc (0 : ℝ) 1, f (x, y)) ^ 2) + (∫ x : Set.Icc (0 : ℝ) 1, (∫ y : Set.Icc (0 : ℝ) 1, f (x, y)) ^ 2) ≤ (∫ y : Set.Icc (0 : ℝ) 1, (∫ x : Set.Icc (0 : ℝ) 1, f (x, y))) ^ 2 + (∫ y : Set.Icc (0 : ℝ) 1, (∫ x : Set.Icc (0 : ℝ) 1, (f (x, y)) ^ 2)) :=
 sorry
diff --git a/lean4/src/putnam_2004_b1.lean b/lean4/src/putnam_2004_b1.lean
index 79922842..a1c382d1 100644
--- a/lean4/src/putnam_2004_b1.lean
+++ b/lean4/src/putnam_2004_b1.lean
@@ -5,12 +5,9 @@ open Nat Topology Filter
 
 theorem putnam_2004_b1
 (n : ℕ)
-(P : Polynomial ℝ)
-(isint : ℝ → Prop)
+(P : Polynomial ℤ)
 (r : ℚ)
 (Pdeg : P.degree = n)
-(hisint : ∀ x : ℝ, isint x = (x = round x))
-(Pcoeff : ∀ i : Fin (n + 1), isint (P.coeff i))
-(Preq0 : P.eval (r : ℝ) = 0)
-: ∀ i : Fin n, isint (∑ j : Fin (i + 1), (P.coeff (n - j) * r ^ ((i.1 + 1) - j))) :=
+(Preq0 : Polynomial.aeval r P = 0)
+: ∀ i ∈ Finset.range n, ∃ m : ℤ, m = ∑ j ∈ Finset.range (i + 1), (P.coeff (n - j) * r ^ (i + 1 - j)) :=
 sorry
diff --git a/lean4/src/putnam_2005_a1.lean b/lean4/src/putnam_2005_a1.lean
index 422fc878..01fbc4d2 100644
--- a/lean4/src/putnam_2005_a1.lean
+++ b/lean4/src/putnam_2005_a1.lean
@@ -5,5 +5,5 @@ open Nat
 
 theorem putnam_2005_a1
 : ∀ n : ℤ, n > 0 → (∃ k : ℕ, ∃ a : Fin k → Fin 2 → ℕ, n = ∑ i : Fin k, 2^(a i 0)*3^(a i 1) ∧
-(∀ i j : Fin k, i ≠ j → ¬(2^(a i 0)*3^(a i 0) ∣ 2^(a j 0)*3^(a j 1)))) :=
+(∀ i j : Fin k, i ≠ j → ¬(2^(a i 0)*3^(a i 1) ∣ 2^(a j 0)*3^(a j 1)))) :=
 sorry
diff --git a/lean4/src/putnam_2005_b2.lean b/lean4/src/putnam_2005_b2.lean
index 0eae2428..95466b2a 100644
--- a/lean4/src/putnam_2005_b2.lean
+++ b/lean4/src/putnam_2005_b2.lean
@@ -7,13 +7,5 @@ open Nat Set
 abbrev putnam_2005_b2_solution : Set (ℕ × (ℕ → ℤ)) := sorry
 -- {(n, k) : ℕ × (ℕ → ℤ) | (n = 1 ∧ k 0 = 1) ∨ (n = 3 ∧ (k '' {0, 1, 2} = {2, 3, 6})) ∨ (n = 4 ∧ (∀ i : Fin 4, k i = 4))}
 theorem putnam_2005_b2
-(n : ℕ)
-(k : ℕ → ℤ)
-(nkpos : Prop)
-(nkeq1 : Prop)
-(nkeq2 : Prop)
-(hnkpos : nkpos = (n > 0 ∧ (∀ i : Fin n, k i > 0)))
-(hnkeq1 : nkeq1 = (∑ i : Fin n, k i = 5 * n - 4))
-(hnkeq2 : nkeq2 = (∑ i : Fin n, (1 : ℝ) / (k i) = 1))
-: (nkpos ∧ nkeq1 ∧ nkeq2) ↔ (n, k) ∈ putnam_2005_b2_solution :=
+: {((n : ℕ), (k : ℕ → ℤ)) | (n > 0) ∧ (∀ i ∈ Finset.range n, k i > 0) ∧ (∑ i ∈ Finset.range n, k i = 5 * n - 4) ∧ (∑ i : Finset.range n, (1 : ℝ) / (k i) = 1)} = putnam_2005_b2_solution :=
 sorry
diff --git a/lean4/src/putnam_2005_b3.lean b/lean4/src/putnam_2005_b3.lean
index 99d89ed0..ee0c2b40 100644
--- a/lean4/src/putnam_2005_b3.lean
+++ b/lean4/src/putnam_2005_b3.lean
@@ -8,7 +8,5 @@ abbrev putnam_2005_b3_solution : Set (Set.Ioi (0 : ℝ) → Set.Ioi (0 : ℝ)) :
 -- {f : Set.Ioi (0 : ℝ) → Set.Ioi (0 : ℝ) | ∃ c d : ℝ, c > 0 ∧ d > 0 ∧ (d = 1 → c = 1) ∧ (∀ x : Set.Ioi (0 : ℝ), f x = c * x ^ d)}
 theorem putnam_2005_b3
 (f : ℝ → ℝ)
-(fexa : Prop)
-(hfexa : fexa = (∃ a > 0, ∀ x > 0, deriv f (a / x) = x / f x))
-: (DifferentiableOn ℝ f (Set.Ioi (0 : ℝ)) ∧ fexa) ↔ (∃ f' ∈ putnam_2005_b3_solution, ∀ x : Set.Ioi (0 : ℝ), f' x = f x) :=
+: (DifferentiableOn ℝ f (Set.Ioi (0 : ℝ)) ∧ ∃ a > 0, ∀ x > 0, deriv f (a / x) = x / f x) ↔ (∃ f' ∈ putnam_2005_b3_solution, ∀ x : Set.Ioi (0 : ℝ), f' x = f x) :=
 sorry