search

openai / lean-gym

Apache License 2.0
167 stars 30 forks source link

strengthen `validate_proof` #14

Closed jesse-michael-han closed 3 years ago

jesse-michael-han commented 3 years ago

h/t Mario for suggesting this solution on the Lean Zulip: link

spolu commented 3 years ago

LGTM

spolu commented 3 years ago

(confirmed it fixes the issue we identified while preserving behavior on previous situations we worked on in the past)