search

openai / miniF2F

Formal to Formal Mathematics Benchmark
309 stars 43 forks source link

Lean aime_1988_p8 #47

Closed TJ-Machado closed 3 years ago

TJ-Machado commented 3 years ago

There appears to be a typo in the statement of aime_1988_p8 in test.lean. Namely, h₂ is stated as ∀ x y, f x y = y * (f x (x + y)) which I believe should instead by ∀ x y, (x + y) * f x y = y * (f x (x + y)) as indicated by the problem statement in metamath/test/aime-1988-p8.mm.

DyeKuu commented 3 years ago

you're correct, that's also what the original statement looks like (cf https://artofproblemsolving.com/wiki/index.php/1988_AIME_Problems/Problem_8). Thanks for spotting this.