Reproducing LEGO Prover

Stream: Machine Learning for Theorem Proving

[Hank]

Has anyone reproduced the results of LEGO Prover? Its evaluation asks the system to solve MiniF2F problems 50 times each, and the database of lemmas for retrieval will grow gradually. However, since it uses GPT 3.5 turbo and OpenAI Ada embeddings, running one evaluation is estimated to cost 150 dollars, which is quite expensive. So if anyone who has reproduced the evaluation is willing to share the checkpoints of lemma databases, that would be super helpful!

I wrote an issue about this on LEGO Prover's official github repository but did not get replies. The authors also did not seem to reply to emails. That is why I am asking here.