Open DyeKuu opened 2 years ago
I deleted the entries for the statements not yet formalized.
HOL Light Tracking:
[x] amc12a_2020_p22 Wrong name, should be amc12a_2020_p21. Also, the answer should be 48.
[x] mathd_algebra_77 This problem has also a solution a = b = -1/2.
[x] mathd_algebra_421 The assumption a ≤ c needs to be changed into a < c.
[x] numbertheory_nckeqnm1ckpnm1ckm1 This problem does not match its name.
[x] mathd_numbertheory_155 The answer is 48.
[x] amc12_2000_p1 The condition i =/= 0, m =/= 0, k =/= 0 should become i =/= m, m =/= k, k =/= i.
[x] amc12a_2021_p12 The thesis should be b = -88.
[x] imo_2007_p6 Check summation - the term (a 100)^2 * a 1 is probably inside the summation.
[x] imo_2019_p1 Missing brackets around the first quantifier
[x] mathd_algebra_17 add the assumption 1 + a > 0.
[x] mathd_algebra_276 The sum should have been 7.
[x] mathd_algebra_288 This simply doesn't hold.
[x] mathd_algebra_320 We need to normalize the variables a, b, c, for example by fixing c = 2.
[x] mathd_algebra_332 Is wrong.
[x] mathd_algebra_487 Is wrong.
[x] numbertheory_notequiv2i2jasqbsqdiv8 Is wrong. Counterexample: a = b = 0
Here a list of theorems possibly containing errors, mirrored from #7
I deleted the entries for the statements not yet formalized.
HOL Light Tracking:
[x] amc12a_2020_p22 Wrong name, should be amc12a_2020_p21. Also, the answer should be 48.
[x] mathd_algebra_77 This problem has also a solution a = b = -1/2.
[x] mathd_algebra_421 The assumption a ≤ c needs to be changed into a < c.
[x] numbertheory_nckeqnm1ckpnm1ckm1 This problem does not match its name.
[x] mathd_numbertheory_155 The answer is 48.
[x] amc12_2000_p1 The condition i =/= 0, m =/= 0, k =/= 0 should become i =/= m, m =/= k, k =/= i.
[x] amc12a_2021_p12 The thesis should be b = -88.
[x] imo_2007_p6 Check summation - the term (a 100)^2 * a 1 is probably inside the summation.
[x] imo_2019_p1 Missing brackets around the first quantifier
[x] mathd_algebra_17 add the assumption 1 + a > 0.
[x] mathd_algebra_276 The sum should have been 7.
[x] mathd_algebra_288 This simply doesn't hold.
[x] mathd_algebra_320 We need to normalize the variables a, b, c, for example by fixing c = 2.
[x] mathd_algebra_332 Is wrong.
[x] mathd_algebra_487 Is wrong.
[x] numbertheory_notequiv2i2jasqbsqdiv8 Is wrong. Counterexample: a = b = 0