search

lean-dojo / ReProver

Retrieval-Augmented Theorem Provers for Lean
https://leandojo.org
MIT License
229 stars 53 forks source link

Checkpoints #64

Closed Adarsh321123 closed 3 months ago

Adarsh321123 commented 4 months ago

What are the most recent model checkpoints for retrieving premises and generating tactics? I was using https://huggingface.co/kaiyuy/leandojo-pl-ckpts, but it seems to have been deleted from HuggingFace.

yangky11 commented 4 months ago

We no longer need leandojo-pl-ckpts since the model checkpoints are available in the Hugging Face format. If you need models in the PyTorch Lightning format, you can use the tricks here.