l3lab/ntp-mathlib-instruct-context

Dataset Overview

Dataset Name

miniCTX: Neural Theorem Proving with (Long‑)Contexts

Dataset Content

• Source: Lean 4 tactic prediction examples extracted from Mathlib.
• Example Structure:
  • prompt:
    • Contains instruction, preceding file content, proof state or instruction, proof state
  • completion: tactic
• File Content: Truncated to 1,024 tokens.

Dataset Configuration

• Configuration Name: default
• Data Files:
  • split: train, dev, test
  • path: "with_context_mathlib_only/with_context_train*", "with_context_mathlib_only/with_context_dev*", "with_context_mathlib_only/with_context_test*"

Version Information

• Generation Tools: ntptoolkit's ntp‑training‑data and instruction_tuning.py
• Configuration Details:

  {
      "repo": "https://github.com/leanprover-community/mathlib4",
      "commit": "cf8e23a62939ed7cc530fbb68e83539730f32f86",
      "lean": "leanprover/lean4:v4.4.0",
      "name": "mathlib",
      "import_file": "Mathlib.lean",
      "imports": ["Mathlib"]
  }
  

Citation

@misc{hu2024minictx, author = {Jiewen Hu and Thomas Zhu and Sean Welleck}, title = {miniCTX: Neural Theorem Proving with (Long‑)Contexts}, year = {2024}, eprint={}, archivePrefix={arXiv}, }