l3lab/

ntp-mathlib-instruct-st

Lean 4 tactic prediction examples extracted from Mathlib. Examples contain:

prompt: instruction, proof state

completion: tactic

Generated using ntptoolkit's ntp-training-data and instruction_tuning.py. It used the following config for ntp-training-data: { "repo": "https://github.com/leanprover-community/mathlib4", "commit": "cf8e23a62939ed7cc530fbb68e83539730f32f86", "lean":… See the full description on the dataset page: https://huggingface.co/datasets/l3lab/ntp-mathlib-instruct-st.