Dataset Card for DExploration-40K

Please refer to the 📺GitHub repo and 📃Paper for more details.

🔍 About

This dataset contains 301,909 single-step (Proof State, DExploration Action) pairs extracted from 39,509 DExploration trajectories. It is produced by applying exploratory transformation on the NuminaMath-Lean dataset: formal statement-proof pairs are transformed into mathematical exploration trajectories through deductive rewriting, dependency analysis, and exploratory reassembling.

Each sample represents one step in the DExploration process, where the model is given the current exploration state and must propose the next action:

• Introduce: Add a new variable or hypothesis to the exploration context.
• Deduce: Derive a new intermediate fact from the current context.
• Submit: Submit a discovered fact as the final conclusion, ending the exploration episode.

⚙️ Data Format

Each line in exploration_steps.jsonl is a JSON object representing a single-turn conversation:

{
  "conversation": [
    {
      "system": "<system prompt>",
      "input": "<user prompt with exploration state>",
      "output": "<model response with next step>"
    }
  ]
}

📄 Citation

If you find our work useful in your research, please cite:

@inproceedings{
liu2026lets,
title={Let's Explore Step by Step: Generating Provable Formal Statements with Deductive Exploration},
author={Qi Liu and Kangjie Bao and Yue Yang and Xinhao Zheng and Renqiu Xia and Qinxiang Cao and Junchi Yan},
booktitle={The Fourteenth International Conference on Learning Representations},
year={2026},
url={https://openreview.net/forum?id=Njrkeo3DiJ}
}

©️ License

This project is released under the Apache 2.0 license. See LICENSE for details.

🤝 Contributing

We welcome contributions! Please feel free to submit issues or pull requests.

📧 Contact

For questions about the paper, data, or code:

• Qi Liu: [email protected]
• Issues: GitHub Issues

👍 Acknowledgments

• NuminaMath-LEAN for the high-quality statement-proof data.
• Goedel-Prover for the base model.
• Pantograph for Lean 4 interaction.
• And many other open-source projects!