Add new Isabelle formalization.

isabelle/putnam_2023_a6.thy

@@ -0,0 +1,23 @@
+theory Scratch imports Complex_Main
+"HOL-Number_Theory.Cong"
+begin
+
+definition putnam_2023_a6_solution :: "nat set" where
+"putnam_2023_a6_solution \<equiv> {n :: nat. 0 < n}"
+theorem putnam_2023_a6:
+  fixes IsValidGame :: "nat list \<Rightarrow> bool"
+    and parityOf :: "nat list \<Rightarrow> nat"
+    and ConformsToStrategy :: "nat list \<Rightarrow> (nat list \<Rightarrow> nat) \<Rightarrow> bool"
+    and IsWinningFor :: "nat \<Rightarrow> (nat list \<Rightarrow> nat) \<Rightarrow> bool"
+  assumes IsValidGame_def : "\<forall> g. (IsValidGame G \<longleftrightarrow> 
+       distinct g \<and> (\<forall> i \<in> set g. i \<in> {1..length g}))"
+    and parityOf_def : "\<forall> g. parityOf g = card {n :: nat. n ∈ {0..<length g} \<and> nth g n = n+1} mod 2"
+    and ConformsToStrategy_def : "\<forall> g s. (ConformsToStrategy g s \<longleftrightarrow> 
+      (\<forall> i ∈ {1..<length g}. odd i \<longrightarrow> nth g i = s (take i g)))"
+    and IsWinningFor_def : "\<forall> n s. (IsWinningFor n s \<longleftrightarrow>
+          (\<exists> p. \<forall> g. length g = n \<longrightarrow> IsValidGame g 
+           \<longrightarrow> ConformsToStrategy g s \<longrightarrow> parityOf g = p))"
+  shows "{n :: nat. 0 < n \<and> (\<exists> s. IsWinningFor n s)} = putnam_2023_a6_solution"
+  sorry
+
+end