purewhite42/DExploration-40K

---
license: apache-2.0
language:
- en
tags:
- formal-mathematics
- lean4
- data-synthesis
- problem-generation
- formal-statement-synthesis
task_categories:
- text-generation
pretty_name: DExploration-40K
size_categories:
- 100K<n<1M
configs:
- config_name: default
data_files:
- split: train
path:
- "exploration_steps.jsonl"
---

<div align="center">
<h1 style="font-size: 1.5em;">[ICLR'26] Let's Explore Step by Step: Generating Provable Formal Statements with Deductive Exploration</h1>
<div style="display: flex; justify-content: center; gap: 8px; flex-wrap: wrap;">
<a href="https://choosealicense.com/licenses/apache-2.0/"><img src="https://img.shields.io/badge/License-Apache%202.0-blue.svg" alt="License: Apache 2.0"></a>
<a href="https://github.com/leanprover-community/mathlib4"><img src="https://img.shields.io/badge/Lean-4-orange" alt="Lean 4"></a>
<a href="https://github.com/Purewhite2019/dexploration_main"><img src="https://img.shields.io/badge/GitHub-%23121011.svg?logo=github&logoColor=white" alt="GitHub"></a>
</div>
<h2>Qi Liu, Kangjie Bao, Yue Yang, Xinhao Zheng, Renqiu Xia, Qinxiang Cao, Junchi Yan* (* indicates corresponding author)</h2>
<h3>School of Computer Science & School of Artificial Intelligence, Shanghai Jiao Tong University</h3>
<h3>Shanghai Innovation Institute</h3>
</div>

# Dataset Card for DExploration-40K

Please refer to the [📺GitHub repo](https://github.com/Purewhite2019/dexploration_main) and
[📃Paper](https://openreview.net/pdf?id=Njrkeo3DiJ) 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](https://huggingface.co/datasets/AI-MO/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:

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

| Field | Description |
|-------|-------------|
| `system` | System prompt (role description) |
| `input` | User input (task description + proof state) |
| `output` | Model output (DExploration action) |

## 📄 Citation

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

```bibtex
@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](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**: [e-mail]
- **Issues**: [GitHub Issues](https://github.com/Purewhite2019/dexploration_main/issues)

## 👍 Acknowledgments
- [NuminaMath-LEAN](https://huggingface.co/datasets/AI-MO/NuminaMath-LEAN) for the high-quality statement-proof data.
- [Goedel-Prover](https://huggingface.co/Goedel-LM/Goedel-Prover-V2-8B) for the base model.
- [Pantograph](https://github.com/leanprover/Pantograph) for Lean 4 interaction.
- And many other open-source projects!