Jiangwei Yu

> Have you solved this problem? I encountered it, too.

> They have removed the model now and we don't have access anymore. I did train a separate GPT based model on lean. Feel free to use this. 😀 >...

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