Create README.md

README.md

@@ -0,0 +1,14 @@
+
+### 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). 
+