Downloads · 30 days
22
26% of all-time downloads
purewhite42/DExplorer-8B
DExplorer-8B is a text generation model from purewhite42. Use it when you need the model to write or continue text. It is set up for transformers. The card lists the license as apache-2.0.
<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;…
Downloads · 30 days
22
26% of all-time downloads
All-time downloads
86
Public
Repo size
16.4 GB
Likes
0
Public
Click a slice to open those files.
.bin16.4 GB · 100%
From the Hugging Face model README
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: