[Lean Tracking] errors in problems

[albertqjiang]

There are a bunch of errors in Isabelle, the majority of which were mirrored from Lean

Here a list of theorems possibly containing errors:

It is worth looking into for each language.

I create this issue for Lean Specifically. For fixing in other languages, copy and create another issue.

• [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_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] imo_1978_p5 Missing assumption that f has range [1, n]

• [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] mathd_algebra_451 Is wrong.

• [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] amc12b_2021_p4 Is simply wrong.

• [x] imo_1965_p2 The condition "a 7 < 0 ∧ a 9 < 0" should be "a 6 < 0 ∧ a 7 < 0"

• [x] imo_1974_p3 Bad summation range

• [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_276 The sum should have been 7.

• [x] mathd_algebra_288 This simply doesn't hold.

• [x] mathd_algebra_293 It should be: sqrt (60 x) sqrt (12 x) sqrt (63 x) = 36 |x| sqrt (35 x)

• [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] mathd_numbertheory_728 The remainder should be 3.

• [x] numbertheory_notequiv2i2jasqbsqdiv8 Is wrong. Counterexample: a = b = 0

[DyeKuu]

I doubt imo_1966_p5 Missing assumption a1 > a2 > a3 > a4.

This assumption is introduced in the proof a1 > a2 > a3 > a4 to get rid of the symmetry of abs value. https://artofproblemsolving.com/wiki/index.php/1966_IMO_Problems/Problem_5

So if we don't assume it, it should be fine with the abs values.

[Wenda302]

Hmm, if we are breaking the symmetry in a different way, say a4>a2>a3>a1, then we should have x1=x4=1/(a4-a1).

[DyeKuu]

Lean version all fixed! 🏁

[DyeKuu]

Metamath & Lean & HOL Light are all good (at least for now)! Thank you all for your great job! @Wenda302 @albertqjiang @timlacroix @malachaux for what have been done (I like the collection of the informal part so much).

[albertqjiang]

Thanks @DyeKuu !!!! That was a blast!

We'll open source it very soon for the world to use it :)

[Wenda302]

Thanks a lot for your effort @DyeKuu! The dataset is looking increasingly better :-)