search

openai / miniF2F

Formal to Formal Mathematics Benchmark
309 stars 43 forks source link

Typo in theorem mathd_algebra_185? #73

Closed albertqjiang closed 2 years ago

albertqjiang commented 2 years ago

https://github.com/openai/miniF2F/blob/18b1400db731999f6501ef777fc3c8b0e2e529f3/lean/src/valid.lean#L1090

The original description of the problem is: How many integers are in the solution of the inequality $|x + 4|< 9$? Here the function f is defined as over real numbers: (f : ℝ → ℝ). I suspect that this is a typo, but I'm no lean expert. Hopefully someone can verify this.

DyeKuu commented 2 years ago

Hi @albertqjiang ! Thank you for spotting this. Just take a look at the statements and it does look like a mistake here. I will push a fix on that later.