Fix Isabelle, Coq formalizations pursuant to #229, #238, #243.

coq/src/putnam_2017_a2.v

@@ -9,12 +9,9 @@ Local Open Scope ring_scope.
 
 Variable R : realType.
 Theorem putnam_2017_a2
-    (Q : nat -> R -> R)
-    (hQbase : forall x : R, Q 0%nat x = 1 /\ Q 1%nat x = x)
-    (hQn : forall n : nat, ge n 2 -> forall x : R, Q n x = ((Q (n.-1) x) ^+ 2 - 1) / (Q (n.-2) x))
-    : forall n : nat, gt n 0 -> 
-        exists P : {poly R}, 
-            size P = n.+1 /\ 
-            (forall i : nat, exists c : int, P`_i = c%:~R) /\
-            Q n = (fun x : R => P.[x]).
+    (Q : nat -> {poly R})
+    (hQbase : Q 0%nat = 1%:P /\ Q 1%nat = 'X)
+    (hQn : forall n : nat, Q (n.+2) * Q n = Q (n.+1) ^+ 2 - 1%:P)
+    (n : nat) (hn : lt 0 n) : 
+    exists P : {poly int}, Q n = map_poly intr P.
 Proof. Admitted.

coq/src/putnam_2022_a1.v

@@ -1,5 +1,5 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_2022_a1_solution : R -> R -> Prop := (a = 0 /\ b = 0) \/ (Rabs a >= 1) \/ (Rabs a < 1 /\ (b < ln (1 - (1 - sqrt (1 - a ^ 2)) / a) ^ 2 - Rabs a * (1 - (1 - sqrt (1 - a ^ 2)) / a) \/ b > ln (1 - (1 + sqrt (1 - a ^ 2) / a) ^ 2 - Rabs a * (1 + sqrt (1 - a ^ 2) / a)))).
+Definition putnam_2022_a1_solution : R -> R -> Prop := fun a b => (a = 0 /\ b = 0) \/ (Rabs a >= 1) \/ (0 < Rabs a < 1 /\ (b < ln (1 + ((1 - sqrt (1 - a ^2))/ a) ^ 2) - a * (1 - sqrt (1 - a ^ 2) / a) \/ b > ln (1 + ((1 + sqrt (1 - a ^ 2)) / a) ^ 2) - a * (1 + sqrt (1 - a ^ 2) / a))).
 Theorem putnam_2022_a1 
     : forall a b : R, (exists! (x: R), a * x + b = ln (1 + x ^ 2) / ln 10) <-> putnam_2022_a1_solution a b. 
 Proof. Admitted.

isabelle/putnam_1963_a3.thy

@@ -13,9 +13,8 @@ theorem putnam_1963_a3:
   assumes hP : "(\<forall> x. P 0 x = x) \<and> (\<forall> (i :: nat) (y :: real \<Rightarrow> real). P (i + 1) y = P i (\<lambda> x. x * deriv y x - (real_of_nat i) * y x))"
     and hn : "0 < n"
     and hf : "continuous_on {1..} f"
-  shows "((\<forall> k :: nat < n. 
-           ((deriv^^k) y) C1_differentiable_on {1..} ∧
-           ((deriv^^k) y) 1 = 0) \<and>
+    and hy : "\<forall> k :: nat < n. ((deriv^^k) y) C1_differentiable_on {1..}"
+  shows "((\<forall> k :: nat < n. ((deriv^^k) y) 1 = 0) \<and>
         (\<forall> x :: real. x \<ge> 0 \<longrightarrow> (P n y) x = f x)) \<longleftrightarrow>
         (\<forall> x :: real \<ge> 1. y x = interval_lebesgue_integral lebesgue 1 (ereal x) (putnam_1963_a3_solution f n x))"
   sorry

isabelle/putnam_1984_a6.thy

@@ -2,18 +2,18 @@ theory putnam_1984_a6 imports Complex_Main
 "HOL-Number_Theory.Cong"
 begin
 
-definition putnam_1984_a6_solution :: "bool \<times> nat" where "putnam_1984_a6_solution \<equiv> undefined"
-(* (True, 4) *)
+definition putnam_1984_a6_solution :: "nat" where "putnam_1984_a6_solution \<equiv> undefined"
+(* 4 *)
 theorem putnam_1984_a6:
   fixes f :: "nat \<Rightarrow> nat"
-    and kadistinct :: "nat \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool"
-    and gpeq :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> bool"
-  defines "kadistinct \<equiv> \<lambda> (k :: nat) (a :: nat \<Rightarrow> nat). k \<ge> 1 \<and> (\<forall> i j :: nat. (i < k \<and> j < k \<and> i \<noteq> j) \<longrightarrow> a i \<noteq> a j)"
-    and "gpeq \<equiv> \<lambda> (g :: nat \<Rightarrow> nat) (p :: nat). p > 0 \<and> (\<forall> (s :: nat) \<ge> 1. g s = g (s + p))"
-  assumes hf : "\<forall> n > 0. f n = (if [fact n \<noteq> 0] (mod 10) then ((fact n) mod 10) else f ((fact n) div 10))" 
-  shows "let (b, n) = putnam_1984_a6_solution in \<exists> g :: nat \<Rightarrow> nat. 
-(\<forall> (k :: nat) (a :: nat \<Rightarrow> nat). kadistinct k a \<longrightarrow> g (\<Sum> i=0..(k-1). a i) = f (\<Sum> i=0..(k-1). 5^(a i)))
-\<and> (if b then gpeq g n \<and> (\<forall> p :: nat. gpeq g p \<longrightarrow> p \<ge> n) else \<not>(\<exists> p :: nat. gpeq g p))"
+    and IsPeriodicFrom :: "nat \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> bool"
+    and P :: "nat \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> bool"
+  assumes hf : "\<forall> n > 0. f n = (if [fact n \<noteq> 0] (mod 10) then ((fact n) mod 10) else f ((fact n) div 10))"
+    and P_def : "\<forall> x g p. P x g p \<longleftrightarrow> (if p = 0 then (\<forall> q > 0. \<not> IsPeriodicFrom x g q) else p = (LEAST q ::nat. 0 < q  \<and> IsPeriodicFrom x g q))"
+    and IsPeriodicFrom_def : "\<forall> x f p. (IsPeriodicFrom x f p \<longleftrightarrow> (\<forall> (s :: nat) \<ge> x. f s = f (s + p)))"
+  shows "\<exists> g :: nat \<Rightarrow> nat.
+          (\<forall> (k :: nat) (a :: nat \<Rightarrow> nat). (k > 0 \<and> inj a) \<longrightarrow> (f (\<Sum> i=0..(k-1). 5^(a i)) = g (\<Sum> i=0..(k-1). a i)) \<and>
+         P 1 g putnam_1984_a6_solution)"
   sorry
 
 end

isabelle/putnam_1994_a1.thy

@@ -4,7 +4,7 @@ begin
 theorem putnam_1994_a1:
   fixes a :: "nat \<Rightarrow> real"
   assumes ha: "\<forall>n::nat\<ge>1. 0 < a n \<and> a n \<le> a (2*n) + a (2*n+1)"
-  shows "\<not>(\<exists>s::real. filterlim (\<lambda>N::nat. (\<Sum>n::nat=1..N. a n)) (nhds s) at_top)"
+  shows "filterlim (\<lambda>N::nat. (\<Sum>n::nat=1..N. a n)) at_top at_top"
   sorry
 
 end

isabelle/putnam_1994_b3.thy

@@ -5,10 +5,8 @@ begin
 definition putnam_1994_b3_solution :: "real set" where "putnam_1994_b3_solution \<equiv> undefined"
 (* {..<1} *)
 theorem putnam_1994_b3:
-  fixes k :: real
-  and allfexN :: bool
-  assumes hallfexN: "allfexN \<equiv> (\<forall>f::real\<Rightarrow>real. (((\<forall>x::real. f x > 0) \<and> f differentiable_on UNIV \<and> (\<forall>x::real. deriv f x > f x)) \<longrightarrow> (\<exists>N::real. \<forall>x::real>N. f x > exp (k*x))))"
-  shows "allfexN \<longleftrightarrow> k \<in> putnam_1994_b3_solution"
+  shows "{k :: real. (\<forall> f::real\<Rightarrow>real. ((\<forall> x. 0 < f x \<and> f x < deriv f x) \<and> f differentiable_on UNIV) \<longrightarrow>
+    (\<exists> N::real. \<forall> x::real>N. f x > exp (k * x)))} = putnam_1994_b3_solution"
   sorry
 
 end

isabelle/putnam_2009_b4.thy

@@ -2,6 +2,7 @@ theory putnam_2009_b4 imports Complex_Main
 "HOL-Computational_Algebra.Polynomial"
 "HOL-Analysis.Set_Integral"
 "HOL-Analysis.Lebesgue_Measure"
+"HOL-Analysis.Interval_Integral"
 begin
 
 definition putnam_2009_b4_solution :: nat where "putnam_2009_b4_solution \<equiv> undefined"
@@ -11,9 +12,9 @@ interpretation mvpolyspace: vector_space "mvpolyscale" sorry
 theorem putnam_2009_b4:
   fixes balanced :: "(real poly poly) \<Rightarrow> bool"
   and V :: "(real poly poly) set"
-  defines "balanced \<equiv> (\<lambda>P::real poly poly. (\<forall>r::real>0. (set_lebesgue_integral lebesgue (sphere 0 r) (\<lambda>x::real^2. poly (poly P (monom (x$2) 0)) (x$1))) / (2*pi*r) = 0))"
+  defines "balanced \<equiv> (\<lambda>P::real poly poly. (\<forall>r::real>0. (interval_lebesgue_integral lebesgue 0 (2*pi) (\<lambda> t. poly (poly P (monom (r * sin t) 0)) (r * cos t))) / (2*pi*r) = 0))"
   assumes hV: "\<forall>P::real poly poly. (P \<in> V \<longleftrightarrow> (balanced P \<and> degree P \<le> 2009 \<and> (\<forall>i::nat. degree (coeff P i) \<le> 2009)))"
   shows "mvpolyspace.dim V = putnam_2009_b4_solution"
   sorry
 
-end
+end

isabelle/putnam_2017_a2.thy

@@ -3,10 +3,10 @@ theory putnam_2017_a2 imports Complex_Main
 begin
 
 theorem putnam_2017_a2:
-  fixes Q :: "nat \<Rightarrow> real \<Rightarrow> real"
-  assumes hQbase: "\<forall>x::real. Q 0 x = 1 \<and> Q 1 x = x"
-  and hQn: "\<forall>n::nat>2. \<forall>x::real. Q n x = ((Q (n-1) x)^2 - 1) / Q (n-2) x"
-  shows "\<forall>n::nat>0. \<exists>P::real poly. (\<forall>i::nat. coeff P i = round (coeff P i)) \<and> Q n = poly P"
+  fixes Q :: "nat \<Rightarrow> real poly"
+  assumes hQbase: "\<forall>x::real. Q 0 = monom 1 0 \<and> Q 1 = monom 1 1"
+  and hQn: "\<forall>n::nat. Q (n + 2) * Q n = (Q (n-1))^2 - 1"
+  shows "\<forall>n::nat>0. \<exists>P::int poly. Q n = map_poly real_of_int P"
   sorry
 
-end
+end

isabelle/putnam_2021_a1.thy

@@ -5,9 +5,8 @@ definition putnam_2021_a1_solution :: nat where "putnam_2021_a1_solution \<equiv
 (* 578 *)
 theorem putnam_2021_a1:
   fixes P :: "((int \<times> int) list) \<Rightarrow> bool"
-  assumes "P \<equiv> (\<lambda>l::(int\<times>int) list. length l \<ge> 1 \<and> l!0 = (0,0) \<and> last l = (2021,2021) \<and>
-  (\<forall>n::nat\<in>{0..((length l)-2)}. sqrt ((fst (l!n) - fst (l!(n + 1)))^2 + (snd (l!n) - snd (l!(n + 1)))^2) = 5))"
-  shows "(LEAST llen::nat. (\<exists>l::(int\<times>int) list. P l \<and> llen = length l)) = putnam_2021_a1_solution"
+  assumes P_def : "\<forall> l. (P l \<longleftrightarrow> successively (\<lambda> p q. (fst p - fst q) ^ 2 + (snd p - snd q) ^ 2 = 25) l)"
+  shows "(LEAST k :: nat. \<exists> l. P ((0, 0) # l) \<and> last l = (2021, 2021) \<and> length l = k) = putnam_2021_a1_solution"
   sorry
 
 end

isabelle/putnam_2022_a1.thy

@@ -2,7 +2,7 @@ theory putnam_2022_a1 imports Complex_Main
 begin
 
 definition putnam_2022_a1_solution :: "(real \<times> real) set" where "putnam_2022_a1_solution \<equiv> undefined"
-(* {(a, b). (a = 0 \<and> b = 0) \<or> ((abs a) \<ge> 1) \<or> (0 < (abs a) \<and> (abs a) < 1 \<and> (b < (ln (1 - (1 - sqrt (1 - a^2))/a))^2 - (abs a) * (1 - sqrt (1 - a^2))/a \<or> b > (ln (1 - (1 + sqrt (1 - a^2))/a))^2 - (abs a) * (1 + sqrt (1 - a^2))/a))} *)
+(* {(a, b). (a = 0 \<and> b = 0) \<or> ((abs a) \<ge> 1) \<or> (0 < (abs a) \<and> (abs a) < 1 \<and> (b < (ln (1 + (1 - sqrt (1 - a^2))/a)^2) - (abs a) * (1 - sqrt (1 - a^2))/a \<or> b > (ln (1 + (1 + sqrt (1 - a^2))/a)^2) - (abs a) * (1 + sqrt (1 - a^2))/a))} *)
 theorem putnam_2022_a1:
   shows "{(a, b). \<exists>! x :: real. a * x + b = ln (1 + x^2)} = putnam_2022_a1_solution"
   sorry