(Willing to PR) Support multi sub-goals, like what is done in `HyperTree Proof Search for Neural Theorem Proving`

openai / lean-gym

Apache License 2.0

167 stars 30 forks source link

(Willing to PR) Support multi sub-goals, like what is done in `HyperTree Proof Search for Neural Theorem Proving` #30

Open fzyzcjy opened 1 year ago

fzyzcjy commented 1 year ago

Hi thanks for the environment! The recent paper https://arxiv.org/abs/2205.11491 let one goal create multiple subgoals, but currently lean-gym will do something like 2 goals\ngoal-one\n\ngoal-two instead of really creating two state-ids.

So, is there a plan to implement it? Or, if I implement it, will you accept the PR?

venom12138 commented 1 year ago

@fzyzcjy Hi, I find that the "induction" tactic is invalid for lean-gym, have you encountered the same error? Here is the code and error infomation.