Update README.md

README.md

@@ -1,10 +1,8 @@
 
-### Neural theorem proving (`ntp`) `mathlib-tactic-instruct`
+Model from the [neural theorem proving tutorial vII](https://github.com/cmu-l3/ntptutorial-II). 
 
-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.
+A deepseek-coder 1.3B model finetuned on [ntp-mathlib-tactic-instruct-st](https://huggingface.co/datasets/l3lab/ntp-lean-mathlib-instruct-st) for 3 epochs.
 
 It is specifically finetuned for Lean 4 tactic prediction given proof states. See the tutorial for code and more information.