Please refer to the 📺GitHub repo and 📃Paper for more details.
DExplorer-8B is a Lean 4-based agent that generates provable formal mathematical statements through step-by-step Deductive Exploration (DExploration). Instead of directly synthesizing problems in one shot, DExplorer explores the mathematical world step by step — introducing variables/hypotheses, deriving intermediate facts, and submitting conclusions — with each step verified by the Lean 4 kernel. This ensures the provability of generated statements while enabling the synthesis of complex problems that push the limits of state-of-the-art provers.
This model is fine-tuned from Goedel-Prover-V2-8B on DExploration-40K using supervised fine-tuning.
This model is SFTed for the DExploration task: given the current exploration state (introduced variables/hypotheses and Lean 4 context), the model proposes the next exploration step — either introducing a new variable/hypothesis, deriving a new fact, or submitting a conclusion.
See the 📺GitHub repo for prompt templates and detailed usage.
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}
}
This project is released under the Apache 2.0 license. See LICENSE for details.
We welcome contributions! Please feel free to submit issues or pull requests.
For questions about the paper, data, or code:
Please refer to the 📺GitHub repo and 📃Paper for more details.
DExplorer-8B is a Lean 4-based agent that generates provable formal mathematical statements through step-by-step Deductive Exploration (DExploration). Instead of directly synthesizing problems in one shot, DExplorer explores the mathematical world step by step — introducing variables/hypotheses, deriving intermediate facts, and submitting conclusions — with each step verified by the Lean 4 kernel. This ensures the provability of generated statements while enabling the synthesis of complex problems that push the limits of state-of-the-art provers.
This model is fine-tuned from Goedel-Prover-V2-8B on DExploration-40K using supervised fine-tuning.
This model is SFTed for the DExploration task: given the current exploration state (introduced variables/hypotheses and Lean 4 context), the model proposes the next exploration step — either introducing a new variable/hypothesis, deriving a new fact, or submitting a conclusion.
See the 📺GitHub repo for prompt templates and detailed usage.
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}
}
This project is released under the Apache 2.0 license. See LICENSE for details.
We welcome contributions! Please feel free to submit issues or pull requests.
For questions about the paper, data, or code: