From 34174040a2c2d4ed11dc45720759262e91be66c5 Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@caltech.edu>
Date: Fri, 26 May 2023 17:45:19 -0700
Subject: [PATCH 1/3] Add machine generated proofs.

---
 lean/src/test.lean  | 52 ++++++++++++++++++++++++++++++---------------
 lean/src/valid.lean | 35 ++++++++++++++----------------
 2 files changed, 51 insertions(+), 36 deletions(-)

diff --git a/lean/src/test.lean b/lean/src/test.lean
index 64c89c04..fa555f22 100644
--- a/lean/src/test.lean
+++ b/lean/src/test.lean
@@ -133,7 +133,8 @@ end
 theorem mathd_numbertheory_237 :
   (∑ k in (finset.range 101), k) % 6 = 4 :=
 begin
-  sorry
+  rw [finset.sum_range_succ'],
+  norm_num [finset.sum_range_succ],
 end
 
 theorem mathd_algebra_33
@@ -644,7 +645,7 @@ end
 theorem mathd_numbertheory_175 :
   (2^2010) % 10 = 4 :=
 begin
-  sorry
+  norm_num [pow_succ],
 end
 
 theorem induction_sumkexp3eqsumksq
@@ -836,13 +837,15 @@ theorem mathd_numbertheory_293
   (h₁ : 11∣20 * 100 + 10 * n + 7) :
   n = 5 :=
 begin
-  sorry
+  contrapose! h₁,
+  norm_num [h₁],
+  dec_trivial!,
 end
 
 theorem mathd_numbertheory_769 :
   (129^34 + 96^38) % 11 = 9 :=
 begin
-  sorry
+  norm_num [add_assoc],
 end
 
 theorem mathd_algebra_452
@@ -986,7 +989,9 @@ end
 theorem amc12a_2013_p4 :
   (2^2014 + 2^2012) / (2^2014 - 2^2012) = (5:ℝ) / 3 :=
 begin
-  sorry
+  rw div_eq_iff,
+  norm_num,
+  norm_num,
 end
 
 theorem mathd_algebra_392
@@ -1020,7 +1025,9 @@ end
 theorem mathd_numbertheory_343 :
   (∏ k in finset.range 6, (2 * k + 1)) % 10 = 5 :=
 begin
-  sorry
+  rw [finset.prod_range_succ, 
+  finset.prod_range_succ],
+  norm_num [finset.prod, finset.prod_range_succ],
 end
 
 theorem mathd_algebra_756
@@ -1681,7 +1688,9 @@ theorem mathd_numbertheory_100
   (h₂ : nat.lcm n 40 = 280) :
   n = 70 :=
 begin
-  sorry
+  have h₃ := nat.gcd_mul_lcm n 40,
+  rw [h₁, h₂] at h₃, 
+  linarith,
 end
 
 theorem mathd_algebra_313
@@ -1874,7 +1883,7 @@ end
 theorem mathd_numbertheory_212 :
   (16^17 * 17^18 * 18^19) % 10 = 8 :=
 begin
-  sorry
+  norm_num,
 end
 
 theorem mathd_numbertheory_320
@@ -1893,7 +1902,9 @@ theorem mathd_algebra_125
   (h₂ : (↑x - (3:ℤ)) + (y - (3:ℤ)) = 30) :
   x = 6 :=
 begin
-  sorry
+  revert h₂,
+  intro h,
+  linarith,
 end
 
 theorem induction_1pxpownlt1pnx
@@ -2212,7 +2223,7 @@ end
 theorem mathd_numbertheory_239 :
   (∑ k in finset.Icc 1 12, k) % 4 = 2 :=
 begin
-  sorry
+  simpa using nat.mod_add_div 1 12,
 end
 
 theorem amc12b_2002_p2
@@ -2247,7 +2258,7 @@ end
 theorem mathd_numbertheory_517 :
   (121 * 122 * 123) % 4 = 2 :=
 begin
-  sorry
+  norm_num1,
 end
 
 theorem amc12a_2009_p7
@@ -2515,7 +2526,8 @@ end
 theorem mathd_numbertheory_127 :
   (∑ k in (finset.range 101), 2^k) % 7 = 3 :=
 begin
-  sorry
+  rw [finset.sum_range_succ, finset.sum_range_succ],
+  norm_num [finset.sum],
 end
 
 theorem imo_1974_p3
@@ -2550,7 +2562,9 @@ theorem mathd_algebra_158
   (h₁ : ↑∑ k in finset.range 8, (2 * k + 1) - ↑∑ k in finset.range 5, (a + 2 * k) = (4:ℤ)) :
   a = 8 :=
 begin
-  sorry
+  simp only [nat.cast_sum, finset.sum_range_succ] at h₁,
+  simp at h₁,
+  linarith,
 end
 
 theorem algebra_absxm1pabsxpabsxp1eqxp2_0leqxleq1
@@ -2570,7 +2584,8 @@ theorem aime_1990_p4
   (h₄ : 1 / (x^2 - 10 * x - 29) + 1 / (x^2 - 10 * x - 45) - 2 / (x^2 - 10 * x - 69) = 0) :
   x = 13 :=
 begin
-  sorry
+  field_simp at h₃ h₄,
+  nlinarith,
 end
 
 theorem mathd_numbertheory_541
@@ -2653,7 +2668,9 @@ theorem mathd_numbertheory_150
   (h₀ : ¬ nat.prime (7 + 30 * n)) :
   6 ≤ n :=
 begin
-  sorry
+  contrapose! h₀,
+  rw nat.prime_def_lt,
+  dec_trivial!,
 end
 
 theorem aime_1989_p8
@@ -2663,7 +2680,7 @@ theorem aime_1989_p8
   (h₂ : 9 * a + 16 * b + 25 * c + 36 * d + 49 * e + 64 * f + 81 * g = 123) :
   16 * a + 25 * b + 36 * c + 49 * d + 64 * e + 81 * f + 100 * g = 334 :=
 begin
-  sorry
+  linarith,
 end
 
 theorem mathd_numbertheory_296
@@ -2719,7 +2736,8 @@ theorem mathd_numbertheory_185
   (h₀ : n % 5 = 3) :
   (2 * n) % 5 = 1 :=
 begin
-  sorry
+  rw ← nat.mod_add_div n 5,
+  norm_num [h₀, nat.mul_mod],
 end
 
 theorem mathd_algebra_441
diff --git a/lean/src/valid.lean b/lean/src/valid.lean
index f2569be5..c2afe834 100644
--- a/lean/src/valid.lean
+++ b/lean/src/valid.lean
@@ -96,7 +96,8 @@ end
 theorem mathd_numbertheory_169 :
   nat.gcd 20! 200000 = 40000 :=
 begin
-  sorry
+  rw nat.gcd_comm,
+  norm_num,
 end
 
 theorem amc12a_2009_p9
@@ -145,7 +146,8 @@ end
 theorem mathd_numbertheory_149 :
   ∑ k in (finset.filter (λ x, x % 8 = 5 ∧ x % 6 = 3) (finset.range 50)), k = 66 :=
 begin
-  sorry
+  rw [finset.sum_filter, finset.sum_range_succ],
+  dec_trivial,
 end
 
 theorem imo_1984_p2
@@ -260,7 +262,8 @@ end
 theorem mathd_numbertheory_466 :
   (∑ k in (finset.range 11), k) % 9 = 1 :=
 begin
-  sorry
+  rw [finset.sum_range_succ, finset.sum_range_succ], 
+  norm_num [finset.sum],
 end
 
 theorem mathd_algebra_48
@@ -930,17 +933,9 @@ end
 theorem mathd_numbertheory_211 :
   finset.card (finset.filter (λ n, 6 ∣ (4 * ↑n - (2 : ℤ))) (finset.range 60)) = 20 :=
 begin
-  -- apply le_antisymm,
-  -- -- haveI := classical.prop_decidable,
-  -- swap,
-  -- dec_trivial!,
-  -- apply le_trans,
-  -- swap,
-  -- apply nat.le_of_dvd,
-  -- { norm_num, },
-  -- -- haveI := classical.dec,
-  -- simp,
-  sorry
+  rw finset.card_eq_sum_ones,
+  rw [finset.sum_filter, finset.sum_range_succ'],
+  dec_trivial,
 end
 
 theorem mathd_numbertheory_640 :
@@ -1454,7 +1449,7 @@ end
 theorem mathd_numbertheory_252 :
   7! % 23 = 3 :=
 begin
-  sorry
+  norm_num [fin.succ_ne_zero],
 end
 
 theorem amc12a_2020_p21
@@ -1504,7 +1499,7 @@ end
 theorem mathd_numbertheory_269 :
   (2005^2 + 2005^0 + 2005^0 + 2005^5) % 100 = 52 :=
 begin
-  sorry
+  norm_num,
 end
 
 theorem aime_1990_p2 :
@@ -1714,7 +1709,8 @@ theorem mathd_algebra_616
   (h₁ : ∀ x, g x = x - 1) :
   f (g 1) = 1 :=
 begin
-  sorry
+  simp only [h₀, h₁, pow_one],
+  ring,
 end
 
 theorem mathd_numbertheory_690 :
@@ -2375,7 +2371,8 @@ theorem amc12a_2017_p2
   (h₂ : x + y = 4 * (x * y)) :
   1 / x + 1 / y = 4 :=
 begin
-  sorry
+  field_simp [h₀, h₁, h₂],
+  linarith,
 end
 
 theorem algebra_amgm_sumasqdivbsqgeqsumbdiva
@@ -2389,7 +2386,7 @@ end
 theorem mathd_numbertheory_202 :
   (19^19 + 99^99) % 10 = 8 :=
 begin
-  sorry
+  norm_num [add_comm, add_assoc],
 end
 
 theorem imo_1979_p1

From 8b1954099f9f5257582238f1d4eadbbffb9bfb55 Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@caltech.edu>
Date: Tue, 30 May 2023 23:18:45 -0700
Subject: [PATCH 2/3] Update test.lean

---
 lean/src/test.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/lean/src/test.lean b/lean/src/test.lean
index fa555f22..e5a3e36e 100644
--- a/lean/src/test.lean
+++ b/lean/src/test.lean
@@ -1025,8 +1025,7 @@ end
 theorem mathd_numbertheory_343 :
   (∏ k in finset.range 6, (2 * k + 1)) % 10 = 5 :=
 begin
-  rw [finset.prod_range_succ, 
-  finset.prod_range_succ],
+  rw [finset.prod_range_succ, finset.prod_range_succ],
   norm_num [finset.prod, finset.prod_range_succ],
 end
 

From 5740c4ac7978a97b25a747c5ade52f896edce1f7 Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@caltech.edu>
Date: Wed, 7 Jun 2023 00:55:08 -0700
Subject: [PATCH 3/3] add additional machine-generated proofs

---
 lean/src/test.lean  |  7 +++++--
 lean/src/valid.lean | 16 +++++++++++-----
 2 files changed, 16 insertions(+), 7 deletions(-)

diff --git a/lean/src/test.lean b/lean/src/test.lean
index fa555f22..ece14bfc 100644
--- a/lean/src/test.lean
+++ b/lean/src/test.lean
@@ -454,7 +454,9 @@ end
 theorem mathd_numbertheory_12 :
   finset.card (finset.filter (λ x, 20∣x) (finset.Icc 15 85)) = 4 :=
 begin
-  sorry
+  classical,
+  classical,
+  refine finset.card_eq_sum_ones _,
 end
 
 theorem mathd_numbertheory_345 :
@@ -466,7 +468,8 @@ end
 theorem mathd_numbertheory_447 :
   ∑ k in finset.filter (λ x, 3∣x) (finset.Icc 1 49), (k % 10) = 78 :=
 begin
-  sorry
+  dsimp,
+  dec_trivial,
 end
 
 theorem mathd_numbertheory_328 :
diff --git a/lean/src/valid.lean b/lean/src/valid.lean
index c2afe834..fb3c73cc 100644
--- a/lean/src/valid.lean
+++ b/lean/src/valid.lean
@@ -688,7 +688,8 @@ theorem mathd_numbertheory_335
   (h₀ : n % 7 = 5) :
   (5 * n) % 7 = 4 :=
 begin
-  sorry
+  rw [nat.mul_mod, h₀], 
+  norm_num,
 end
 
 theorem mathd_numbertheory_35
@@ -961,6 +962,7 @@ theorem algebra_2rootsintpoly_am10tap11eqasqpam110
 begin
   ring,
 end
+
 theorem aime_1991_p1
   (x y : ℕ)
   (h₀ : 0 < x ∧ 0 < y)
@@ -1389,7 +1391,8 @@ theorem mathd_numbertheory_458
   (h₀ : n % 8 = 7) :
   n % 4 = 3 :=
 begin
-  sorry
+  rw [← nat.mod_mod_of_dvd n, h₀],
+  all_goals {norm_num},
 end
 
 theorem amc12a_2008_p15
@@ -1556,7 +1559,8 @@ theorem mathd_algebra_144
   (h₃ : a + b > c) :
   d < 10 :=
 begin
-  sorry
+  contrapose! h₃,
+  linarith,
 end
 
 theorem mathd_algebra_282
@@ -1952,7 +1956,8 @@ theorem mathd_numbertheory_370
   (h₀ : n % 7 = 3) :
   (2 * n + 1) % 7 = 0 :=
 begin
-  sorry
+  norm_num [nat.succ_mul, h₀],
+  norm_num [nat.add_mod, h₀],
 end
 
 theorem mathd_algebra_437
@@ -2315,7 +2320,8 @@ theorem mathd_numbertheory_412
   (h₁ : y % 19 = 7) :
   ((x + 1)^2 * (y + 5)^3) % 19 = 13 :=
 begin
-  sorry
+  norm_num [pow_succ],
+  norm_num [nat.add_mod, nat.mul_mod, h₀, h₁],
 end
 
 theorem mathd_algebra_181