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