l3lab/

ntp-mathlib-instruct-context

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.

Generated using ntptoolkit's ntp-training-data and instruction_tuning.py. It used the following config for ntp-training-data: { "repo":… See the full description on the dataset page: https://huggingface.co/datasets/l3lab/ntp-mathlib-instruct-context.