--- title: "Who cites Lyra: Orchestrating Dual — 22 citing papers" description: "22 papers of the Elamur Research library cite «Lyra: Orchestrating Dual Correction in Automated Theorem Proving», found in their…" canonical: "https://research.elamur.ai/free/en/papers/zheng-2023-lyra-orchestrating-dual-correction-automated/cited-by/" --- [Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/zheng-2023-lyra-orchestrating-dual-correction-automated/cited-by/) [home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [Lyra: Orchestrating Dual Correction in Automated…](https://md.research.elamur.ai/free/en/papers/zheng-2023-lyra-orchestrating-dual-correction-automated/) / cited by # Who cites «Lyra: Orchestrating Dual Correction in Automated Theorem Proving» 22 papers of our library cite it (of the 149,439 whose bibliographies we read) · 17 with a page here, the most cited first · [← back to «Lyra: Orchestrating Dual Correction in Automated Theorem Proving»](https://md.research.elamur.ai/free/en/papers/zheng-2023-lyra-orchestrating-dual-correction-automated/) 1. [**DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition arXiv:2504.21801**Z. Z. Ren, Zhihong Shao, Junxiao Song, et al.*2025 · 122 citations*](https://md.research.elamur.ai/free/en/papers/ren-2025-deepseek-prover-v2-advancing-formal/) 2. [**DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search arXiv:2408.08152**Huajian Xin, Z. Z. Ren, Junxiao Song, et al.*2024 · 116 citations*](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-v1-5-harnessing/) 3. **[PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://md.research.elamur.ai/free/en/papers/tsoukalas-2024-putnambench-evaluating-neural-theorem-provers/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**George Tsoukalas, Jasper Lee, John Jennings, et al.*2024 · 93 citations* 4. [**InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning arXiv:2402.06332**Huaiyuan Ying, Shuo Zhang, Linyang Li, et al.*2024 · 90 citations*](https://md.research.elamur.ai/free/en/papers/ying-2024-internlm-math-open-math-large/) 5. [**An In-Context Learning Agent for Formal Theorem-Proving arXiv:2310.04353**Amitayush Thakur, George Tsoukalas, Yeming Wen, et al.*2023 · 47 citations*](https://md.research.elamur.ai/free/en/papers/thakur-2023-context-learning-agent-formal-theorem/) 6. [**A Survey on Deep Learning for Theorem Proving arXiv:2404.09939**Zhaoyu Li, Jialiang Sun, Logan Murphy, et al.*2024 · 46 citations*](https://md.research.elamur.ai/free/en/papers/li-2024-survey-deep-learning-theorem-proving/) 7. [**STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving arXiv:2502.00212**Kefan Dong, Tengyu Ma*2025 · 43 citations*](https://md.research.elamur.ai/free/en/papers/dong-2025-stp-self-play-llm-theorem/) 8. [**MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data arXiv:2402.08957 (ICLR 2024 spotlight)**Yinya Huang, Xiaohan Lin, Zhengying Liu, et al.*2024 · 29 citations*](https://md.research.elamur.ai/free/en/papers/huang-2024-mustard-mastering-uniform-synthesis-theorem/) 9. **[TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models](https://md.research.elamur.ai/free/en/papers/xiong-2023-trigo-benchmarking-formal-mathematical-proof/) [Conference on Empirical Methods in Natural Language Processing (EMNLP)](https://md.research.elamur.ai/free/en/venues/emnlp/)**Jing Xiong, Jianhao Shen, Ye Yuan, et al.*2023 · 21 citations* 10. **[Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://md.research.elamur.ai/free/en/papers/li-2024-autoformalize-mathematical-statements-symbolic-equivalence/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Zenan Li, Yifan Wu, Zhaoyu Li, et al.*2024 · 19 citations* 11. **[Proving Theorems Recursively](https://md.research.elamur.ai/free/en/papers/wang-2024-proving-theorems-recursively/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Haiming Wang, Huajian Xin, Zhengying Liu, et al.*2024 · 19 citations* 12. [**MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving arXiv:2503.03205**Ruida Wang, Rui Pan, Yuxin Li, et al.*2025 · 18 citations*](https://md.research.elamur.ai/free/en/papers/wang-2025-ma-lot-model-collaboration-lean/) 13. **[ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://md.research.elamur.ai/free/en/papers/liu-2025-atlas-autoformalizing-theorems-through-lifting/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, et al.*2025 · 16 citations* 14. [**Solving Formal Math Problems by Decomposition and Iterative Reflection arXiv:2507.15225**Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, et al.*2025 · 16 citations*](https://md.research.elamur.ai/free/en/papers/zhou-2025-solving-formal-math-problems-decomposition/) 15. [**Autoformalization in the Era of Large Language Models: A Survey arXiv:2505.23486**Ke Weng, Lun Du, Sirui Li, et al.*2025 · 11 citations*](https://md.research.elamur.ai/free/en/papers/weng-2025-autoformalization-era-large-language-models/) 16. [**Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning arXiv:2502.13834**Zenan Li, Zhaoyu Li, Wen Tang, et al.*2025 · 11 citations*](https://md.research.elamur.ai/free/en/papers/li-2025-proving-olympiad-inequalities-synergizing-llms/) 17. [**SubgoalXL: Subgoal-based Expert Learning for Theorem Proving arXiv:2408.11172**Xueliang Zhao, Lin Zheng, Haige Bo, et al.*2024 · 10 citations*](https://md.research.elamur.ai/free/en/papers/zhao-2024-subgoalxl-subgoal-based-expert-learning/) 5 more papers of our library cite it; they have no page here yet. - [← back to](https://md.research.elamur.ai/free/en/papers/zheng-2023-lyra-orchestrating-dual-correction-automated/) — Lyra: Orchestrating Dual Correction in Automated Theorem Proving