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

[fzyzcjy]

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]

@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.