Update README.md

README.md

@@ -34,7 +34,7 @@ Please refer to the [📺GitHub repo](https://github.com/Purewhite2019/dexplorat
 
 **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](https://huggingface.co/Goedel-Prover/Goedel-Prover-V2-8B) on [🤗purewhite42/DExploration_Dataset](https://huggingface.co/datasets/purewhite42/DExploration_Dataset) using supervised fine-tuning.
+This model is fine-tuned from [Goedel-Prover-V2-8B](https://huggingface.co/Goedel-LM/Goedel-Prover-V2-8B) on [DExploration-40K](https://huggingface.co/datasets/purewhite42/DExploration-40K) using supervised fine-tuning.
 
 ## ⚙️ Usage
 
@@ -73,7 +73,7 @@ For questions about the paper, data, or code:
 - **Issues**: [GitHub Issues](https://github.com/Purewhite2019/dexploration_main/issues)
 
 ## 👍 Acknowledgments
-- [NuminaMath-LEAN](https://huggingface.co/AI-MO/NuminaMath-LEAN) for the high-quality statement-proof data.
+- [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!