Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

33 New Proofs Found by Machines #13

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

33 New Proofs Found by Machines #13

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3417404
Add machine generated proofs.
yangky11 May 27, 2023
8b19540
Update test.lean
yangky11 May 31, 2023
5740c4a
add additional machine-generated proofs
yangky11 Jun 7, 2023
c605019
Merge branch 'main' of github.com:yangky11/miniF2F into main
yangky11 Jun 7, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
58 changes: 39 additions & 19 deletions lean/src/test.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -453,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 :
Expand All @@ -465,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 :
Expand Down Expand Up @@ -644,7 +648,7 @@ end
theorem mathd_numbertheory_175 :
(2^2010) % 10 = 4 :=
begin
sorry
norm_num [pow_succ],
end

theorem induction_sumkexp3eqsumksq
Expand Down Expand Up @@ -836,13 +840,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
Expand Down Expand Up @@ -986,7 +992,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
Expand Down Expand Up @@ -1020,7 +1028,8 @@ 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
Expand Down Expand Up @@ -1681,7 +1690,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
Expand Down Expand Up @@ -1874,7 +1885,7 @@ end
theorem mathd_numbertheory_212 :
(16^17 * 17^18 * 18^19) % 10 = 8 :=
begin
sorry
norm_num,
end

theorem mathd_numbertheory_320
Expand All @@ -1893,7 +1904,9 @@ theorem mathd_algebra_125
(h₂ : (↑x - (3:ℤ)) + (y - (3:ℤ)) = 30) :
x = 6 :=
begin
sorry
revert h₂,
intro h,
linarith,
end

theorem induction_1pxpownlt1pnx
Expand Down Expand Up @@ -2212,7 +2225,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
Expand Down Expand Up @@ -2247,7 +2260,7 @@ end
theorem mathd_numbertheory_517 :
(121 * 122 * 123) % 4 = 2 :=
begin
sorry
norm_num1,
end

theorem amc12a_2009_p7
Expand Down Expand Up @@ -2515,7 +2528,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
Expand Down Expand Up @@ -2550,7 +2564,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
Expand All @@ -2570,7 +2586,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
Expand Down Expand Up @@ -2653,7 +2670,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
Expand All @@ -2663,7 +2682,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
Expand Down Expand Up @@ -2719,7 +2738,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
Expand Down
51 changes: 27 additions & 24 deletions lean/src/valid.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -685,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
Expand Down Expand Up @@ -930,17 +934,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 :
Expand All @@ -966,6 +962,7 @@ theorem algebra_2rootsintpoly_am10tap11eqasqpam110
begin
ring,
end

theorem aime_1991_p1
(x y : ℕ)
(h₀ : 0 < x ∧ 0 < y)
Expand Down Expand Up @@ -1394,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
Expand Down Expand Up @@ -1454,7 +1452,7 @@ end
theorem mathd_numbertheory_252 :
7! % 23 = 3 :=
begin
sorry
norm_num [fin.succ_ne_zero],
end

theorem amc12a_2020_p21
Expand Down Expand Up @@ -1504,7 +1502,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 :
Expand Down Expand Up @@ -1561,7 +1559,8 @@ theorem mathd_algebra_144
(h₃ : a + b > c) :
d < 10 :=
begin
sorry
contrapose! h₃,
linarith,
end

theorem mathd_algebra_282
Expand Down Expand Up @@ -1714,7 +1713,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 :
Expand Down Expand Up @@ -1956,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
Expand Down Expand Up @@ -2319,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
Expand Down Expand Up @@ -2375,7 +2377,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
Expand All @@ -2389,7 +2392,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
Expand Down