l3lab/ntp-mathlib-instruct-context download history

l3lab/ntp-mathlib-instruct-context is a dataset on the Hugging Face Hub. In the last 30 days it was downloaded 99 times (34 in the last 7 days), and 2,452 times in total. It ranks #114,681 among datasets by monthly downloads.

miniCTX: Neural Theorem Proving with (Long-)Contexts Lean 4 tactic prediction examples extracted from Mathlib. Examples contain: prompt: instruction, preceding file content, proof state instruction, proof state completion: tactic The file content has been truncated to 1024 tokens.

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

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