Some other issues reported by Yutaka Nagashima and Daniel Sebastian

[Wenda302]

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

• [x] algebra_manipexpr_apbeq2cceqiacpbceqm2 It's wrong, the assumption should be c = i

• [x] amc12a_2002_p12 We need an assumption that the quadratic has a root.

• [x] amc12a_2003_p25 The thesis should be a=0 ∨ a=-4

• [x] amc12a_2009_p25 Mistake in indexing. Should be: a (n+2) = (a n + a (n+1)) / (1 - (a n) * (a (n+1)))

• [x] amc12a_2010_p10 Wrong assumption. Should be: a 4 = 3 * p + q

• [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] imo_1977_p5 To ensure that the subtraction is calculated on integers (and not naturals) we should change the expression abs (a - 22) into abs (a - (22::int)) e.t.c.

• [x] imo_1978_p5 Missing assumption that f has range [1, n]

• [x] imo_1987_p6 A typo. floor(sqrt (q/3)) should become floor(sqrt (p/3))

• [x] mathd_algebra_48 The complex numbers are encoded badly.

• [x] mathd_algebra_77 This problem has also a solution a = b = -1/2.

• [x] mathd_algebra_110 The numbers are encoded badly (should remove the Re an Im parts)

• [x] mathd_algebra_192 This problem also encodes complex numbers badly.

• [x] mathd_algebra_421 The assumption a ≤ c needs to be changed into a < c.

• [x] mathd_algebra_451 Is wrong.

• [x] mathd_numbertheory_126 This problem also has a solution (x, a) = (37, 1480)

• [x] mathd_numbertheory_668 The assumption ∃x y::int. [x2=1] (mod 7) ∧ [x3=1] (mod 7) ⟶ r=x+y can never be satisfied.

• [x] numbertheory_nckeqnm1ckpnm1ckm1 This problem does not match its name.

• [x] mathd_numbertheory_155 The answer is 47.

[albertqjiang]

Great job! This is very clear. Again I'll work bottom up and tick the tasks

[albertqjiang]

numbertheory_nckeqnm1ckpnm1ckm1 This problem does not match its name.

I don't understand this one. the name looks correct to me @Wenda302

[albertqjiang]

• [x] Change all the inv to Hilbert_Choice.inv to avoid confusion errors

[albertqjiang]

mathd_numbertheory_155 The answer is 47.

The answer should be 48. I evaluated this and looked up the math dataset

[albertqjiang]

mathd_numbertheory_126 This problem also has a solution (x, a) = (37, 1480)

@Wenda302 how do you say that the smaller solution is ...?

[albertqjiang]

mathd_algebra_192 This problem also encodes complex numbers badly.

fixed but I don't think the original is "wrong"

[Wenda302]

mathd_numbertheory_126 This problem also has a solution (x, a) = (37, 1480)

@Wenda302 how do you say that the smaller solution is ...?

We use the Least operator. I got this one :-)

[Wenda302]

imo_2007_p6 was a silly mistake I overlooked in my previous skim-through. It is now fixed.

[Wenda302]

aime_1997_p12, aimeI_2001_p3, and amc12a_2020_p22: the problem has also been noticed by Gary. Shall we rename the current .thy file & the theorem name? @albertqjiang

[Wenda302]

It appears that you were considering Im 1 = \<i> or Im 7 = 7 * \<i> in Isabelle, Albert :-)

[Wenda302]

@albertqjiang I pushed my fixes for problems from top to bottom until (and including) imo_1978_p5, plus mathd_numbertheory_126.

[Wenda302]

numbertheory_nckeqnm1ckpnm1ckm1 This problem does not match its name.

I don't understand this one. the name looks correct to me @Wenda302

Ahh, me neither. I guess they mean the problem itself does not look like a number theory problem?

[albertqjiang]

aime_1997_p12, aimeI_2001_p3, and amc12a_2020_p22: the problem has also been noticed by Gary. Shall we rename the current .thy file & the theorem name? @albertqjiang

The naming problem has already been fixed

[albertqjiang]

It appears that you were considering Im 1 = \<i> or Im 7 = 7 * \<i> in Isabelle, Albert :-)

Wait is this not true?

[albertqjiang]

numbertheory_nckeqnm1ckpnm1ckm1 This problem does not match its name. I don't understand this one. the name looks correct to me @Wenda302

Ahh, me neither. I guess they mean the problem itself does not look like a number theory problem?

Let's leave this unchanged

[Wenda302]

It appears that you were considering Im 1 = \<i> or Im 7 = 7 * \<i> in Isabelle, Albert :-)

Wait is this not true?

As both 1 and 7 are real numbers, their imaginary parts are zeros:Im 1 = Im 7 = 0...

[albertqjiang]

It appears that you were considering Im 1 = \<i> or Im 7 = 7 * \<i> in Isabelle, Albert :-)

Wait is this not true?

As both 1 and 7 are real numbers, their imaginary parts are zeros:Im 1 = Im 7 = 0...

Ah I see. So Im and Re are functions and not constructors of complex numbers....

[DyeKuu]

Hey @Wenda302 @albertqjiang , mathd_algebra_17 is reported as add the assumption 1 + a > 0.. I found that it's bcs in lean version there is real.sqrt (1+a) in it. and real.sqrt is truncated to 0 for negative number so that should be fine in lean. Don't know what's the case for Isabelle?

[Wenda302]

Hmm, I think Lean is handling this better. In Isabelle, we have sqrt (-(2::real)) = - sqrt 2:-(

In this case, it is probably safer to add this extra assumption to the Isabelle version. I will PR.