Merge branch 'main' of https://github.com/trishullab/PutnamBench into…

… george

.github/workflows/lean.yml

@@ -37,3 +37,18 @@ jobs:
       working-directory: lean4
       run: |
         lake exe cache pack
+
+    - name: Insert solutions
+      working-directory: lean4
+      run: |
+        python scripts/rewrite_solutions.py
+
+    - name: Build
+      working-directory: lean4
+      run: |
+        lake build putnam_with_solutions
+
+    - name: Save olean cache
+      working-directory: lean4
+      run: |
+        lake exe cache pack

coq/src/putnam_1999_a2.v

@@ -1,7 +1,8 @@
-From mathcomp Require Import ssrnat ssrnum ssralg fintype poly.
+From mathcomp.analysis Require Import reals. From mathcomp Require Import ssrnat ssrnum ssralg fintype poly.
 Open Scope ring_scope.
 Theorem putnam_1999_a2
-    (R: numDomainType)
+    (R : realType)
     (p : {poly R})
-    : forall x, p.[x] > 0 = true -> exists (k : nat) (f : nat -> {poly R}), p = \sum_(i < k) (f i)*(f i). 
+    (hpos : forall x, (p.[x] >= 0) = true)
+    : exists (k : nat) (f : nat -> {poly R}), p = \sum_(i < k) ((f i)*(f i)).
 Proof. Admitted.

coq/src/putnam_1999_a3.v

@@ -2,6 +2,6 @@ Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_1999_a3
     (f : R -> R := fun x => 1/(1- 2 * x - x^2))
     (a : nat -> R)
-    (hf : exists epsilon : R, epsilon > 0 /\ (forall x : R, 0 < Rabs (x) < epsilon -> filterlim (fun n : nat => sum_n (fun i => a i * x^i) n) eventually (locally (f x))))
-    : forall n : nat, ge n 0 -> (exists m : nat, (a n)^2 + (a (S n))^2 = a m).
+    (hf : exists epsilon : R, epsilon > 0 /\ (forall x : R, 0 <= Rabs (x) < epsilon -> filterlim (fun n : nat => sum_n (fun i => a i * x^i) n) eventually (locally (f x))))
+    : forall n : nat, exists m : nat, (a n)^2 + (a (S n))^2 = a m.
 Proof. Admitted.

coq/src/putnam_1999_a4.v

@@ -1,5 +1,5 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_1999_a4_solution := 9/32.
+Definition putnam_1999_a4_solution : R := 9/32.
 Theorem putnam_1999_a4: 
-    Series (fun m => Series (fun n => (INR m ^ 2 * INR n) / (3 ^ m *(INR n * 3 ^ m + INR m * 3 ^ n)))) = putnam_1999_a4_solution.
+    Series (fun m => Series (fun n => (INR (m + 1) ^ 2 * INR (n + 1)) / (3 ^ (m + 1) * (INR (n + 1) * 3 ^ (m + 1) + INR (m + 1) * 3 ^ (n + 1))))) = putnam_1999_a4_solution.
 Proof. Admitted.

coq/src/putnam_1999_a5.v

@@ -1,5 +1,5 @@
 Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_1999_a5
-    (p : (nat -> R) -> R -> R := fun a x => sum_n (fun i => a i * x ^ i) 2000)
-    : forall (a: nat -> R), exists (c: R), Rabs (p a 0) <= c * RInt (fun  x => Rabs (p a x)) (-1) 1.
+    (p : (nat -> R) -> R -> R := fun a x => sum_n (fun i => a i * x ^ i) 1999)
+    : exists (c: R), forall (a: nat -> R), Rabs (p a 0) <= c * RInt (fun x => Rabs (p a x)) (-1) 1.
 Proof. Admitted.

coq/src/putnam_1999_a6.v

@@ -1,11 +1,11 @@
 Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_1999_a6
-    (A := fix a (n: nat) :=
+    (A : nat -> R := fix a (n: nat) :=
         match n with 
         | O => 1
         | S O => 2
         | S (S O) => 24
-        | S (S ((S n'') as n') as n) => (6 * a n ^ 2 * a n'' - 8 * a n * a n' ^ 2) / (a n' * a n'')
-    end) 
-    : forall (n: nat), exists (k: nat), A n = INR (n * k).
+        | S (S ((S n'') as n') as n) => (6 * (a n) ^ 2 * a n'' - 8 * a n * (a n') ^ 2) / (a n' * a n'')
+    end)
+    : forall (n: nat), exists (k: Z), A n = INR (n + 1) * IZR k.
 Proof. Admitted.

coq/src/putnam_1999_b2.v

@@ -4,7 +4,7 @@ Theorem putnam_1999_b2
     (n: nat)
     (p : R -> R := fun x => sum_n (fun i => a1 i * x ^ i) n)
     (q : R -> R := fun x => sum_n (fun i => a2 i * x ^ i) 2)
-    : forall (x: R), p x = q x * (Derive_n (fun x => p x) 2) x /\
-    exists (r1 r2: R), r1 <> r2 /\ p r1 = 0 /\ p r2 = 0 ->
-    exists (roots: list R), length roots = n /\ NoDup roots /\ forall (r: R), In r roots -> p r = 0.
+    (hP : forall (x: R), p x = q x * (Derive_n p 2) x)
+    : (exists (r1 r2: R), r1 <> r2 /\ p r1 = 0 /\ p r2 = 0) ->
+    (exists (roots: list R), length roots = n /\ NoDup roots /\ (forall (r: R), In r roots -> p r = 0)).
 Proof. Admitted.

coq/src/putnam_1999_b4.v

@@ -2,5 +2,8 @@ Require Import Reals Coquelicot.Derive.
 Open Scope R_scope.
 Theorem putnam_1999_b4
     (f: R -> R)
-    : continuity (Derive_n f 3) -> forall (x: R), f x > 0 /\ (Derive_n f 1) x > 0 /\ (Derive_n f 2) x > 0 /\ (Derive_n f 3) x > 0 -> forall (x: R), (Derive_n f 3) x <= f x -> forall (x: R), (Derive_n f 1) x < 2 * f x.
+    (f_cont : (forall n : nat, (le 1 n /\ le n 3) -> (forall x : R, ex_derive_n f n x)) /\ continuity (Derive_n f 3))
+    (f_pos : forall (x: R), f x > 0 /\ (Derive_n f 1) x > 0 /\ (Derive_n f 2) x > 0 /\ (Derive_n f 3) x > 0)
+    (hf : forall (x: R), (Derive_n f 3) x <= f x)
+    : forall (x: R), (Derive_n f 1) x < 2 * f x.
 Proof. Admitted.

coq/src/putnam_1999_b6.v

@@ -1,5 +1,7 @@
 Require Import Reals List Znumtheory.
 Theorem putnam_1999_b6
     (A : list Z)
-    : forall (x: Z), In x A -> x > 1 -> forall (n: Z), exists (s: Z), In s A -> Zis_gcd s n 1 \/ Zis_gcd s n s -> exists (s: Z) (t: Z) (p: Z), In s A /\ In t A /\ prime p -> Zis_gcd s t p.
+    (Age1 : forall (x: Z), In x A -> x > 1)
+    (hgcd : forall (n: Z), exists (s: Z), In s A /\ (Zis_gcd s n 1 \/ Zis_gcd s n s))
+    : exists (s: Z) (t: Z) (p: Z), In s A /\ In t A /\ Zis_gcd s t p /\ prime p.
 Proof. Admitted.

coq/src/putnam_2000_a1.v

@@ -1,7 +1,7 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_2000_a1_solution (x A: R) := 0 < x < A ^ 2.
+Definition putnam_2000_a1_solution : R -> (R -> Prop) := (fun A : R => (fun x : R => 0 < x < A ^ 2)).
 Theorem putnam_2000_a1
     (A: R)
     (hA : A > 0)
-    : forall (x: nat -> R), Series x = A -> putnam_2000_a1_solution (Series (fun j => x j ^ 2)) A.
+    : forall SS : R, ((exists x : nat -> R, (forall j : nat, x j > 0) /\ Series x = A /\ Series (fun j => (x j) ^ 2) = SS) <-> (putnam_2000_a1_solution A) SS).
 Proof. Admitted.

coq/src/putnam_2000_a4.v

@@ -1,4 +1,4 @@
 Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_2000_a4
-    : ex_finite_lim_seq (fun n => sum_n (fun x => sin (INR x) * sin ((INR x) ^ 2)) n).
+    : ex_finite_lim_seq (fun B : nat => RInt (fun x : R => sin x * sin (x ^ 2)) 0 (INR B)).
 Proof. Admitted.

coq/src/putnam_2000_a6.v

@@ -4,6 +4,6 @@ Theorem putnam_2000_a6
     (coeff : nat -> Z)
     (f : R -> R := fun x => sum_n (fun i => (IZR (coeff i)) * (x^i)) n)
     (a : nat -> R)
-    (ha : a O = 0 /\ forall i : nat, a (S n) = f (a n))
+    (ha : a O = 0 /\ forall i : nat, a (S i) = f (a i))
     : (exists m : nat, gt m 0 /\ a m = 0) -> (a (S O) = 0 \/ a (S (S O)) = 0).
 Proof. Admitted.

coq/src/putnam_2000_b1.v

@@ -1,9 +1,12 @@
-Require Import List Nat Reals ZArith.
+Require Import List Nat Reals ZArith Ensembles Finite_sets.
 Open Scope Z.
-Theorem putnam_2000_b1 
-    (a b c: nat -> Z)
-    (n: nat)
-    (habc : forall (j: nat), and (le 1 j) (le j n) -> Z.odd (a j) = true \/ Z.odd (b j) = true \/ Z.odd (c j) = true)
-    : exists (l: list nat), ge (length l) (4 * n / 7) /\ forall (j: nat), In j l -> and (le 1 j) (le j n)
-    -> exists (r s t: Z), Z.odd (Z.add (Z.add (Z.mul r (a j)) (Z.mul s (b j))) (Z.mul t (c j))) = true.
+Theorem putnam_2000_b1
+    (n : nat)
+    (a b c : nat -> Z)
+    (SS : Z -> Z -> Z -> Ensemble nat := (fun r s t : Z => (fun j : nat => le 1 j /\ le j n /\ Z.odd (Z.add (Z.add (Z.mul r (a j)) (Z.mul s (b j))) (Z.mul t (c j))) = true)))
+    (SSsize : Z -> Z -> Z -> nat)
+    (nge1 : ge n 1)
+    (habc : forall j : nat, ((le 1 j) /\ (le j n)) -> (Z.odd (a j) = true \/ Z.odd (b j) = true \/ Z.odd (c j) = true))
+    (hSSsize : forall r s t : Z, cardinal nat (SS r s t) (SSsize r s t))
+    : exists r s t : Z, Rge (INR (SSsize r s t)) (Rdiv (Rmult 4 (INR n)) 7).
 Proof. Admitted.

coq/src/putnam_2000_b2.v

@@ -1,5 +1,5 @@
 Require Import Nat Reals.
 Open Scope R.
 Theorem putnam_2000_b2 
-    : forall (n m: nat), and (ge n m) (ge m 1) -> exists (c: Z), INR (gcd m n) / INR n * Binomial.C n m = IZR c.
+    : forall (n m: nat), and (ge n m) (ge m 1) -> exists (c: Z), (INR (gcd m n) / INR n) * Binomial.C n m = IZR c.
 Proof. Admitted.

coq/src/putnam_2000_b4.v

@@ -1,6 +1,7 @@
-Open Scope R_scope.
-Require Import Reals.
+Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_2000_b4
-    (f: R -> R)
-    : continuity f -> forall x, f (2*x*x-1) = 2*x*(f x) -> forall x, -1 <= x <= 1 -> f x = 0. 
+    (f : R -> R)
+    (hf : forall x : R, f (2*x*x-1) = 2*x*(f x))
+    (f_cont : continuity f)
+    : forall x : R, -1 <= x <= 1 -> f x = 0. 
 Proof. Admitted.

coq/src/putnam_2000_b5.v

@@ -1,8 +1,8 @@
 Require Import ZArith Ensembles Finite_sets.
 Theorem putnam_2000_b5
-    (S : nat -> Ensemble Z)
-    (hSfin : forall n : nat, exists m : nat, cardinal _ (S n) m)
-    (hSpos : forall n : nat, forall s : Z, In _ (S n) s -> Z.gt s 0)
-    (hSdef : forall n : nat, forall a : Z, (In _ (S (n + 1)) a) <-> ((In _ (S n) (Z.sub a 1) /\ ~ (In _ (S n) a)) \/ (In _ (S n) a /\ ~ (In _ (S n) (Z.sub a 1)))))
-    : forall n : nat, exists N : nat, N >= n /\ Same_set _ (S N) (Union _ (S 0) (fun i : Z => exists a : Z, In _ (S 0) a /\ i = Z.add a (Z.of_nat N))).
+    (SS : nat -> Ensemble Z)
+    (hSSfin : forall n : nat, exists m : nat, cardinal _ (SS n) m)
+    (hSSpos : forall n : nat, forall s : Z, In _ (SS n) s -> Z.gt s 0)
+    (hSSdef : forall n : nat, forall a : Z, (In _ (SS (n + 1)) a) <-> ((In _ (SS n) (Z.sub a 1) /\ ~ (In _ (SS n) a)) \/ (In _ (SS n) a /\ ~ (In _ (SS n) (Z.sub a 1)))))
+    : forall n : nat, exists N : nat, N >= n /\ Same_set _ (SS N) (Union _ (SS 0) (fun i : Z => exists a : Z, In _ (SS 0) a /\ i = Z.add a (Z.of_nat N))).
 Proof. Admitted.

coq/src/putnam_2001_a1.v

@@ -1,6 +1,7 @@
 Require Import Ensembles RelationClasses.
 Theorem putnam_2001_a1
     (A : Type)
-    (op: A->A->A)
-    : (forall (a b: A), op (op a b) a = b) -> (forall (a b: A), op a (op b a) = b).
+    (op : A->A->A)
+    (hop : forall (a b: A), op (op a b) a = b)
+    : forall (a b: A), op a (op b a) = b.
 Proof. Admitted.

coq/src/putnam_2001_a3.v

@@ -1,7 +1,8 @@
-Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_2001_a3_solution (m: Z) := exists (n: Z), m = Z.mul n n \/ m = Z.mul 2 (Z.mul n n).
+Require Import Reals Coquelicot.Coquelicot Ensembles.
+Definition putnam_2001_a3_solution : Ensemble Z := (fun m : Z => exists (n: Z), m = Z.mul n n \/ m = Z.mul 2 (Z.mul n n)).
 Theorem putnam_2001_a3
     (P : Z -> R -> R := fun m x => x ^ 4 - (2 * IZR m + 4) * x ^ 2 + (IZR m - 2) ^ 2)
     (p : (nat -> Z) -> R -> nat -> R := fun a x n => sum_n (fun i => IZR (a i) * x ^ i) n)
-    : forall (m: Z), exists (a1 a2: nat -> Z) (n1 n2: nat), forall (x: R), P m x = p a1 x n1 * p a2 x n2 <-> putnam_2001_a3_solution m.
+    : forall (m: Z), (exists (a1 a2: nat -> Z) (n1 n2: nat), (exists i : nat, gt i 0 /\ le i n1 /\ a1 i <> 0%Z) /\ (exists i : nat, gt i 0 /\ le i n2 /\ a2 i <> 0%Z) /\
+    (forall (x: R), P m x = p a1 x n1 * p a2 x n2)) <-> putnam_2001_a3_solution m.
 Proof. Admitted.

coq/src/putnam_2001_b2.v

@@ -1,7 +1,7 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_2001_b2_solution (x y: R) := x = (3 ^ (1 / 5) + 1) / 2 /\ y = (3 ^ (1 / 5) - 1) / 2.
+Definition putnam_2001_b2_solution : R -> R -> Prop := (fun x y : R => x = (3 ^ (1 / 5) + 1) / 2 /\ y = (3 ^ (1 / 5) - 1) / 2).
 Theorem putnam_2001_b2
     : forall (x y: R), 
-    1 / x + 1 / (2 * y) = (x ^ 2 + 3 * y ^ 2) * (3 * x ^ 2 + y ^ 2) /\
-    1 / x - 1 / (2 * y) = 2 * (y ^ 4 - x ^ 4) <-> putnam_2001_b2_solution x y.
+    (1 / x + 1 / (2 * y) = (x ^ 2 + 3 * y ^ 2) * (3 * x ^ 2 + y ^ 2) /\
+    1 / x - 1 / (2 * y) = 2 * (y ^ 4 - x ^ 4)) <-> putnam_2001_b2_solution x y.
 Proof. Admitted.

coq/src/putnam_2001_b3.v

@@ -1,8 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_2001_b3_solution := 3.
+Definition putnam_2001_b3_solution : R := 3.
 Theorem putnam_2001_b3
-    (n: nat)
-    (hn : ge n 0)
-    (closest : nat -> R := fun n => let n := INR n in Rmin ((n - sqrt n) - IZR (floor (n - sqrt n))) (IZR (floor (n + 1 - sqrt n)) - (n - sqrt n)))
-    : Series (fun n => sum_n (fun n => (Rpower 2 (closest n) + Rpower 2 (- closest n)) / (2 ^ n)) n) = putnam_2001_b3_solution.
+    (closest : nat -> R := (fun n : nat => IZR (floor (sqrt (INR n) + 0.5))))
+    : Series (fun n : nat => sum_n_m (fun n' : nat => (Rpower 2 (closest n') + Rpower 2 (-closest n')) / (2 ^ n')) 1 n) = putnam_2001_b3_solution.
 Proof. Admitted.

coq/src/putnam_2001_b4.v

@@ -1,13 +1,13 @@
-Require Import Basics List QArith. From mathcomp Require Import bigop fintype seq ssrbool ssreflect ssrnat ssrnum ssralg    finfun. 
+Require Import Basics List QArith. From mathcomp Require Import bigop fintype seq ssrbool ssreflect ssrnat ssrnum ssralg finfun. 
 Open Scope Q_scope.
-Definition putnam_2001_b4_solution := False.
-Definition image (f: Q -> Q) := fun y => exists(x: Q), f x = y.
+Definition putnam_2001_b4_solution : Prop := True.
+Definition image (f: Q -> Q) := fun y => exists (x: Q), (~ In x [:: -1; 0; 1]) /\ f x = y.
 Fixpoint 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.
 Theorem putnam_2001_b4
     (f : Q -> Q := fun x => x - 1 / x)
-    : exists (x: Q), ~ In x [:: -1; 0; 1] -> forall (n: nat), (image (compose_n f n)) x <-> putnam_2001_b4_solution.
+    : (~exists (x: Q), (~ In x [:: -1; 0; 1]) /\ (forall (n: nat), ge n 1 -> (image (compose_n f n)) x)) <-> putnam_2001_b4_solution.
 Proof. Admitted.

coq/src/putnam_2001_b5.v

@@ -3,6 +3,7 @@ Theorem putnam_2001_b5
     (a b: R) 
     (g: R -> R)
     (hab : 0 < a < 1/2 /\ 0 < b < 1/2)
-    (hg : continuity g)
-    : forall (x: R), g (g x) = a * g x + b * x -> exists (c: R), g x = c * x.
+    (gcont : continuity g)
+    (hg : forall (x: R), g (g x) = a * g x + b * x)
+    : exists c : R, forall x : R, g x = c * x.
 Proof. Admitted.

coq/src/putnam_2001_b6.v

@@ -1,7 +1,7 @@
 Require Import Nat Reals Coquelicot.Coquelicot.
-Definition putnam_2001_b6_solution := True.
+Definition putnam_2001_b6_solution : Prop := True.
 Theorem putnam_2001_b6
-    (a: nat -> R)
-    (ha : forall (i j: nat), lt i j -> a i < a j) 
-    : Lim_seq (fun n => a n / INR n) = 0 -> forall (n: nat), exists (m: nat), gt m n /\ forall (i: nat), and (le 1 i) (le i (n - 1)) -> a (sub n i) + a (add n i) < 2 * a n /\ a (sub m i) + a (add m i) < 2 * a m.
+    (aposinc : (nat -> R) -> Prop := (fun a : nat -> R => forall n : nat, ge n 1 -> (a n > 0 /\ a n < a (add n 1))))
+    (alim : (nat -> R) -> Prop := (fun a : nat -> R => Lim_seq (fun n : nat => a (add n 1) / INR (add n 1)) = 0))
+    : (forall a : nat -> R, (aposinc a /\ alim a) -> forall m : nat, exists n : nat, gt n m /\ (forall i : nat, (le 1 i /\ le i (n - 1)) -> a (sub n i) + a (add n i) < 2 * a n)) <-> putnam_2001_b6_solution.
 Proof. Admitted.

isabelle/putnam_1999_a2.thy

@@ -5,7 +5,7 @@ begin
 theorem putnam_1999_a2:
   fixes p :: "real poly"
   assumes hpos : "\<forall>x. poly p x \<ge> 0"
-  shows "\<exists>S :: real poly set . \<forall>x. finite S \<and> poly p x = (\<Sum>s \<in> S. (poly s x)^2)"
+  shows "\<exists>S :: real poly set . finite S \<and> (\<forall>x. poly p x = (\<Sum>s \<in> S. (poly s x)^2))"
   sorry
 
 end

isabelle/putnam_1999_a4.thy

@@ -5,7 +5,7 @@ begin
 definition putnam_1999_a4_solution :: real where "putnam_1999_a4_solution \<equiv> undefined"
 (* 9 / 32 *)
 theorem putnam_1999_a4:
-  shows "(\<Sum> m :: nat. \<Sum> n :: nat. (m + 1) ^ 2 * (n + 1) / (3 ^ (m + 1) * ((n + 1) * 3 ^ (m + 1) + (m + 1) * 3 ^ (n + 1)))) = putnam_1999_a4_solution"
+  shows "(\<Sum> m :: nat. \<Sum> n :: nat. ((m + 1) ^ 2 * (n + 1)) / (3 ^ (m + 1) * ((n + 1) * 3 ^ (m + 1) + (m + 1) * 3 ^ (n + 1)))) = putnam_1999_a4_solution"
   sorry
 
 end

isabelle/putnam_1999_a6.thy

@@ -8,7 +8,7 @@ theorem putnam_1999_a6:
   and ha2: "a 2 = 2"
   and ha3: "a 3 = 24"
   and hange4: "\<forall> n :: nat. n \<ge> 4 \<longrightarrow> a n = (6 * (a (n - 1)) ^ 2 * (a (n - 3)) - 8 * (a (n - 1)) * (a (n - 2)) ^ 2) / (a (n - 2) * a (n - 3))"
-  shows "\<forall> n. n \<ge> 1 \<longrightarrow> (\<exists> k :: int. a n = k * n)"
+  shows "\<forall> n :: nat. n \<ge> 1 \<longrightarrow> (\<exists> k :: int. a n = k * n)"
   sorry
 
 end

isabelle/putnam_1999_b4.thy

@@ -4,7 +4,7 @@ begin
 
 theorem putnam_1999_b4:
   fixes f :: "real\<Rightarrow>real"
-  assumes f_cont : "continuous_on UNIV ((deriv^^3) f)"
+  assumes f_cont : "\<forall>n::nat\<in>{0..2}. ((deriv^^n) f) C1_differentiable_on UNIV"
     and f_pos : "\<forall>x. f x > 0"
     and f'_pos : "\<forall>x. deriv f x > 0"
     and f''_pos : "\<forall>x. (deriv^^2) f x > 0"

isabelle/putnam_1999_b6.thy

@@ -7,7 +7,7 @@ theorem putnam_1999_b6:
   assumes S_fin: "finite S"
     and Sge1: "\<forall>s \<in> S. s > 1"
     and hgcd: "\<forall>n::int. \<exists>s \<in> S. (gcd s n) = 1 \<or> (gcd s n) = s"
-  shows "\<exists> s \<in> S. \<exists> t \<in> S. prime(gcd s t)"
+  shows "\<exists> s \<in> S. \<exists> t \<in> S. prime (gcd s t)"
   sorry
 
 end

isabelle/putnam_2000_a5.thy

@@ -1,6 +1,7 @@
 theory putnam_2000_a5 imports
 Complex_Main
 "HOL-Analysis.Finite_Cartesian_Product"
+"HOL-Analysis.Elementary_Metric_Spaces"
 begin
 
 theorem putnam_2000_a5:
@@ -9,7 +10,7 @@ theorem putnam_2000_a5:
   and S :: "(real^2) set"
   assumes rpos: "r > 0"
   and Scard: "finite S \<and> card S = 3"
-  and pint: "\<forall> p \<in> S. p$1 = round (p$1) \<and> p$2 = round (p$2)"
+  and pint: "\<forall> p \<in> S. p$1 \<in> \<int> \<and> p$2 \<in> \<int>"
   and pcirc: "\<forall> p \<in> S. p \<in> sphere z r"
   shows "\<exists> p \<in> S. \<exists> q \<in> S. dist p q \<ge> r powr (1 / 3)"
   sorry

isabelle/putnam_2000_b1.thy

@@ -3,7 +3,7 @@ begin
 
 (* uses (nat \<Rightarrow> int) instead of (Fin N \<Rightarrow> int) *)
 theorem putnam_2000_b1:
-  fixes n :: nat
+  fixes N :: nat
   and a b c :: "nat \<Rightarrow> int"
   assumes Nge1: "N \<ge> 1"
   and hodd: "\<forall>j::nat\<in>{0..(N-1)}. odd (a j) \<or> odd (b j) \<or> odd (c j)"

isabelle/putnam_2000_b4.thy

@@ -3,9 +3,9 @@ begin
 
 theorem putnam_2000_b4:
   fixes f :: "real \<Rightarrow> real"
-  assumes hf : "\<forall>x. f (2 * x^2  - 1) = 2 * x * f x"
+  assumes hf : "\<forall>x::real. f (2 * x^2 - 1) = 2 * x * f x"
     and f_cont : "continuous_on UNIV f"
-  shows "\<forall>x. x \<ge> -1 \<and> x \<le> 1 \<longrightarrow> f x = 0"
+  shows "\<forall>x::real. x \<ge> -1 \<and> x \<le> 1 \<longrightarrow> f x = 0"
   sorry
 
 end

isabelle/putnam_2001_a3.thy

@@ -8,7 +8,7 @@ definition putnam_2001_a3_solution :: "int set" where "putnam_2001_a3_solution \
 theorem putnam_2001_a3:
   fixes P :: "int \<Rightarrow> int poly"
   defines "P \<equiv> \<lambda> m :: int. monom 1 4 - monom (2 * m + 4) 2 + monom ((m - 2) ^ 2) 0"
-  shows "{m :: int. \<exists> a b :: int poly. P m = a * b \<and> (\<exists> n \<in> {1..}. coeff a n \<noteq> 0) \<and> (\<exists> n \<in> {1..}. coeff b n \<noteq> 0)} = putnam_2001_a3_solution"
+  shows "{m :: int. \<exists> a b :: int poly. P m = a * b \<and> degree a > 0 \<and> degree b > 0} = putnam_2001_a3_solution"
   sorry
 
 end

isabelle/putnam_2001_a5.thy

@@ -2,7 +2,7 @@ theory putnam_2001_a5 imports Complex_Main
 begin
 
 theorem putnam_2001_a5:
-  shows "\<exists>! (a :: int). \<exists>! (n :: nat). a > 0 \<and> \<and> n > 0 \<and> a^(n+1) - (a+1)^n = 2001"
+  shows "\<exists>! (a :: int). \<exists>! (n :: nat). a > 0 \<and> n > 0 \<and> a^(n+1) - (a+1)^n = 2001"
   sorry
 
 end

isabelle/putnam_2001_b4.thy

@@ -7,8 +7,7 @@ theorem putnam_2001_b4:
   fixes f :: "rat \<Rightarrow> rat" and S :: "rat set"
   defines "f \<equiv> \<lambda>x. x - 1/x"
     and "S \<equiv> \<rat> - {-1, 0, 1}"
-  shows "putnam_2001_b4_solution = 
-    ((\<Inter>n \<in> {1..}. image (f^^n) S) = {}) "
+  shows "putnam_2001_b4_solution \<longleftrightarrow> ((\<Inter>n::nat \<in> {1..}. image (f^^n) S) = {}) "
   sorry
 
 end

isabelle/putnam_2001_b6.thy

@@ -6,7 +6,7 @@ definition putnam_2001_b6_solution :: bool where "putnam_2001_b6_solution \<equi
 (* True *)
 theorem putnam_2001_b6:
   fixes aposinc alim :: "(nat \<Rightarrow> real) \<Rightarrow> bool"
-  defines "aposinc \<equiv> \<lambda> a. \<forall> n \<ge> 1. a n > 0 \<and> a n < a (n + 1)"
+  defines "aposinc \<equiv> \<lambda> a. \<forall> n::nat \<ge> 1. a n > 0 \<and> a n < a (n + 1)"
   and "alim \<equiv> \<lambda> a. (\<lambda> n :: nat. a (n + 1) / (n + 1)) \<longlonglongrightarrow> 0"
   shows "(\<forall> a :: nat \<Rightarrow> real. (aposinc a \<and> alim a) \<longrightarrow> infinite {n :: nat. n > 0 \<and> (\<forall> i \<in> {1 .. n - 1}. a (n - i) + a (n + i) < 2 * a n)}) \<longleftrightarrow> putnam_2001_b6_solution"
   sorry