search

openai / lean-gym

Apache License 2.0
167 stars 30 forks source link

Having trouble init_search miniF2F proofs #32

Closed Some-random closed 1 year ago

Some-random commented 1 year ago

I followed the instructions given in the README document, using the theorem int.prime.dvd_mul as a test case, and everything worked as expected. However, when I tried to replace 'int.prime.dvd_mul' with mathd_algebra_141 - a theorem from the miniF2F collection, the system returned the following error message:

"{"error":"not_a_theorem: name=mathd_algebra_141 open_ns=","proof_steps":[],"search_id":null,"tactic_state":null,"tactic_state_id":null}"

As my experience with Lean is rather limited, I'm finding it challenging to pinpoint and resolve the issue. I'd greatly appreciate any assistance or direction you could provide to help me navigate this hurdle.

image

wiio12 commented 1 year ago

Hi @Some-random, sorry for the late reply. Have you tried to run the scripts/setup_miniF2F.sh script? This will complete the setup for miniF2F.

Some-random commented 1 year ago

Hi @wiio12 , thanks for the help. I've managed to load miniF2F theorems!