l3lab/

ntp-mathlib-instruct-context-fullproof

Lean 4 full proof generation examples extracted from Mathlib. Examples contain:

prompt: instruction, preceding file content

completion: proof

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": "https://github.com/leanprover-community/mathlib4", "commit":… See the full description on the dataset page: https://huggingface.co/datasets/l3lab/ntp-mathlib-instruct-context-fullproof.