1995 Isabelle & Coq verifications

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.

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.

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.

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.

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.

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.

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

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

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

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