`imo_2001_p6` is said to be buggy in HTPS paper

[fzyzcjy]

Hi, I see https://arxiv.org/abs/2205.11491 (written by you? ;) ) mentioning that:

... the statement is erroneous. The hypothesis h4 : b + d − a + c actually represents max(b + d − a, 0) + c. This is due to Lean’s nat type behaviour where (a : N) − (b : N) = (0 : N) if b ≥ a...

I have checked

miniF2F/lean/src/test.lean

Line 1483 in 5271dde

theorem imo_2001_p6

and seems that it has not been updated. Thus, I guess maybe the minif2f dataset should be fixed?

[DyeKuu]

A similar bug involving natural numbers is also reported here openai/miniF2F#125

I found that probably this repo is not actively merging pull-request. Maybe I am wrong.

[fzyzcjy]

I found that probably this repo is not actively merging pull-request.

I think so :(