Upload folder using huggingface_hub

Browse files

Files changed (13) hide show

.gitattributes +9 -0
RL/RL_train.json +3 -0
RL/miniF2F_valid.json +1 -0
SFT/train.json +3 -0
SFT/val.json +3 -0
SFT_noinvoke/train.json +3 -0
SFT_noinvoke/val.json +3 -0
holdout.json +1 -0
tests/afp_2022_test.json +3 -0
tests/afp_2023_test.json +3 -0
tests/unformatted_miniF2F_raw.json +0 -0
tests_noinvoke/afp_2022_test.json +3 -0
tests_noinvoke/afp_2022_val.json +3 -0

.gitattributes CHANGED Viewed

@@ -33,3 +33,12 @@ saved_model/**/* filter=lfs diff=lfs merge=lfs -text
 *.zip filter=lfs diff=lfs merge=lfs -text
 *.zst filter=lfs diff=lfs merge=lfs -text
 *tfevents* filter=lfs diff=lfs merge=lfs -text

 *.zip filter=lfs diff=lfs merge=lfs -text
 *.zst filter=lfs diff=lfs merge=lfs -text
 *tfevents* filter=lfs diff=lfs merge=lfs -text
+RL/RL_train.json filter=lfs diff=lfs merge=lfs -text
+SFT/train.json filter=lfs diff=lfs merge=lfs -text
+SFT/val.json filter=lfs diff=lfs merge=lfs -text
+SFT_noinvoke/train.json filter=lfs diff=lfs merge=lfs -text
+SFT_noinvoke/val.json filter=lfs diff=lfs merge=lfs -text
+tests/afp_2022_test.json filter=lfs diff=lfs merge=lfs -text
+tests/afp_2023_test.json filter=lfs diff=lfs merge=lfs -text
+tests_noinvoke/afp_2022_test.json filter=lfs diff=lfs merge=lfs -text
+tests_noinvoke/afp_2022_val.json filter=lfs diff=lfs merge=lfs -text

RL/RL_train.json ADDED Viewed

	@@ -0,0 +1,3 @@

+version https://git-lfs.github.com/spec/v1
+oid sha256:66f56f975dbcdc76bde24b21c6c8c43a90e8ea22376f465a658df834d2b9beaf
+size 999611353

RL/miniF2F_valid.json ADDED Viewed

	@@ -0,0 +1 @@

+ [["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_binomnegdiscrineq_10alt28asqp1:\n fixes a :: real\n shows \"10 * a \\<le> 28 * a^2 + 1\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12_2000_p15:\n fixes f :: \"complex \\<Rightarrow> complex\"\n assumes asm:\"\\<forall> x. f (x / 3) = x^2 + x + 1\"\n shows \"(\\<Sum>y\\<in>f -` {7}. y / 3) = - 1 / 9\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2008_p2:\n fixes x :: real\n assumes h0 : \"x * (1 / 2 + 2 / 3) = 1\"\n shows \"x = 6/7\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2003_p24:\n fixes a b::real\n assumes \"b\\<le>a\"\n and \"1<b\"\n shows \"ln (a/b) / ln a + ln (b/a) / ln b \\<le>0\" (is \"?L \\<le> _\")"], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_132:\n fixes x :: real\n and f g :: \"real \\<Rightarrow> real\"\n assumes h0 : \"\\<And>x. f x = x + 2\"\n and h1 : \"\\<And>x. g x = x^2\"\n and h2 : \"f (g x) = g (f x)\"\n shows \"x = -1/2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_64 :\n \"(LEAST x ::nat. [30 * x = 42] (mod 47)) = 39\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_155:\n \"card ({x::nat. x mod 19 = 7 \\<and> 100\\<le>x \\<and> x < 1000}) = 48\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_51:\n fixes a b ::real\n assumes \"0 < a \\<and> 0 < b\"\n and \"a + b = 35\"\n and \"a = (2/5) * b\"\n shows \"b - a = 15\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_149:\n fixes f :: \"real \\<Rightarrow> real\"\n assumes \"\\<forall> x < -5. f x = x^2 + 5\"\n and \"\\<forall> x \\<ge> -5. f x = 3 * x -8\"\n shows \"(\\<Sum> k \\<in> (f -` {10}). k) = 6\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_709:\n fixes n :: nat\n assumes \"n>0\" \n and \"card ({k. k dvd (2*n)}) = 28\"\n and \"card ({k. k dvd (3*n)}) = 30\" \n shows \"card ({k. k dvd (6*n)}) = 35\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem induction_sum_odd:\n fixes n :: nat\n assumes \"n > 0\"\n shows \"(\\<Sum>(k::nat) = 0..(n-1). 2 * k + 1) = n^2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2019_p9:\n fixes a :: \"nat \\<Rightarrow> rat\"\n assumes \"a 1 = 1\"\n and \"a 2 = 3 / 7\"\n and \"\\<forall> n. a (n + 2) = (a n * a (n + 1)) / (2 * a n - a (n + 1))\" \n shows \"fst (quotient_of (a 2019)) + snd (quotient_of (a 2019)) = 8078\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_89:\n fixes b :: real\n assumes h0 : \"b\\<noteq>0\"\n shows \"(7 * b^3)^2 * 1/((4 * b^2)^3) = 49 / 64\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_140:\n fixes a b c :: real\n assumes h0 : \"0 < a \\<and> 0 0 < c\"\n and h1 : \"\\<forall>x. 24 * x^2 - 19 * x - 35 = ((a*x-5) * (2 * (b*x) + c))\"\n shows \"a * b - 3 * c = -9\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_405:\n fixes x :: nat\n assumes h0 : \"0 < x\"\n and h1 : \"x ^ 2 + 4 * x + 4 < 20\"\n shows \"x = 1 \\<or> x = 2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12b_2002_p3:\n fixes n ::nat\n assumes \"n>0\"\n and prime:\"prime (n^2+2-3*n)\"\n shows \"n=3\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_326:\n fixes n :: nat\n assumes \"(n - 1) * n * (n + 1) = 720\" \n shows \"(n + 1) = 10\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_169:\n \"gcd (fact 20) 200000 = (40000::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_11:\n fixes a b :: real\n assumes h0 : \"a \\<noteq> b\"\n and h1 : \"a \\<noteq> 2 * b\"\n and h2 : \"(4*a+3*b) / (a-2*b) = 5\"\n shows \"(a+11*b) / (a-b) = 2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_109:\n fixes a b :: real\n assumes h0 : \"3*a+2*b=12\"\n and h1 : \"a=4\"\n shows \"b=0\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_202:\n \"(19^19 + 99^99) mod 10 = (8::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_568:\n fixes a :: real\n shows \"(a-1) * (a+1) * (a+2) - (a-2) * (a+1) = a^3 + a^2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem induction_divisibility_9div10tonm1:\n fixes n::nat\n shows \"(9::nat) dvd 10^n - 1\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_437:\n fixes x y :: real\n and n :: int\n assumes \"x^3 = -45\"\n and \"y^3 = -101\"\n and \"x < n\"\n and \"n < y\" \n shows \"n = -4\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem induction_seq_mul2pnp1:\n fixes n :: nat\n and u :: \"nat \\<Rightarrow> nat\"\n assumes h0 : \"u 0 = 0\"\n and h1 : \"\\<And>(n::nat). u (n+1) = 2 * u n + (n+1)\"\n shows \"u n = 2 ^ (n+1) - (n+2)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_24:\n \"(\\<Sum> k \\<in>{1..<10}. 11^k) mod 100 = (59::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_493:\n fixes f :: \"real \\<Rightarrow> real\"\n assumes h0 : \"\\<And>x. f x = x^2 - 4 * (sqrt x) + 1\"\n shows \"f (f 4) = 70\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12_2000_p5:\n fixes x p ::real\n assumes \"x<2\"\n and \"\\<bar>x -2\\<bar> = p\"\n shows \"x - p = 2 - 2 * p\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_manipexpr_2erprsqpesqeqnrpnesq:\n fixes e r :: complex\n shows \"2 * (e * r) + (e^2 + r^2) = (-r + (-e))^2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1964_p1_1:\n fixes n :: nat\n assumes \"7 dvd (2^n-1)\"\n shows \"3 dvd n\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2019_p21:\n fixes z::complex\n assumes h0: \"z = (Complex (1/sqrt 2) (1/sqrt 2))\"\n shows \"(\\<Sum>k::nat=1..12. (z^(k^2))) * (\\<Sum> k::nat=1..12. 1/(z^(k^2))) =36\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_482:\n fixes m n :: nat\n and k :: real\n and f :: \"real \\<Rightarrow> real\"\n assumes h0 : \"prime m\"\n and h1 : \"prime n\"\n and h2 : \"m \\<noteq> n\"\n and h3 : \"\\<And>x. f x = x^2 - 12*x + k\"\n and h4 : \"f m = 0\"\n and h5 : \"f n = 0\"\n shows \"k = 35\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_116:\n fixes k x :: real\n assumes h0 : \"x = (13 - sqrt 131) / 4\"\n and h1 : \"2 * x^2 - 13 * x + k = 0\"\n shows \"k = 19/4\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_206:\n fixes a b :: real\n and f :: \"real \\<Rightarrow> real\"\n assumes h0 : \"\\<And>x. f x = x^2 + a*x + b\"\n and h1 : \"2 * a \\<noteq> b\"\n and h2 : \"f (2 * a) = 0\"\n and h3 : \"f b = 0\"\n shows \"a + b = -1\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12b_2003_p9:\n fixes a b ::real and f :: \"real \\<Rightarrow> real\"\n assumes \"\\<forall> x. f x = a * x + b\"\n and \" f 6 - f 2 = 12\"\n shows \"f 12 - f 2 = 30\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem induction_divisibility_3div2tooddnp1:\n fixes n ::nat\n shows \"(3::nat) dvd (2^(2 * n + 1) + 1)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1961_p1:\n fixes x y z a b :: real\n assumes h0 : \"0 < x \\<and> 0 < y \\<and> 0 < z\"\n and h1 : \"x \\<noteq> y\"\n and h2 : \"y \\<noteq> z\"\n and h3 : \"z \\<noteq> x\"\n and h4 : \"x + y + z = a\"\n and h5 : \"x^2 + y^2 + z^2 = b^2\"\n and h6 : \"x * y = z^2\"\n shows \"0<a \\<and> b^2 < a^2 \\<and> a^2 < 3*b^2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_amgm_faxinrrp2msqrt2geq2mxm1div2x:\n \"\\<And>x. (x>0) \\<Longrightarrow> 2 - sqrt 2 \\<ge> 2 - x - 1/ (2 * x)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_amgm_sumasqdivbsqgeqsumbdiva:\n fixes a b c :: real\n assumes h0 : \"0 < a \\<and> 0 0 < c\"\n shows \"a^2 / b^2 + b^2 / c^2 + c^2 / a^2 \\<ge> b / a + c / b + a / c\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_35:\n fixes k :: nat\n assumes \"k^2 = 196\"\n shows \"(\\<Sum> k \\<in> { n ::nat. n dvd k}. k) = (24::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1966_p4:\n fixes n :: nat\n and x :: real\n assumes h0 : \"\\<And>(k::nat). \\<And>(m::int). k\\<noteq>0 \\<Longrightarrow> x \\<noteq> m * pi / (2^k)\"\n and h1 : \"0 < n\"\n shows \"(\\<Sum>(k::nat) =1..n.(1 / sin ((2^k) * x))) = 1 / tan x - 1 / tan ((2^n) * x)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_780:\n fixes m x :: nat\n assumes h0 : \"10 \\<le> m\"\n and h1 : \"m \\<le> 99\"\n and h2 : \"(6 * x) mod m = 1\"\n and h3 : \"(x - 6^2) mod m = 0\"\n shows \"m = 43\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_32:\n \"(\\<Sum> k \\<in> { n ::nat. n dvd 36}. k) = 91\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem induction_sum_1oktkp1:\n fixes n :: nat\n shows \"n=0 \\<or> (\\<Sum>(k::nat) = 0..(n-1). (1::real)/((k+1)*(k+2))) = n / (n+1)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_421:\n fixes a b c d :: real\n assumes h0 : \"b = a^2 + 4 * a + 6\"\n and h1 : \"b = 1 / 2 * a^2 + a + 6\"\n and h2 : \"d = c^2 + 4 * c + 6\"\n and h3 : \"d = 1 / 2 * c^2 + c + 6\"\n and h4 : \"a < c\"\n shows \"c-a=6\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_151:\n shows \"ceiling (sqrt 27) - floor (sqrt 26) = 1\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2009_p15:\n fixes n :: nat\n assumes \"0 < n\"\n and \"(\\<Sum> k \\<in> {1..<n+1}. (k * (\\^k))) = 48 + 49 * \\\" \n shows \"n = 97\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_35:\n fixes p q :: \"real \\<Rightarrow> real\"\n assumes h0 : \"\\<And>x. p x = 2 - x^2\"\n and h1 : \"\\<And>x. (x\\<noteq>0) \\<Longrightarrow> q x = 6 / x\"\n shows \"p (q 2) = -7\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2021_p7:\n fixes x y ::real\n shows \"1 \\<le> ((x * y) - 1)^2 + (x + y)^2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_221:\n \"card {x ::nat. 0 < x \\<and> x < 1000 \\<and> card ({n. n dvd x}) = 3} = 11\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_640:\n \"(91145+91146+91147+91148) mod 4 = (2::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_136:\n fixes n ::nat\n assumes \"123 * n + 17 = 39500\"\n shows \"n = 321\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_xmysqpymzsqpzmxsqeqxyz_xpypzp6dvdx3y3z3:\n fixes x y z :: int\n assumes h0 : \"(x-y)^2 + (y-z)^2 + (z-x)^2 = x * y * z\"\n shows \"(x + y + z + 6) dvd (x^3 + y^3 + z^3)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1974_p5:\n fixes a b c d s :: real\n assumes \"a>0\" \"b>0\" \"c>0\" \"d>0\"\n assumes h0 : \"s=a/(a+b+d) + b/(a+b+c) + c/(b+c+d) + d/(a+c+d)\"\n shows \"1<s \\<and> s<2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_96:\n fixes x y z a ::real\n assumes \"x>0\" \"y>0\" \"z>0\" \n and \"ln x - ln y = a\"\n and \"ln y - ln z = 15\"\n and \"ln z - ln x=-7\"\n shows \"a = -8\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem induction_ineq_nsqlefactn:\n fixes n::nat\n assumes \" 4 \\<le> n\"\n shows \"n^2 \\<le> fact n\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1987_p4:\n fixes f :: \"nat \\<Rightarrow> nat\"\n shows \"\\<exists>(n::nat). f (f n) \\<noteq> n + 1987\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_123:\n fixes a b :: nat\n assumes h0 : \"a + b = 20\"\n and h1 : \"a = 3 * b\"\n shows \"a - b = 10\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_234:\n fixes d :: real\n assumes h0 : \"27/125 * d = 9/25\"\n shows \"3/5 * d^3 = 25/9\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_370:\n fixes n :: nat\n assumes h0 : \"n mod 7 = (3::nat)\"\n shows \"(2*n+1) mod 7 = (0::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_2varlineareq_xpeeq7_2xpeeq3_eeq11_xeqn4:\n fixes x e :: complex\n assumes h0 : \"x + e = 7\"\n and h1 : \"2 * x + e = 3\"\n shows \"e=11 \\<and> x= (-4)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_81:\n \"71 mod 3 = (2::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_101:\n fixes x :: real\n assumes h0 : \"x^2 - 5 * x - 4 \\<le> 10\"\n shows \"x\\<ge> -2 \\<and> x \\<le> 7\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_458:\n fixes n :: nat\n assumes h0 : \"n mod 8 = (7::nat)\"\n shows \"n mod 4 = 3\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2017_p2:\n fixes x y :: real\n assumes h0 : \"x \\<noteq> 0\"\n and h1 : \"y \\<noteq> 0\"\n and h2 : \"x + y = 4 * (x * y)\"\n shows \"1/x + 1/y = 4\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem numbertheory_sqmod4in01d:\n fixes a :: int\n shows \"(a^2 mod 4 = 0) \\<or> (a^2 mod 4 = 1)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1993_p5:\n \"\\<exists> f :: nat \\<Rightarrow> nat. \n (\\<forall> a b. (a < b) \\<longleftrightarrow> f a < f b) \n \\<and> f 1 = 2 \\<and> (\\<forall> n. f (f n) = f n + n)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_22:\n fixes b :: nat\n assumes h0 : \"b < 10\"\n and h1 : \"\\<exists>a. (10*b+6) = a^2\"\n shows \"b=3 \\<or> b =1\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem aimeII_2020_p6:\n fixes t :: \"nat \\<Rightarrow> rat\"\n assumes \"t 1 = 20\"\n and \"t 2 = 21\"\n and \"\\<forall> n \\<ge> 3. t n = (5 * t (n - 1) + 1) / (25 * t (n - 2))\" \n shows \"let (a,b) = quotient_of (t 2020) in a +b = 626\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_10:\n \"abs ((120::real) / 100 * 30 - 130 / 100 * 20) = 10\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_190:\n \"((3::real) / 8 + 7 / 8) / (4 / 5) = 25 / 16\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_59:\n fixes b :: real\n assumes \"4 powr b + 2^3 = 12\"\n shows \"b=1\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12b_2003_p17:\n fixes x y ::real\n assumes \"x>0\" \"y>0\"\n and \"ln (x * y^3) =1\"\n and \"ln (x^2 * y) = 1\"\n shows \"ln (x*y) = 3/5\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_apb4leq8ta4pb4:\n fixes a b :: real\n assumes h0 : \"0 < a \\<and> 0 < b\"\n shows \"(a+b)^4 \\<le> 8 * (a^4 + b^4)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_236:\n \"(1999^2000) mod 5 = (1::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_126:\n fixes x :: nat\n assumes \"x>0\"\n shows \"(LEAST a. gcd a 40 = x + 3 \\<and> lcm a 40 = x * (x + 3)) = 8\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_22:\n \"(log 2 (5^4)) / (log 2 (5^2)) = 2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2008_p15:\n fixes k :: nat\n assumes h0 : \"k = 2008^2 + 2^2008\"\n shows \"(k^2 + 2^k) mod 10 = 6\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_sqineq_36azm9asqle36zsq:\n fixes z a :: real\n shows \"36 * (a * z) - 9 * a^2 \\<le> 36 * z^2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem numbertheory_prmdvsneqnsqmodpeq0:\n fixes n :: int\n and p :: nat\n assumes \"prime p\" \n shows \"p dvd n \\<longleftrightarrow> (n^2) mod p = 0\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_251:\n fixes x :: real\n assumes h0: \"x \\<noteq> 0\"\n and h1: \"3 + 1/x = 7/x\"\n shows \"x = 2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem induction_divisibility_3divnto3m2n:\n fixes n::nat\n shows \"3 dvd n^3 + 2 * n\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_amgm_prod1toneq1_sum1tongeqn:\n fixes a :: \"nat \\<Rightarrow> real\"\n and n :: nat\n assumes \"\\<forall>i. a i \\<ge>0\"\n and \"prod a {..<n} = 1\" \n shows \"sum a {..<n} \\<ge> n\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2008_p4:\n \"(\\<Prod>k::nat=1..501. ((4::real) * k + 4) / (4 * k)) = 502\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_2rootspoly_apatapbeq2asqp2ab:\n fixes a b :: complex\n shows \"(a+a) * (a+b) = 2 * a^2 + 2 * (a*b)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2002_p1:\n fixes f::\"complex \\<Rightarrow> complex\"\n assumes \"\\<forall> x. f x = (2 * x + 3) * (x - 4) + (2 * x + 3) * (x - 6)\"\n shows \"(\\<Sum> y \\<in> f -` {0}. y) = 7/2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2003_p25:\n fixes a b::real and f ::\"real \\<Rightarrow> real\"\n assumes \"b>0\" \n and \"\\<forall> x. f x = sqrt (a * x^2 + b * x)\"\n and \"{x. 0 \\<le> f x} = f ` {x. 0 \\<le> f x}\"\n shows \"a=0 \\<or> a = -4\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_224:\n \"card { n :: nat. sqrt n < 7 / 2 \\<and> 2 < sqrt n} = 8\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_284:\n fixes a b :: nat\n assumes h0 : \"1\\<le>a \\<and> a \\<le>9 \\<and> b \\<le>9\"\n and h1 : \"10 * a + b = 2 * (a+b)\"\n shows \"10 * a + b = 18\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem numbertheory_sqmod3in01d:\n fixes a :: int\n shows \"a^2 mod 3 = 0 \\<or> a^2 mod 3 = 1\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1962_p4:\n fixes x :: real\n assumes h0 : \"(cos x)^2 + (cos (2 * x))^2 + (cos (3 * x))^2 = 1\"\n shows \"(\\<exists>(m::int). x = pi/2 + m * pi) \\<or>\n (\\<exists>(m::int). x = pi/4 + m * pi/2) \\<or> \n (\\<exists>(m::int). x = pi/6 + m * pi/6) \\<or> \n (\\<exists>(m::int). x = 5*pi/6 + m * pi/6) \n \""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_252:\n \"(fact 7) mod 23 = (3::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_159:\n fixes b :: real\n and f :: \"real \\<Rightarrow> real\"\n assumes h0 : \"\\<And>x. f x = 3 * x^4 - 7 * x^3 + 2*x^2 - b*x +1\"\n and h1 : \"f 1 = 1\"\n shows \"b = -2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1965_p1:\n fixes x :: real\n assumes \"0 \\<le> x\"\n and \"x \\<le> 2 * pi\"\n and \"2 * cos x \\<le> abs (sqrt (1 + sin (2 * x)) \n - sqrt (1 - sin (2 * x)))\"\n and \"abs (sqrt (1 + sin (2 * x)) - sqrt (1 - sin (2 * x))) \\<le> sqrt 2\" \n shows \"pi / 4 \\<le> x \\<and> x \\<le> 7 * pi / 4\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_690 :\n \"(LEAST a ::nat. [a = 2] (mod 3) \\<and> [a = 4] (mod 5) \n \\<and> [a = 6] (mod 7) \\<and> [a = 8] (mod 9)) = 314\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2009_p9:\n fixes a b c::real\n and f::\"real \\<Rightarrow> real\"\n assumes h0:\"\\<forall> x. f (x+3) = 3 * x^2 + 7*x + 4\"\n and h1:\"\\<forall> x. f x = a * x^2 + b * x + c\"\n shows \"a+b+c=2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_536:\n \"fact 3 * (2^3 + sqrt 9) / 2 = 33\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_3rootspoly_amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta:\n fixes a b c d :: complex\n shows \"(a-d) * (a-c) * (a-b) = -(((a^2 - (b+c) * a) + c * b) * d) + (a^2 - (b+c) * a + c * b) * a\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem aime_1988_p3:\n fixes x :: real\n assumes h0 : \"0 < x\"\n and h1 : \"log 2 (log 8 x) = log 8 (log 2 x)\"\n shows \"(log 2 x)^2 = 27\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12b_2002_p11:\n fixes a b::nat\n assumes \"prime a\" and \"prime b\"\n and \"prime (a+b)\" and \"prime (a-b)\"\n shows \"prime (a + b + (a - b + (a + b)))\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_48:\n fixes q e :: complex\n assumes h0 : \"q = Complex 9 (-4)\"\n and h1 : \"e = Complex (-3) (-4)\"\n shows \"q - e = 12\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_181:\n fixes n :: real\n assumes h0 : \"n \\<noteq> 3\"\n and h1 : \"(n+5) / (n-3) = 2\"\n shows \"n=11\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_247:\n fixes t s :: real\n and n :: nat\n assumes h0 : \"t = 2 * s - s^2\"\n and h1 : \"s = n^2 - 2^n + 1\"\n and h2 : \"n=3\"\n shows \"t=0\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem aime_1988_p4:\n fixes n :: nat\n and a :: \"nat \\<Rightarrow> real\"\n assumes h0 : \"\\<And>n. abs (a n) < 1\"\n and h1 : \"(\\<Sum>(k::nat) = 0..(n-1). (abs (a k))) = 19 + abs(\\<Sum>(k::nat) = 0..(n-1). (a k))\"\n shows \"20 \\<le> n\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_303:\n \"(\\<Sum> k \\<in> {n ::nat. 2 \\<le> n \\<and> [171 = 80] (mod n) \\<and> [468 = 13] (mod n)}. k) = 111\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12_2001_p9:\n fixes f:: \"real \\<Rightarrow> real\"\n assumes f_times:\"\\<forall> x > 0. \\<forall> y > 0. f (x * y) = f x / y\"\n and \"f 500 = 3\"\n shows \"f 600 = 5 / 2 \""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_33:\n fixes n :: nat\n assumes h0 : \"n < 398\"\n and h1 : \"(n * 7) mod 398 = 1\"\n shows \"n=57\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_119:\n fixes d e :: real\n assumes h0 : \"2 * d = 17 * e - 8\"\n and h1 : \"2 * e = d - 9\"\n shows \"e = 2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem numbertheory_sumkmulnckeqnmul2pownm1:\n fixes n k :: nat\n assumes h0 : \"0<n \\<and> 0<k\"\n and h1 : \"k\\<le>n\"\n shows \"n choose k = ((n-1) choose k) + ((n-1) choose (k-1))\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12b_2003_p6:\n fixes a r::real and u::\"nat \\<Rightarrow> real\"\n assumes \"\\<forall> k. u k = a * r^k\"\n and \"u 1= 2\"\n and \"u 3=6\"\n shows \"u 0 = 2/ sqrt 3 \\<or> u 0 = - 2/sqrt 3\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_102:\n \"(2^8) mod 5 = (1::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_48:\n fixes b :: nat\n assumes h0 : \"0<b\"\n and h1 : \"3 * b^2 + 2 * b + 1 = 57\"\n shows \"b=4\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_269:\n \"(2005^2 + 2005^0 + 2005^0 + 2005^5) mod 100 = (52::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1966_p5:\n fixes x a :: \"nat \\<Rightarrow> real\"\n assumes \"a 1 > a 2\" and \"a 2 > a 3\" and \"a 3 > a 4\"\n assumes \n h6 : \"abs (a 1 - a 2) * x 2 + abs (a 1 - a 3) * x 3 + abs (a 1 - a 4) * x 4 = 1\"\n and h7 : \"abs (a 2 - a 1) * x 1 + abs (a 2 - a 3) * x 3 + abs (a 2 - a 4) * x 4 = 1\"\n and h8 : \"abs (a 3 - a 1) * x 1 + abs (a 3 - a 2) * x 2 + abs (a 3 - a 4) * x 4 = 1\"\n and h9 : \"abs (a 4 - a 1) * x 1 + abs (a 4 - a 2) * x 2 + abs (a 4 - a 3) * x 3 = 1\"\n shows \"x 2 = 0 \\<and> x 3 = 0 \\<and> x 1 = 1 / abs (a 1 - a 4) \\<and> x 4 = 1 / abs (a 1 - a 4)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_2complexrootspoly_xsqp49eqxp7itxpn7i:\n fixes x :: complex\n shows \"x^2 + 49 = (x + 7 * \\) * (x - 7 * \\)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12b_2004_p3:\n fixes x y :: nat\n assumes \"2^x * 3^y = 1296\"\n shows \"x + y = 8\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_110:\n fixes q e :: complex\n assumes h0 : \"q = Complex 2 (-2)\"\n and h1 : \"e = Complex 5 5\"\n shows \"q * e = 20\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_455:\n fixes x :: real\n assumes h0 : \"2 * (2 * (2 * (2 * x))) = 48\"\n shows \"x=3\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_323:\n fixes \\<sigma>:: \"real \\<Rightarrow> real\"\n assumes \"bij \\<sigma>\"\n and \"\\<forall> x. \\<sigma> x = x^3 - 8\" \n shows \"Hilbert_Choice.inv \\<sigma> (\\<sigma> (Hilbert_Choice.inv \\<sigma> 19)) = 3\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_73:\n fixes p q r x :: complex\n assumes h0 : \"(x-p) * (x-q) = (r-p) * (r-q)\"\n and h1 : \"x \\<noteq> r\"\n shows \"x = p + q -r\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_126:\n fixes x y :: real\n assumes h0 : \"2 * 3 = x - 9\"\n and h1 : \"2 * (-5) = y + 1\"\n shows \"x=15 \\<and> y = -11\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_547:\n fixes x y :: real\n assumes \"x=5\"\n and \"y=2\"\n shows \"sqrt (x^3 - y^2) = 11\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_403:\n \"(\\<Sum> k \\<in> ({n. n dvd 198 \\<and> n\\<noteq> 198}). k) = (270::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1987_p6:\n fixes p :: nat\n and f :: \"nat \\<Rightarrow> nat\"\n assumes h0 : \"\\<And>x. f x = x^2 + x + p\"\n and h1 : \"\\<And>(k::nat). (k\\<le>floor(sqrt (p/3))) \\<Longrightarrow> prime (f k)\"\n shows \"\\<And>i. (i \\<le> p - 2) \\<Longrightarrow> prime (f i)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2003_p1:\n fixes u v :: \"nat \\<Rightarrow> nat\"\n assumes u:\"\\<forall>n. u n = 2 *n\"\n and v:\"\\<forall>n. v n= 2* n -1\"\n shows \"(\\<Sum> k \\<in>{1..2003}. u k) - (\\<Sum> k \\<in>{1..2003}. v k) = 2003\"\n (is \"?L = ?R\")"], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_2006_p3:\n fixes a b c ::real\n shows \"(a * b * (a^2 - b^2)) + (b * c * (b^2 - c^2)) + \n (c * a * (c^2 - a^2)) \\<le> (9 * sqrt 2) / 32 * (a^2 + b^2 + c^2)^2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_182:\n fixes y:: complex\n shows \"7*(3*y+2) = 21 * y + 14\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_37:\n fixes x y :: real\n assumes h0 : \"x+y=7\"\n and h1 : \"3 * x + y = 45\"\n shows \"x^2 - y^2 = 217\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem aimeI_2000_p7:\n fixes x y z :: real\n and m :: rat\n assumes \"0 < x \\<and> 0 < y \\<and> 0 < z\"\n and \"x * y * z = 1\"\n and \"x + 1 / z = 5\"\n and \"y + 1 / x = 29\"\n and \"z + 1 / y = m\"\n and \"0 < m\" \n shows \"let (x,y) = quotient_of m in x + y = 5\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_amgm_sqrtxymulxmyeqxpy_xpygeq4:\n fixes x y :: real\n assumes h0 : \"0 < x \\<and> 0 < y\"\n and h1 : \"y \\<le> x\"\n and h2 : \"sqrt (x * y) * (x - y) = (x + y)\"\n shows \"x + y \\<ge> 4\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_185:\n fixes f :: \"int \\<Rightarrow> int\"\n assumes h0 : \"\\<And>x. (f x = abs (x+4))\"\n shows \"card {(x::int). (f x < 9)} = 17\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2011_p18:\n fixes x y :: real\n assumes h0 : \"abs (x+y) + abs (x-y) = 2\"\n shows \"x^2 - 6 * x + y^2 \\<le> 8\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_101:\n \"(17 * 18) mod 4 = (2::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2009_p25:\n fixes a :: \"nat \\<Rightarrow> real\"\n assumes h0 : \"a 1 = 1\"\n and h1 : \"a 2 = 1 / (sqrt 3)\"\n and h2 : \"\\<And>n. a (n+2) = (a n + a (n+1)) / (1 - (a n) * (a (n+1)))\"\n shows \"abs (a 2009) = 0\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_37:\n \"lcm 9999 100001 = (90900909::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2016_p2:\n fixes x :: nat\n assumes h0 : \"10^x * 100^(2*x) = 1000^5\"\n shows \"x=3\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_30:\n \"(33818^2 + 33819^2 + 33820^2 + 33821^2 + 33822^2) mod 17 = (0::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_335:\n fixes n :: nat\n assumes h0 : \"n mod 7 = 5\"\n shows \"(5 * n) mod 7 = 4\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_211 :\n \"card {n::nat. n<60 \\<and> 6 dvd (4 * n - 2)} = 20\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_509:\n \"sqrt ((5 / sqrt 80 + sqrt 845 / 9 + sqrt 45) / sqrt 5) = 13 / 6\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_451:\n fixes \\<sigma>:: \"real \\<Rightarrow> real\"\n assumes \"bij \\<sigma>\"\n and \"Hilbert_Choice.inv \\<sigma> (-15) = 0\"\n and \"Hilbert_Choice.inv \\<sigma> 0 = 3\"\n and \"Hilbert_Choice.inv \\<sigma> 3 = 9\"\n and \"Hilbert_Choice.inv \\<sigma> 9 = 20\" \n shows \"\\<sigma> (\\<sigma> 9) = 0\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_480:\n fixes f :: \"real \\<Rightarrow> real\"\n assumes h0 : \"\\<And>x. x<0 \\<Longrightarrow> f x = -(x^2)-1\"\n and h1 : \"\\<And>x. (0 \\<le> x \\<and> x < 4) \\<Longrightarrow> f x = 2\"\n and h2 : \"\\<And>x. x\\<ge>4 \\<Longrightarrow> f x = sqrt x\"\n shows \"f pi = 2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_327:\n fixes a :: real\n assumes h0 : \"1 / 5 * abs(9 + 2 * a) < 1\"\n shows \"-7 < a \\<and> a < -2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_42:\n fixes u v :: nat\n assumes \"27 * u mod 40 = 17\"\n and \"27 * v mod 40 = 17\"\n and \"u < 40\"\n and \"v < 80\"\n and \"40 < v\" \n shows \"(u + v) = 62\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1984_p2:\n fixes a b :: nat\n assumes h0 : \"0 < a \\<and> 0 < b\"\n and h1 : \"\\<not> (7 dvd a)\"\n and h2 : \"\\<not> (7 dvd b)\"\n and h3 : \"\\<not> (7 dvd (a+b))\"\n and h4 : \"(7^7) dvd ((a+b)^7 - a^7 - b^7)\"\n shows \"19 \\<le> a + b\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_45 :\n \"(gcd 6432 132) + 11 = (23::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2002_p12:\n fixes f :: \"real => real\"\n and k :: real and a b::nat\n assumes \"\\<forall> x. f x = x^2 - 63 * x + k\"\n and \"f -` {0} = {of_nat a, of_nat b}\"\n and \"prime a\" and \"prime b\"\n shows \"k=122\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_sqineq_2at2pclta2c2p41pc:\n fixes a c :: real\n shows \"2 * a * (2+c) \\<le> a^2 + c^2 + 4 * (1+c)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_77:\n fixes a b :: real\n and f :: \"real \\<Rightarrow> real\"\n assumes h0 : \"a \\<noteq> 0 \\<and> b \\<noteq> 0 \\<and> a \\<noteq> b\"\n and h1 : \"\\<And>x. f x = x^2 + a*x + b\"\n and h2 : \"f a = 0\"\n and h3 : \"f b = 0\"\n shows \"a=1 \\<and> b = -2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem numbertheory_xsqpysqintdenomeq:\n fixes x y :: rat\n assumes \"snd (quotient_of (x^2 + y^2)) = 1\"\n shows \"snd (quotient_of x) = snd (quotient_of y)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_668:\n fixes l r::int and a b::int\n assumes \"0\\<le>l\" \"l<7\" \"0\\<le>r\" \"r<7\"\n and \"[l * (2 + 3) = 1] (mod 7)\" \n and \"0\\<le>a \\<and> a<7 \\<and> [a*2=1] (mod 7)\"\n and \"0\\<le>b \\<and> b<7 \\<and> [b*3=1] (mod 7)\"\n and \"r = (a+b) mod 7\"\n shows \"l - r = 1\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem aime_1996_p5:\n fixes a b c r s t :: real\n and f g :: \"real \\<Rightarrow> real\"\n assumes h0 : \"\\<And>x. f x = x^3 + 3 * x^2 + 4*x -11\"\n and h1 : \"\\<And>x. g x = x^3 + r * x^2 + s*x + t\"\n and h2 : \"f a = 0\"\n and h3 : \"f b = 0\"\n and h4 : \"f c = 0\"\n and h5 : \"g (a+b) = 0\"\n and h6 : \"g (b+c) = 0\"\n and h7 : \"g (c+a) = 0\"\n and h8 : \"a \\<noteq> b\"\n and h9 : \"a \\<noteq> c\"\n and h10 : \"b \\<noteq> c\"\n shows \"t=23\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12b_2020_p5:\n fixes a b :: nat\n assumes \"(5::real) / 8 * b - 2 / 3 * a = 7\"\n and \"of_nat b - (5::real) / 8 * b - (a - 2 / 3 * a) = 7\"\n shows \"a = 42\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2010_p22:\n fixes x ::real \n shows \"49 \\<le> (\\<Sum> k \\<in> {1..<120}. abs (k * x - 1))\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1988_p6:\n fixes a b :: nat\n assumes h0 : \"0<a \\<and> 0<b\"\n and h1 : \"(a*b+1) dvd (a^2 + b^2)\"\n shows \"\\<exists>(x::nat). ((x^2) = (a^2+b^2)/(a*b+1))\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_739:\n \"(fact 9) mod 10 = (0::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_200:\n \"139 mod 11 = (7::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_13:\n fixes a b :: real\n assumes h0: \"\\<forall>(x::real). (x-3 \\<noteq> 0 \\<and> x - 5 \\<noteq> 0) \\<Longrightarrow> \n 4 * x / (x^2 - 8 * x + 15) = a / (x-3) + b / (x-5)\"\n shows \"a = -6 \\<and> b = 10\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2020_p13:\n fixes a b c::nat\n assumes \"1 < a \\<and> 1 1 < c\"\n and \"\\<forall>n>1. (n * ((n * (n powr (1 / c))) powr (1 / b))) powr (1 / a) = (n^25) powr (1 / 36)\"\n shows \"b=3\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_110:\n fixes a b :: nat\n assumes h0 : \"0 < a \\<and> 0 b \\<le> a\"\n and h1 : \"(a+b) mod 10 = 2\"\n and h2 : \"(2*a + b) mod 10 = 1\"\n shows \"(a-b) mod 10 = 6\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12b_2002_p6:\n fixes a b :: real\n assumes \"a \\<noteq> 0 \\<and> b \\<noteq> 0\"\n and \"\\<forall> x. x^2 + a * x + b = (x - a) * (x - b)\"\n shows \" a = 1 \\<and> b = -2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_267:\n fixes x :: real\n assumes h0 : \"x \\<noteq> 1\"\n and h1 : \"x \\<noteq> -2\"\n and h2 : \"(x + 1) / (x - 1) = (x - 2) / (x + 2)\"\n shows \"x=0\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_232:\n fixes x y z::nat\n assumes \"x<31\" \"y<31\" \"z<31\"\n and \"[x *3 = 1] (mod 31)\"\n and \"[y * 5 = 1] (mod 31)\"\n and \"[z * (x + y) =1] (mod 31)\" \n shows \"z = 29\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_13:\n fixes u v :: nat\n assumes \"u>0 \\<and> v>0\"\n and \"(14 * u) mod 100 = 46\"\n and \"(14 * v) mod 100 = 46\"\n and \"u < 50\"\n and \"v < 100\"\n and \"50 < v\" \n shows \"(u + v) / 2 = 64\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_188:\n \"gcd 180 168 = (12::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_543 :\n \"(\\<Sum> k \\<in> ({n::nat. n dvd (30^4)}). 1) - 2 = (123::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2020_p21:\n \"card {n :: nat. 5 dvd n \\<and> lcm (fact 5) n \n = 5 * gcd (fact 10) n} = 48\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2013_p7:\n fixes s :: \"nat \\<Rightarrow> real\"\n assumes h0 : \"\\<And>n. s (n+2) = s (n+1) + s n\"\n and h1 : \"s 9 = 110\"\n and h2 : \"s 7 = 42\"\n shows \"s 4 = 10\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_28:\n fixes c :: real\n and f :: \"real \\<Rightarrow> real\"\n assumes h0 : \"\\<forall>x. f x = 2 * x^2 + 5 * x + c\"\n and h1 : \"\\<exists>x. f x \\<le> 0\"\n shows \"c \\<le> 25/8\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_412:\n fixes x y :: nat\n assumes h0 : \"x mod 19 = (4:: nat)\"\n and h1 : \"y mod 19 = (7:: nat)\"\n shows \"(x+1)^2 * (y+5)^3 mod 19 = (13:: nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2010_p10:\n fixes p q :: real\n and a :: \"nat \\<Rightarrow> real\"\n assumes h0 : \"\\<And>n. a (n+2) - a (n+1) = a (n+1) - a n\"\n and h1 : \"a 1 = p\"\n and h2 : \"a 2 = 9\"\n and h3 : \"a 3 = 3 * p - q\"\n and h4 : \"a 4 = 3 * p + q\"\n shows \"a 2010 = 8041\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_961:\n \"2003 mod 11 = (1::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12_2001_p2:\n fixes a b n::nat\n assumes \"1 \\<le> a \\<and> a \\<le> 9\"\n and \"0 \\<le> b \\<and> b \\<le> 9\"\n and \"n = 10 * a + b\"\n and \"n = a * b + a + b\"\n shows \"b=9\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem numbertheory_aneqprodakp4_anmsqrtanp1eq2:\n fixes a :: \"nat \\<Rightarrow> real\"\n assumes h0 : \"a 0 = 1\"\n and h1 : \"\\<And>n. a (n+1) = (\\<Prod>(k::nat) =1..n. (a k))+4\"\n shows \"\\<And>n. (n\\<ge>1) \\<Longrightarrow> a n - sqrt (a (n+1)) = 2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1964_p1_2:\n fixes n :: nat\n shows \"\\<not> ((7::nat) dvd (2^n + 1))\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12b_2021_p21:\n \"2 \\<le> (\\<Sum> k \\<in> {x ::real. 0 < x \\<and> x powr (2 powr (sqrt 2))\n = (sqrt 2) powr (2 powr x)}. k) \\<and> \n (\\<Sum> k \\<in> {x :: real. 0 < x \\<and> x powr (2 powr (sqrt 2)) \n = (sqrt 2)powr (2 powr x)}. k) < 6\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_109:\n fixes v :: \"nat \\<Rightarrow> nat\"\n assumes \"\\<forall> n. v n = 2 * n - 1\" \n shows \"(\\<Sum> k \\<in>{1..<101}. v k) mod 7 = 4\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_92:\n fixes n :: nat\n assumes h0 : \"(5 * n) mod 17 = 8\"\n shows \"n mod 17 = 5\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_43:\n fixes n :: nat\n assumes h0 : \"15^n dvd (fact 942)\"\n and h1 : \"\\<And>(m::nat). ((15::nat)^m dvd (fact 942)) \\<Longrightarrow> m \\<le> n\"\n shows \"n=233\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1977_p5:\n fixes a b q r :: nat\n assumes h0 : \"r < a + b\"\n and h1 : \"a^2 + b^2 = (a+b) * q + r\"\n and h2 : \"q^2 + r = 1977\"\n shows \"(abs (int a - 22) = 15 \\<and> abs (int b - 22) = 28) \\<or> (abs (int a - 22) = 28 \\<and> abs (int b - 22) = 15)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_422:\n fixes x :: real and \\<sigma>::\"real \\<Rightarrow> real\"\n assumes \"bij \\<sigma>\"\n and \\<sigma>:\"\\<forall> x. \\<sigma> x = 5 * x - 12\"\n and \"\\<sigma> (x + 1) = (Hilbert_Choice.inv \\<sigma>) x\" \n shows \"x = 47 / 24\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_manipexpr_apbeq2cceqiacpbceqm2:\n fixes a b c :: complex\n assumes h0 : \"a+b = 2*c\"\n and h1 : \"c = \\\"\n shows \"a*c+b*c=-2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem numbertheory_nckeqnm1ckpnm1ckm1:\n fixes n k ::nat\n assumes \"0 < n \\<and> 0 < k\"\n and \"k \\<le> n\" \n shows \"n choose k = (n - 1) choose k + (n - 1) choose (k - 1)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem aime_1990_p2:\n \"((52::real) + 6 * sqrt 43) powr (3/2) - ((52::real) - 6 * sqrt 43) powr (3/2) = 828\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_616:\n fixes f g :: \"real \\<Rightarrow> real\"\n assumes h0 : \"\\<And>x. f x = x^3 + 2 * x + 1\"\n and h1 : \"\\<And>x. g x = x - 1\"\n shows \"f (g 1) = 1\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2016_p3:\n fixes f :: \"real \\<Rightarrow> real \\<Rightarrow> real\"\n assumes h0 : \"\\<And>x y. f x y = x - y * floor (x/y)\"\n shows \"f ((3::real)/8) (- 2/5) = - 1/40\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_31:\n fixes x :: real\n and u :: \"nat \\<Rightarrow> real\"\n assumes \"\\<forall> n. u (n + 1) = sqrt (x + u n)\"\n and \"filterlim u at_top (nhds 9)\"\n shows \"9 = sqrt (x + 9)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_410:\n fixes x y :: real\n assumes h0 : \"y = x^2 - 6 * x + 13\"\n shows \"4 \\<le> y\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_sqineq_4bap1lt4bsqpap1sq:\n fixes a b :: real\n shows \"4 * b * (a+1) \\<le> 4 * b^2 + (a+1)^2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_198:\n \"(5^2005) mod 100 = (25::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_149:\n \"(\\<Sum> k\\<in> {x::nat. x<50 \\<and> x mod 8 =5 \\<and> x mod 6=3}. k) = 66\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_245:\n fixes x :: real\n assumes h0 : \"x \\<noteq> 0\"\n shows \"1/(4/x) * ((3*x^3)/x)^2 * (1/(1 / (2 * x)))^3 = 18 * x^8\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_301:\n fixes j :: nat \n assumes \"j>0\"\n shows \"(3 * (7 * j + 3)) mod 7 = 2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_132:\n \"2004 mod 12 = (0::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_257:\n fixes x :: nat\n assumes h0 : \"1 \\<le> x \\<and> x \\<le> 100\"\n and h1 : \"77 dvd ((\\<Sum>k::nat=0..100. k)-x)\"\n shows \"x=45\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2002_p21:\n fixes u:: \"nat\\<Rightarrow>nat\" and n::nat\n assumes \"u 0 =4\"\n and \"u 1=7\"\n and \"\\<forall> n \\<ge> 2. u (n + 2) = (u n + u (n + 1)) mod 10\"\n and \"(\\<Sum> k \\<in> {..n}. u k) > 10000\"\n shows \"1999 \\<le> n\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem aime_1994_p4:\n fixes n :: nat\n assumes \"0 < n\"\n and \"(\\<Sum> k \\<in> {1..<n+1}. floor (ln k / ln 2)) = 1994\" \n shows \"n = 312\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2015_p10:\n fixes x y:: nat\n assumes h0: \"0<y\"\n and h1: \"y<x\"\n and h2: \"x+y + (x*y) = 80\"\n shows \"x=26\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2009_p2:\n \"(1 + (1 / (1 + (1 / (1 + 1))))) = (5::real) / 3\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_405:\n fixes a b c :: nat\n and t :: \"nat \\<Rightarrow> nat\"\n assumes h0 : \"t 0 = 0\"\n and h1 : \"t 1 = 1\"\n and h2 : \"\\<And>n. (n > 1) \\<Longrightarrow> t n = t (n-2) + t (n-1)\"\n and h3 : \"a mod 16 = 5\"\n and h4 : \"b mod 16 = 10\"\n and h5 : \"c mod 16 = 15\"\n shows \"(t a + t b + t c) mod 7 = 5\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1973_p3:\n fixes a b :: real\n assumes h0 : \"\\<exists>x. x^4 + a * x^3 + b * x^2 + a*x + 1 = 0\"\n shows \"4/5 \\<le> a^2 + b^2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2009_p5:\n fixes x :: real\n assumes h0 : \"x^3 - (x+1) * (x-1) * x = 5\"\n shows \"x^3 = 125\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1979_p1:\n fixes p q :: nat \n assumes \"0 < q\"\n and \"(\\<Sum> k \\<in> {1..<1320}. ((-1) ^ (k + 1) * (1 / k)))\n = p / q\" \n shows \"1979 dvd p\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_43:\n fixes a b :: real\n and f :: \"real \\<Rightarrow> real\"\n assumes h0 : \"\\<And>x. f x = a * x + b\"\n and h1 : \"f 7 = 4\"\n and h2 : \"f 6 = 3\"\n shows \"f 3 = 0\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_462:\n \"((1::real)/2 + 1/3) * (1/2 - 1/3) = 5/36\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem aime_1984_p5:\n fixes a b ::real\n assumes \"(ln a) / (ln 8) + (ln (b^2)) / (ln 4) = 5\"\n \"(ln b) / (ln 8) + (ln (a^2)) / (ln 4) = 7\"\n shows \"a * b = 512\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2010_p11:\n fixes x b :: real\n assumes \"0 < b\"\n and \"7 powr (x + 7) = 8 powr x\"\n and \"x = ln (7^7) / ln b\" \n shows \"b = 8 / 7\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem numbertheory_2dvd4expn:\n fixes n :: nat\n assumes h0 : \"n \\<noteq> 0\"\n shows \"(2::nat) dvd 4^n\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem aimeII_2001_p3:\n fixes x :: \"nat \\<Rightarrow> int\"\n assumes h0 : \"x 1 = 211\"\n and h1 : \"x 2 = 375\"\n and h2 : \"x 3 = 420\"\n and h3 : \"x 4 = 523\"\n and h4 : \"\\<And>(n::nat). ((n\\<ge>5) \\<Longrightarrow> (x n = x (n-1) - x (n-2) + x (n-3) - x (n-4)))\"\n shows \"x 531 + x 753 + x 975 = 898\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12_2000_p11:\n fixes a b::real\n assumes \"a \\<noteq> 0\" \"b \\<noteq> 0\"\n and \"a * b = a - b\"\n shows \"a / b + b / a - a * b = 2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_156:\n fixes n :: nat\n assumes h0: \"n > 0\"\n shows \"gcd (n+7) (2*n+1) \\<le> 13\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_530:\n fixes n k :: nat\n assumes \"n / k < 6\"\n and \"5 < n / k\" \n shows \"22 \\<le> (lcm n k) / (gcd n k)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1978_p5:\n fixes n :: nat and f :: \"nat \\<Rightarrow> nat\"\n assumes \"inj f\" and \"f 0 = 0\"\n shows \"(\\<Sum> k \\<in>{1..<n+1}. 1 / k) \\<le> (\\<Sum> k \\<in>{1..<n+1}. (f k) / k^2)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem induction_sum2kp1npqsqm1:\n fixes n :: nat \n shows \"(\\<Sum> k<n. 2 * k + 3) = (n + 1)^2 - 1\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_55:\n fixes q p :: real\n assumes h0 : \"q = 2 - 4 + 6 - 8 + 10 -12 + 14\"\n and h1 : \"p = 3 - 6 + 9 - 12 + 15 - 18 + 21\"\n shows \"q/p = 2/3\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem aime_1983_p9:\n fixes x::real\n assumes \"0<x\" \"x<pi\"\n shows \"12 \\<le> ((9 * (x^2 * (sin x)^2)) + 4) / (x * sin x)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_131:\n fixes a b :: real\n and f :: \"real \\<Rightarrow> real\"\n assumes h0 : \"\\<And>x. f x = 2 * x^2 - 7 * x + 2\"\n and h1 : \"f a = 0\"\n and h2 : \"f b = 0\"\n and h3 : \"a \\<noteq> b\"\n shows \"1 / (a-1) + 1 / (b-1) = -1\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2013_p8:\n fixes x y :: real\n assumes h0 : \"x\\<noteq>0\"\n and h1 : \"y\\<noteq>0\"\n and h2 : \"x\\<noteq>y\"\n and h3 : \"x + 2/x = y + 2/y\"\n shows \"x * y = 2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_466:\n \"(\\<Sum> k< 11. k) mod 9 = (1::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_192:\n fixes q e d :: complex\n assumes h0 : \"q = Complex 11 (-5)\"\n and h1 : \"e = Complex 11 5\"\n and h2 : \"d = Complex 0 2\"\n shows \"q * e * d = Complex 0 292\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_629 :\n \"(LEAST t::nat. (lcm 12 t)^3 = (12 * t)^2) = 18\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem aime_1984_p15:\n fixes x y z w::real\n assumes \"(x^2 / (2^2 - 1)) + (y^2 / (2^2 - 3^2)) \n + (z^2 / (2^2 - 5^2)) + (w^2 / (2^2 - 7^2)) = 1\"\n \"(x^2 / (4^2 - 1)) + (y^2 / (4^2 - 3^2)) \n + (z^2 / (4^2 - 5^2)) + (w^2 / (4^2 - 7^2)) = 1\"\n \"(x^2 / (6^2 - 1)) + (y^2 / (6^2 - 3^2)) \n + (z^2 / (6^2 - 5^2)) + (w^2 / (6^2 - 7^2)) = 1\"\n \"(x^2 / (8^2 - 1)) + (y^2 / (8^2 - 3^2)) \n + (z^2 / (8^2 - 5^2)) + (w^2 / (8^2 - 7^2)) = 1\"\n shows \"x^2 + y^2 + z^2 + w^2 = 36\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1990_p3:\n fixes n :: nat\n assumes \"2 \\<le> n\"\n and \"n^2 dvd 2^n + 1\"\n shows \"n = 3\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_2rootsintpoly_am10tap11eqasqpam110:\n fixes a :: complex\n shows \"(a-10) * (a+11) = a^2 + a -110\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_461:\n fixes n :: nat\n assumes \"n = card {k::nat. gcd k 8 = 1 \\<and> 1\\<le>k \\<and> k < 8}\" \n shows \"(3^n) mod 8 = (1::nat)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_144:\n fixes a b c d :: nat\n assumes h0:\"c - b = d\"\n and h1:\"b - a = d\"\n and h2: \"a+b+c = 60\"\n and h3: \"a + b > c\"\n shows \"d < 10\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_282:\n fixes f :: \"real \\<Rightarrow> real\"\n assumes \"\\<forall> x. (x \\<in> \\<rat> ) \\<longrightarrow> f x = abs (floor x)\"\n and \"\\<forall> x. (x \\<notin> \\<rat>) \\<longrightarrow> f x = (ceiling x)^2\" \n shows \"f (8 powr (1/3)) + f (-pi) + f (sqrt 50) + f (9/2) = 79\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2008_p8:\n fixes x y::real\n assumes h0: \"0 < x \\<and> 0 < y\"\n and h1: \"y^3 = 1\"\n and h2: \"6 * x^2 = 2 * (6 * y^2)\"\n shows \"x^3 = 2 * sqrt 2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem algebra_sqineq_2unitcircatblt1:\n fixes a b :: real\n assumes \"a^2 + b^2 = 2\"\n shows \"a * b <= 1\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_393:\n fixes \\<sigma>::\"real \\<Rightarrow> real\" \n assumes \"bij \\<sigma>\"\n and \"\\<forall> x. \\<sigma> x = 4 * x^3 + 1\"\n shows \"Hilbert_Choice.inv \\<sigma> 33 = 2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_15:\n fixes s :: \"nat \\<Rightarrow> nat \\<Rightarrow> nat\"\n assumes h0: \"\\<And>a b. s a b = a ^ b + b ^ a\"\n shows \"s 2 6 = 100\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_510:\n fixes x y :: real\n assumes h0 : \"x+y=13\"\n and h1 : \"x*y=24\"\n shows \"sqrt (x^2 + y^2) = 11\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem aime_1991_p1:\n fixes x y :: nat\n assumes h0 : \"0<x \\<and> 0<y\"\n and h1 : \"x*y + (x+y) = 71\"\n and h2 : \"x^2 * y + x * y^2=880\"\n shows \"x^2 + y^2=146\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_69:\n fixes r s :: nat\n assumes \"r * s = 450\"\n and \"(r + 5) * (s - 3) = 450\" \n shows \"r = 25\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem aime_1991_p6:\n fixes r :: real\n assumes \"(\\<Sum> k \\<in>{19::nat..<92}. (floor (r + k / 100))) = 546\" \n shows \"floor (100 * r) = 743\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem aime_1987_p8:\n fixes n :: nat\n assumes h0 : \"0 < n\"\n and h1 : \"\\<not> (\\<exists>!k. (8 / 15 < n / (n+k)) \\<and> n / (n+k) < 7/13)\"\n shows \"n \\<le> 112\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_433:\n fixes f :: \"real \\<Rightarrow> real\"\n assumes h0 : \"\\<And>x. f x = 3 * sqrt (2 * x -7) - 8\"\n shows \"f 8 = 1\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem aime_1997_p11:\n fixes x :: real\n assumes h0 : \"x = (\\<Sum>(n::nat) =1..44. cos(n*pi/180)) / (\\<Sum>(n::nat) =1..44. sin(n*pi/180))\"\n shows \"floor (100*x) = 241\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem amc12a_2017_p7:\n fixes f :: \"nat \\<Rightarrow> real\"\n assumes h0 : \"f 1 = 2\"\n and h1 : \"\\<And>n. (1 < n \\<and> even n) \\<Longrightarrow> f n = f (n - 1) + 1\"\n and h2 : \"\\<And>n. (1 < n \\<and> odd n) \\<Longrightarrow> f n = f (n - 2) + 2\"\n shows \"f 2017 = 2018\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem imo_1967_p3:\n fixes k m n :: nat\n and c :: \"nat \\<Rightarrow> nat\"\n assumes h0 : \"0<k \\<and> 0<m \\<and> 0<n\"\n and h1 : \"\\<And>s. c s = s * (s+1)\"\n and h2 : \"prime (k+m+1)\"\n and h3 : \"n+1 < k + m + 1\"\n shows \"(\\<Prod>(i::nat) = 1..n.(c i)) dvd (\\<Prod>(i::nat) = 1..n.(c (m+i)) - c k)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_104:\n fixes x :: real\n assumes h0 : \"125/8 = x /12\"\n shows \"x = 375/2\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_numbertheory_84:\n \"floor ((9::real) / 160 * 100) = (5::int)\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_214:\n fixes a :: real\n and f :: \"real \\<Rightarrow> real\"\n assumes h0 : \"\\<And>x. f x = a * (x-2)^2 + 3\"\n and h1 : \"f 4 = 4\"\n shows \"f 6 = 7\""], "miniF2F valid"], ["/tiger/u/kefan/Software/Isabelle2022/src/HOL/Examples/Full.thy", "\n ", ["theorem mathd_algebra_67:\n fixes f g :: \"real \\<Rightarrow> real\"\n assumes h0 : \"\\<And>x. f x = 5 * x + 3\"\n and h1 : \"\\<And>x. g x = x^2 - 2\"\n shows \"g (f (-1)) = 2\""], "miniF2F valid"]]

SFT/train.json ADDED Viewed

	@@ -0,0 +1,3 @@

+version https://git-lfs.github.com/spec/v1
+oid sha256:dae782fdeebfd90887a526eb707d6d5681f2a2721ea92ff407297b44d2e486d5
+size 3101994133

SFT/val.json ADDED Viewed

	@@ -0,0 +1,3 @@

+version https://git-lfs.github.com/spec/v1
+oid sha256:c4dd6a83e55160d6c004405cf069a7dce4700f006bba7b0e2f70cb11ad85a2ed
+size 28530726

SFT_noinvoke/train.json ADDED Viewed

	@@ -0,0 +1,3 @@

+version https://git-lfs.github.com/spec/v1
+oid sha256:4ae50ac8e39f4bcf9a05b638cc322868799ea25c2f0086867c9b301675413fcf
+size 4279948526

SFT_noinvoke/val.json ADDED Viewed

	@@ -0,0 +1,3 @@

+version https://git-lfs.github.com/spec/v1
+oid sha256:1b06a77a4fc042c37300f600ec8f5d4fcf725083c6006a2ddbe9d8bfb47ba414
+size 32207448

holdout.json ADDED Viewed

	@@ -0,0 +1 @@

+ ["Verified_SAT_Based_AI_Planning", "SIFPL", "Khovanskii_Theorem", "Bondy", "Rewriting_Z", "Decreasing-Diagrams-II", "Registers", "LocalLexing", "FeatherweightJava", "FFT", "Knot_Theory", "Eval_FO", "Saturation_Framework_Extensions", "Hales_Jewett", "SPARCv8", "CoSMeDis", "LP_Duality", "PAPP_Impossibility", "Groebner_Macaulay", "Abstract-Hoare-Logics", "PCF", "Jordan_Hoelder", "Knights_Tour", "FOL_Seq_Calc3", "Cartan_FP", "InformationFlowSlicing_Inter", "LOFT", "Diophantine_Eqns_Lin_Hom", "Dynamic_Tables", "Schutz_Spacetime", "Elliptic_Curves_Group_Law", "ArrowImpossibilityGS", "Goodstein_Lambda", "XML", "GenClock", "Topological_Semantics"]

tests/afp_2022_test.json ADDED Viewed

	@@ -0,0 +1,3 @@

+version https://git-lfs.github.com/spec/v1
+oid sha256:fdb895731452a1609d264692e5590264e316e9dbd0ba456ad77a60bf1ddaefaf
+size 24085301

tests/afp_2023_test.json ADDED Viewed

	@@ -0,0 +1,3 @@

+version https://git-lfs.github.com/spec/v1
+oid sha256:faa3b8a3d563449c57fa4b1e1af75650c102deee114c02fce564c5ca0a0efd82
+size 11352546

tests/unformatted_miniF2F_raw.json ADDED Viewed

The diff for this file is too large to render. See raw diff

tests_noinvoke/afp_2022_test.json ADDED Viewed

	@@ -0,0 +1,3 @@

+version https://git-lfs.github.com/spec/v1
+oid sha256:9284ab349905cfac0db6b02dc46d10cd1d93cbd26a05e926b1b67c2fb3e12be4
+size 71937653

tests_noinvoke/afp_2022_val.json ADDED Viewed

	@@ -0,0 +1,3 @@

+version https://git-lfs.github.com/spec/v1
+oid sha256:fe5ca36efd7cf41b68bb8ce36296930cf7d36757b9987d1fdd38fad7e77a165a
+size 33322975