Mechanism

Extracts (proof_state, premise_context) -> tactic pairs (or whole-proof generation with natural-language informal sketch comments) from formal theorem provers (Lean 4, Isabelle/HOL, Coq) and fine-tunes the LLM to emit formally valid tactics or complete formal proofs.

Practical Notes

Serves as the cold-start foundation before expert iteration and RLVR against the Lean 4 kernel.

References

  1. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models ↗

    Yang, Kaiyu, Swope, Aidan M., Gu, Alex, Chalamala, Rahul, Song, Peiyang, Yu, Shixing et al. · 2023

    All 9 authors

    Yang, Kaiyu, Swope, Aidan M., Gu, Alex, Chalamala, Rahul, Song, Peiyang, Yu, Shixing, Godil, Saad, Prenger, Ryan, Anandkumar, Anima

  2. DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search ↗

    Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang et al. · 2024

    All 17 authors

    Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, Chong Ruan

  3. DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition ↗

    Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao et al. · 2025

    All 18 authors

    Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, Chong Ruan