l3lab/ntp-mathlib-instruct-st download history

l3lab/ntp-mathlib-instruct-st is a dataset on the Hugging Face Hub. In the last 30 days it was downloaded 92 times (26 in the last 7 days), and 3,989 times in total. It ranks #120,876 among datasets by monthly downloads.

miniCTX: Neural Theorem Proving with (Long-)Contexts Lean 4 tactic prediction examples extracted from Mathlib. Examples contain: prompt: instruction, proof state completion: tactic Version Generated using ntptoolkit's ntp-training-data and instruction_tuning.py. It used th

Open l3lab/ntp-mathlib-instruct-st on Hugging Face

Sister project: Paper Pulse, the upvote history of every Hugging Face Daily Paper.