`imo_2001_p6` is said to be buggy in HTPS paper

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 https://github.com/facebookresearch/miniF2F/blob/5271ddec788677c815cf818a06f368ef6498a106/lean/src/test.lean#L1483 and seems that it has not been updated. Thus, I guess maybe the minif2f dataset should be fixed?