1986 Isabelle & Coq verifications

coq/src/putnam_1986_a1.v

@@ -1,11 +1,9 @@
-Require Import Reals Coquelicot.Coquelicot.
+Require Import Reals Ensembles Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1986_a1_solution := 18.
 Theorem putnam_1986_a1
-    (f : R -> R := fun x => pow x 3)
-    (on_S : R -> Prop := fun x => pow x 4 - 13 * pow x 2 + 36 <= 0)
-    : exists (m: R), 
-    (forall (x: R), on_S x -> m >= f x) /\
-    (exists (x: R), on_S x -> m = f x) 
-    <-> m = putnam_1986_a1_solution.
+    (f : R -> R := fun x => pow x 3 - 3 * x)
+    (T : Ensemble R := fun x => pow x 4 + 36 <= 13 * pow x 2)
+    : (forall x : R, In R T x -> putnam_1986_a1_solution >= f x) /\
+    (exists x : R, In R T x /\ putnam_1986_a1_solution = f x).
 Proof. Admitted.

coq/src/putnam_1986_a2.v

@@ -1,5 +1,5 @@
 Require Import Nat.
 Definition putnam_1986_a2_solution := 3.
 Theorem putnam_1986_a2
-    : 10 ^ (20000) / (10 ^ (100) + 3) mod 10 = putnam_1986_a2_solution.
+    : (10 ^ (20000) / (10 ^ (100) + 3)) mod 10 = putnam_1986_a2_solution.
 Proof. Admitted.

coq/src/putnam_1986_a3.v

@@ -2,5 +2,9 @@ Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1986_a3_solution := PI / 2.
 Theorem putnam_1986_a3
-    : Series (fun n =>  1/ atan (pow (INR n) 2 + INR n + 1)) = putnam_1986_a3_solution.
+    (cot : R -> R)
+    (fcot : cot = fun t => cos t / sin t)
+    (arccot : R -> R)
+    (harccot : forall t : R, t >= 0 -> 0 < arccot t <= PI / 2 /\ cot (arccot t) = t)
+    : Series (fun n => arccot (pow (INR n) 2 + INR n + 1)) = putnam_1986_a3_solution.
 Proof. Admitted.

coq/src/putnam_1986_a6.v

@@ -1,17 +1,20 @@
 Require Import Reals Factorial Coquelicot.Coquelicot.
-Definition putnam_1986_a6_solution (m: nat -> R) (n: nat) := 
-    let fix prod_n (m: nat -> R) (n : nat) : R :=
+Definition putnam_1986_a6_solution (b: nat -> nat) (n: nat) := 
+    let fix prod_n (b : nat -> nat) (n : nat) : nat :=
         match n with
-        | O => m 0%nat
-        | S n' => m n' * prod_n m n'
+        | O => 1%nat
+        | S n' => Nat.mul (b n') (prod_n b n')
     end in
-    prod_n m n / INR (fact n).
+    INR (prod_n b n) / INR (fact n).
 Theorem putnam_1986_a6
-    (n: nat)
-    (a m: nat -> R) 
-    (ham : forall i j: nat, Nat.lt i j -> 0 < m i < m j)
-    (p : R -> R := fun x => sum_n (fun n => a n * Rpower x (m n)) n)
-    : exists (q: R -> R), forall (x: R), 
-    p x = (1 - x) ^ n * (q x) ->
-    q 1 = putnam_1986_a6_solution m n.
+    (n : nat)
+    (npos : gt n 0)
+    (a : nat -> R) 
+    (b : nat -> nat)
+    (bpos : forall i : nat, lt i n -> gt (b i) 0)
+    (binj : forall i j : nat, lt i n /\ lt j n -> (b i = b j -> i = j))
+    (f : R -> R)
+    (fpoly : exists c : nat -> R, exists deg : nat, f = fun x => sum_n (fun n => c n * x ^ n) deg)
+    (hf : forall x : R, (1 - x) ^ n * f x = 1 + sum_n (fun i => (a i) * x ^ (b i)) (n - 1))
+    : f 1 = putnam_1986_a6_solution b n.
 Proof. Admitted.

coq/src/putnam_1986_b2.v

@@ -2,11 +2,5 @@ Require Import Reals Ensembles Finite_sets Coquelicot.Coquelicot.
 Open Scope C.
 Definition putnam_1986_b2_solution (xyz : C*C*C) := xyz = (RtoC 0, RtoC 0, RtoC 0) \/ xyz = (RtoC 1, RtoC 0, RtoC (-1)) \/ xyz = (RtoC (-1), RtoC 1, RtoC 0) \/ xyz = (RtoC 0, RtoC (-1), RtoC 1).
 Theorem putnam_1986_b2
-    (n: nat)
-    (E: Ensemble (C*C*C) := fun '(x, y, z) => x * (x - 1) * 2 * y * z = y * (y - 1) * 2 * z * x /\ y * (y - 1) * 2 * z * x = z * (z - 1) + 2 * x * y) 
-    (xyz: C*C*C)
-    (x := fst (fst xyz))
-    (y := snd (fst xyz))
-    (z := snd xyz)
-    : cardinal (C*C*C) E n /\ putnam_1986_b2_solution xyz.
+    : forall T : C * C * C, putnam_1986_b2_solution T <-> exists '(x, y, z), T = (x - y, y - z, z - x) /\ x * (x - 1) + 2 * y * z = y * (y - 1) + 2 * z * x /\ y * (y - 1) + 2 * z * x = z * (z - 1) + 2 * x * y.
 Proof. Admitted.

coq/src/putnam_1986_b4.v

@@ -1,8 +1,8 @@
-Require Import Reals Coquelicot.Coquelicot.
+Require Import Reals Ranalysis Coquelicot.Coquelicot.
 Definition putnam_1986_b4_solution := True.
 Theorem putnam_1986_b4
     (G : R -> R)
     (hGeq : forall (r: R), exists (m n: Z), G r = Rabs (r - sqrt (IZR (m ^ 2 + 2 * n ^ 2))))
     (hGlb : forall (r: R), forall (m n: Z), G r <= Rabs (r - sqrt (IZR (m ^ 2 + 2 * n ^ 2))))
-    : Lim_seq (fun n => G (INR n)) = 0 <-> putnam_1986_b4_solution.
+    : filterlim G (Rbar_locally p_infty) (locally 0) <-> putnam_1986_b4_solution.
 Proof. Admitted.

isabelle/putnam_1986_a4.thy

@@ -4,10 +4,12 @@ begin
 definition putnam_1986_a4_solution::"rat\<times>rat\<times>rat\<times>rat\<times>rat\<times>rat\<times>rat" where "putnam_1986_a4_solution \<equiv> undefined"
 (* (1, 4, 2, 3, -4, 2, 1) *)
 theorem putnam_1986_a4:
-  fixes n::nat and f::nat
-  defines "f \<equiv> card {A::int^'a^'a. CARD('a) = n \<and> (\<forall>i::'a. \<forall>j::'a. (A$i$j) \<in> {-1, 0, 1}) \<and>
-    (\<exists>S::int. \<forall>f::'a\<Rightarrow>'a. f permutes UNIV \<longrightarrow> S = (\<Sum>i::'a \<in> UNIV. A$i$(f i)))}"
+  fixes n :: nat
+    and f :: nat
+  defines "f \<equiv> card {A::int^'a^'a. (\<forall>i::'a. \<forall>j::'a. (A$i$j) \<in> {-1, 0, 1}) \<and>
+    (\<exists>S::int. \<forall>p::'a\<Rightarrow>'a. p permutes UNIV \<longrightarrow> S = (\<Sum>i::'a \<in> UNIV. A$i$(p i)))}"
   assumes npos : "n > 0"
+    and hcard : "CARD('a) = n"
   shows "let (a1, b1, a2, b2, a3, b3, a4) = putnam_1986_a4_solution in (f = a1 * b1^n + a2 * b2^n + a3 * b3^n + a4)"
   sorry
 

isabelle/putnam_1986_b3.thy

@@ -1,8 +1,12 @@
-theory putnam_1986_b3 imports Complex_Main "HOL-Computational_Algebra.Polynomial" "HOL-Computational_Algebra.Primes"
+theory putnam_1986_b3 imports Complex_Main 
+"HOL-Computational_Algebra.Polynomial" 
+"HOL-Computational_Algebra.Primes"
 begin
 
 theorem putnam_1986_b3:
-  fixes cong::"(int poly) \<Rightarrow> (int poly) \<Rightarrow> int \<Rightarrow> bool" and n p::nat and f g h r s::"int poly"
+  fixes cong :: "(int poly) \<Rightarrow> (int poly) \<Rightarrow> int \<Rightarrow> bool"
+    and n p :: nat 
+    and f g h r s :: "int poly"
   defines "cong \<equiv> \<lambda>f. \<lambda>g. \<lambda>m. \<forall>i::nat. m dvd (coeff (f - g) i)"
   assumes nppos : "n > 0 \<and> p > 0"
     and pprime : "prime p"

isabelle/putnam_1986_b4.thy

@@ -5,8 +5,8 @@ definition putnam_1986_b4_solution::bool where "putnam_1986_b4_solution \<equiv>
 (* True *)
 theorem putnam_1986_b4:
   fixes G::"real\<Rightarrow>real"
-  defines "G \<equiv> \<lambda>r. (LEAST y. \<exists> m n::int. y = \<bar>r - sqrt (m^2 + 2*n^2)\<bar>)"
-  shows "(G \<longlonglongrightarrow> 0) \<longleftrightarrow> putnam_1986_b4_solution"
+  defines "G \<equiv> \<lambda>r. (LEAST y. \<exists> m \<in> \<int>. \<exists> n \<in> \<int>. y = \<bar>r - sqrt (m^2 + 2*n^2)\<bar>)"
+  shows "filterlim G (nhds 0) at_top \<longleftrightarrow> putnam_1986_b4_solution"
   sorry
 
 end

isabelle/putnam_1986_b6.thy

@@ -1,8 +1,12 @@
-theory putnam_1986_b6 imports Complex_Main "HOL-Algebra.Ring" "HOL-Analysis.Finite_Cartesian_Product"
+theory putnam_1986_b6 imports Complex_Main 
+"HOL-Algebra.Ring" 
+"HOL-Analysis.Finite_Cartesian_Product"
 begin
 
 theorem putnam_1986_b6:
-  fixes n::nat and F::"('a::{semiring_1, minus}, 'm) ring_scheme" (structure) and A B C D::"'a^'b^'b"
+  fixes n :: nat 
+    and F :: "('a::{semiring_1, minus}, 'm) ring_scheme" (structure) 
+    and A B C D :: "'a^'b^'b"
   assumes npos : "n > 0"
     and Ffield : "field F"
     and matdim : "CARD('b) = n"

lean4/src/putnam_1986_a1.lean

@@ -8,5 +8,5 @@ theorem putnam_1986_a1
 (hS : S = {x : ℝ | x ^ 4 + 36 ≤ 13 * x ^ 2})
 (f : ℝ → ℝ)
 (hf : f = fun x ↦ x ^ 3 - 3 * x)
-: (∀ x ∈ S, f x ≤ putnam_1986_a1_solution ∧ ∃ x ∈ S, f x = putnam_1986_a1_solution) :=
+: (∀ x ∈ S, f x ≤ putnam_1986_a1_solution) ∧ (∃ x ∈ S, f x = putnam_1986_a1_solution) :=
 sorry