l3lab/ntp-mathlib-instruct-context-fullproof

--- tags: - theorem-proving - math - lean configs: - config_name: default data_files: - split: train path: "ctx_full_proof_mathlib_only/ctx_full_proof_train*" - split: dev path: "ctx_full_proof_mathlib_only/ctx_full_proof_dev*" - split: test path: "ctx_full_proof_mathlib_only/ctx_full_proof_test*" --- ## [miniCTX: Neural Theorem Proving with (Long-)Contexts]() 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. ### Version Generated using `ntptoolkit`'s `ntp-training-data` and `instruction_tuning.py`. It used the following config for `ntp-training-data`: ```json { "repo": "https://github.com/leanprover-community/mathlib4", "commit": "cf8e23a62939ed7cc530fbb68e83539730f32f86", "lean": "leanprover/lean4:v4.4.0", "name": "mathlib", "import_file": "Mathlib.lean", "imports": ["Mathlib"] } ``` #### Citation Please cite: ``` @misc{hu2024minictx, title={miniCTX: Neural Theorem Proving with (Long-)Contexts}, author={Jiewen Hu and Thomas Zhu and Sean Welleck}, year={2024}, eprint={2408.03350}, archivePrefix={arXiv}, primaryClass={cs.AI}, url={https://arxiv.org/abs/2408.03350}, } ```