Create README.md

README.md

@@ -0,0 +1,26 @@
+
+Model from the [neural theorem proving tutorial vII](https://github.com/cmu-l3/ntptutorial-II). 
+
+
+A deepseek-coder 1.3B model finetuned on [ntp-mathlib-instruct-context](https://huggingface.co/datasets/l3lab/ntp-mathlib-instruct-context).
+
+It is specifically finetuned for Lean 4 tactic prediction given proof states and optional file contexts. See the tutorial for code and more information.
+
+#### Performance
+
+The model achieves 29.5% (72/244) on Lean 4 MiniF2F using the standard search setting (best-first search with beam search expansions and a beam size of 32). 
+
+
+#### Citation
+
+Until an associated preprint is available, please cite the tutorial's repository:
+```
+@misc{ntptutorialII,
+  author = {Sean Welleck},
+  title = {Neural theorem proving tutorial II},
+  year = {2024},
+  publisher = {GitHub},
+  journal = {GitHub repository},
+  howpublished = {\url{https://github.com/cmu-l3/ntptutorial-II}},
+}
+```