| ### Neural theorem proving (`ntp`) `mathlib-tactic-instruct` | |
| Model from the [neural theorem proving tutorial vII](). | |
| A deepseek-coder 1.3B model finetuned on [ntp-mathlib-tactic-instruct](https://huggingface.co/datasets/wellecks/ntp-lean-mathlib-tactic-instruct) for 3 epochs. | |
| It is specifically finetuned for Lean 4 tactic prediction given proof states. See the tutorial for code and more information. | |
| #### Performance | |
| The model achieves 29.1% (71/244) on Lean 4 MiniF2F using the standard search setting (best-first search with beam search expansions and a beam size of 32). | |