search

openai / miniF2F

Formal to Formal Mathematics Benchmark
309 stars 43 forks source link

Fix to IMO 1960 p2 #50

Closed spolu closed 3 years ago

spolu commented 3 years ago

Align MM and Lean use of strict inequality.

Remove the != 0 condition which is trivial.

r? @DyeKuu

DyeKuu commented 3 years ago

LGTM