| This is a CodeLlama-7b model fine-tuned on [LeanDojo Benchmark](https://github.com/lean-dojo/LeanDojo) | |
| The performance is comparable with the paper [Temperature-scaled large language models for Lean proofstep prediction](https://mathai2023.github.io/papers/25.pdf) with around 57.7 pass@1 accuracy on LeanDojo "random" benchmark. | |
| The training lines are formatted as follow: | |
| ``` | |
| GOAL $(tactic state) PROOFSTEP $(tactic) | |
| ``` | |
| For inference, use the following line: | |
| ``` | |
| GOAL $(tactic state) PROOFSTEP | |
| ``` |