search

openai / lean-gym

Apache License 2.0
150 stars 31 forks source link

[repl] tentatively fix dangling metavariable issue #9

Closed jesse-michael-han closed 3 years ago

jesse-michael-han commented 3 years ago

with these changes, intros, nlinarith works and passes validation for mathd_numbertheory_136

spolu commented 3 years ago

Factored some of your changes in the other PR. This one can probably be closed for now.