--- title: "Who cites Lean Workbook: A large-scale — 74 citing papers" description: "74 papers of the Elamur Research library cite «Lean Workbook: A large-scale Lean problem set formalized from natural language math…" canonical: "https://research.elamur.ai/free/en/papers/ying-2024-lean-workbook-large-scale-lean/cited-by/" --- [Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/ying-2024-lean-workbook-large-scale-lean/cited-by/) [home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [Lean Workbook: A large-scale Lean problem set…](https://md.research.elamur.ai/free/en/papers/ying-2024-lean-workbook-large-scale-lean/) / cited by # Who cites «Lean Workbook: A large-scale Lean problem set formalized from natural language math problems» 74 papers of our library cite it (of the 149,439 whose bibliographies we read) · 15 with a page here, the most cited first · [← back to «Lean Workbook: A large-scale Lean problem set formalized from natural language math problems»](https://md.research.elamur.ai/free/en/papers/ying-2024-lean-workbook-large-scale-lean/) 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. **[MathArena: Evaluating LLMs on Uncontaminated Math Competitions](https://md.research.elamur.ai/free/en/papers/balunovic-2025-matharena-evaluating-llms-uncontaminated-math/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Mislav Balunović, Jasper Dekoninck, Ivo Petrov, et al.*2025 · 99 citations* 4. [**Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving arXiv:2502.07640**Yong Lin, Shange Tang, Bohan Lyu, et al.*2025 · 84 citations*](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-frontier-model-open/) 5. [**HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving arXiv:2412.20735**Yang Li, Dong Du, Linfeng Song, et al.*2024 · 25 citations*](https://md.research.elamur.ai/free/en/papers/li-2024-hunyuanprover-scalable-data-synthesis/) 6. **[Chain-of-Reasoning: Towards Unified Mathematical Reasoning in Large Language Models via a Multi-Paradigm Perspective](https://md.research.elamur.ai/free/en/papers/yu-2025-chain-reasoning-unified-mathematical-reasoning/) [Annual Meeting of the Association for Computational Linguistics (ACL)](https://md.research.elamur.ai/free/en/venues/acl/)**Yiyao Yu, Yuxiang Zhang, Dongdong Zhang, et al.*2025 · 23 citations* 7. [**Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience arXiv:2512.17260**Jiangjie Chen, Wenxiang Chen, Jiacheng Du, et al.*2025 · 19 citations*](https://md.research.elamur.ai/free/en/papers/chen-2025-seed-prover-1-5/) 8. [**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/) 9. **[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* 10. **[Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening](https://md.research.elamur.ai/free/en/papers/he-2025-rewarding-unlikely-lifting-grpo-beyond/) [Conference on Empirical Methods in Natural Language Processing (EMNLP)](https://md.research.elamur.ai/free/en/venues/emnlp/)**Andre Wang He, Daniel Fried, Sean Welleck*2025 · 15 citations* 11. **[CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization](https://md.research.elamur.ai/free/en/papers/peng-2026-criticlean-critic-guided-reinforcement-learning/) [Annual Meeting of the Association for Computational Linguistics (ACL)](https://md.research.elamur.ai/free/en/venues/acl/)**Zhongyuan Peng, Yifan Yao, Kaijing Ma, et al.*2026 · 12 citations* 12. [**REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning arXiv:2505.20613**Ziju Shen, Naohao Huang, Fanyi Yang, et al.*2025 · 10 citations*](https://md.research.elamur.ai/free/en/papers/shen-2025-real-prover-retrieval-augmented-lean/) 13. [**ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization arXiv:2510.24592**Guoxin Chen, Jing Wu, Xinjie Chen, et al.*2025 · 8 citations*](https://md.research.elamur.ai/free/en/papers/chen-2025-reform-reflective-autoformalization-prospective-bounded/) 14. [**StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion arXiv:2508.04440**Yutong Wu, Di Huang, Ruosi Wan, et al.*2025 · 7 citations*](https://md.research.elamur.ai/free/en/papers/wu-2025-stepfun-formalizer-unlocking-autoformalization/) 15. **[FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean](https://md.research.elamur.ai/free/en/papers/meadows-2026-formalscience-scalable-human-loop-autoformalisation/) [Annual Meeting of the Association for Computational Linguistics (ACL)](https://md.research.elamur.ai/free/en/venues/acl/)**Jordan Meadows, Lan Zhang, Andre Freitas*2026* 59 more papers of our library cite it; they have no page here yet. - [← back to](https://md.research.elamur.ai/free/en/papers/ying-2024-lean-workbook-large-scale-lean/) — Lean Workbook: A large-scale Lean problem set formalized from natural language math problems