l3lab/ntp-mathlib
miniCTX: Neural Theorem Proving with (Long-)Contexts Lean 4 tactic prediction examples extracted from Mathlib. These examples have not been formatted for instruction tuning (including data splits). Please see l3lab/ntp-mathlib-instruct-* for datasets with instruction tuning examples. Version Generated using ntptoolkit's ntp-training-data. It used the following config for ntp-training-data: { "repo": "https://github.com/leanprover-community/mathlib4"… See the full description on the dataset page: https://huggingface.co/datasets/l3lab/ntp-mathlib.
Conversations for this repository live on Hugging Face.
Team Ai shows imported repositories read-only. Posting into someone else’s repository from here would need an authorised integration and the account holder’s consent, so the link goes to the source instead.
Open discussions on Hugging Face