Here a list of theorems possibly containing errors, mirrored from #7
It is worth looking into for each language.
Metamath Tracking:
[x] Also, please take a closer look at imo_2007_p6. The summation is indeed wrong.
[x] aime_1987_p8
The assumptions are wrong! In current form the problem is wrong.
[x] aime_1996_p5
Missing assumptions that a, b, c are pairwise different
[x] aime_1997_p12
That's a minor problem. The name should be aime_1997_p11.
[x] aimeI_2001_p3
Again, a naming problem. Should be aimeII_2001_p3
[x] amc12a_2011_p18
A stronger thesis can be proved: x^2 - 6 * x + y^2 ≤ 8
[x] amc12a_2020_p13
Missing quantifier forall n.
[x] amc12a_2020_p22
Wrong name, should be amc12a_2020_p21. Also, the answer should be 48.
[x] imo_1962_p4
The last clause of the thesis should be: (∃(m::int). x = pi/6 + m pi/6) ∨ (∃(m::int). x = 5pi/6 + m pi/6) instead of: (∃(m::int). x = pi/6 + m pi/3)
Here a list of theorems possibly containing errors, mirrored from #7
It is worth looking into for each language.
Metamath Tracking:
[x] Also, please take a closer look at imo_2007_p6. The summation is indeed wrong.
[x] aime_1987_p8 The assumptions are wrong! In current form the problem is wrong.
[x] aime_1996_p5 Missing assumptions that a, b, c are pairwise different
[x] aime_1997_p12 That's a minor problem. The name should be aime_1997_p11.
[x] aimeI_2001_p3 Again, a naming problem. Should be aimeII_2001_p3
[x] amc12a_2011_p18 A stronger thesis can be proved: x^2 - 6 * x + y^2 ≤ 8
[x] amc12a_2020_p13 Missing quantifier forall n.
[x] amc12a_2020_p22 Wrong name, should be amc12a_2020_p21. Also, the answer should be 48.
[x] imo_1962_p4 The last clause of the thesis should be: (∃(m::int). x = pi/6 + m pi/6) ∨ (∃(m::int). x = 5pi/6 + m pi/6) instead of: (∃(m::int). x = pi/6 + m pi/3)
[x] imo_1966_p5 Missing assumption a1 > a2 > a3 > a4.
[x] imo_1974_p5 Missing assumption that a, b, c, d are positive.
[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] aime_1999_p11 need an additional assumption m > 0, and the condidtion dd/nn < 90 should be nn/dd < 90 instead.
[x] amc12_2000_p1 The condition i =/= 0, m =/= 0, k =/= 0 should become i =/= m, m =/= k, k =/= i.
[x] amc12a_2019_p12 There is a square (^2) missing
[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