--- title: "Who cites Process-Driven Autoformalization — 33 citing papers" description: "33 papers of the Elamur Research library cite «Process-Driven Autoformalization in Lean 4», found in their bibliographies; the most cited first." canonical: "https://research.elamur.ai/free/en/papers/lu-2024-process-driven-autoformalization-lean-4/cited-by/" --- [Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/lu-2024-process-driven-autoformalization-lean-4/cited-by/) [home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [Process-Driven Autoformalization in Lean 4](https://md.research.elamur.ai/free/en/papers/lu-2024-process-driven-autoformalization-lean-4/) / cited by # Who cites «Process-Driven Autoformalization in Lean 4» 33 papers of our library cite it (of the 149,439 whose bibliographies we read) · 16 with a page here, the most cited first · [← back to «Process-Driven Autoformalization in Lean 4»](https://md.research.elamur.ai/free/en/papers/lu-2024-process-driven-autoformalization-lean-4/) 1. [**Formal Mathematical Reasoning: A New Frontier in AI arXiv:2412.16075**Kaiyu Yang, Gabriel Poesia, Jingxuan He, et al.*2024 · 49 citations*](https://md.research.elamur.ai/free/en/papers/yang-2024-formal-mathematical-reasoning-new-frontier/) 2. [**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/) 3. [**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/) 4. [**FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models arXiv:2505.02735**Zhouliang Yu, Ruotian Peng, Keyi Ding, et al.*2025 · 31 citations*](https://md.research.elamur.ai/free/en/papers/yu-2025-formalmath-benchmarking-formal-mathematical-reasoning/) 5. **[AutoPSV: Automated Process-Supervised Verifier](https://md.research.elamur.ai/free/en/papers/lu-2024-autopsv-automated-process-supervised-verifier/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Jianqiao Lu, Zhiyang Dou, Hongru Wang, et al.*2024 · 28 citations* 6. [**FormalAlign: Automated Alignment Evaluation for Autoformalization arXiv:2410.10135**Jianqiao Lu, Yingjia Wan, Yinya Huang, et al.*2024 · 18 citations*](https://md.research.elamur.ai/free/en/papers/lu-2024-formalalign-automated-alignment-evaluation-autoformalization/) 7. **[Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification](https://md.research.elamur.ai/free/en/papers/liu-2025-safe-enhancing-mathematical-reasoning-large/) [Annual Meeting of the Association for Computational Linguistics (ACL)](https://md.research.elamur.ai/free/en/venues/acl/)**Chengwu Liu, Ye Yuan, Yichun Yin, et al.*2025 · 17 citations* 8. **[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* 9. **[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* 10. [**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/) 11. **[Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions](https://md.research.elamur.ai/free/en/papers/zhang-2025-autoformalization-wild-assessing-llms-real/) [Conference on Empirical Methods in Natural Language Processing (EMNLP)](https://md.research.elamur.ai/free/en/venues/emnlp/)**Lan Zhang, Marco Valentino, Andre Freitas*2025 · 11 citations* 12. **[Consistent Autoformalization for Constructing Mathematical Libraries](https://md.research.elamur.ai/free/en/papers/zhang-2024-consistent-autoformalization-constructing-mathematical-libraries/) [Conference on Empirical Methods in Natural Language Processing (EMNLP)](https://md.research.elamur.ai/free/en/venues/emnlp/)**Lan Zhang, Xin Quan, Andre Freitas*2024 · 11 citations* 13. [**Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics arXiv:2510.12787**Benjamin Breen, Marco Del Tredici, Jacob McCarran, et al.*2025 · 9 citations*](https://md.research.elamur.ai/free/en/papers/breen-2025-ax-prover-deep-reasoning-agentic/) 14. **[Theorem Prover as a Judge for Synthetic Data Generation](https://md.research.elamur.ai/free/en/papers/leang-2025-theorem-prover-as-judge-synthetic/) [Annual Meeting of the Association for Computational Linguistics (ACL)](https://md.research.elamur.ai/free/en/venues/acl/)**Joshua Ong Jun Leang, Giwon Hong, Wenda Li, et al.*2025 · 9 citations* 15. [**ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization arXiv:2510.15981**Rafael Cabral, Tuan Manh Do, Xuejun Yu, et al.*2025 · 5 citations*](https://md.research.elamur.ai/free/en/papers/cabral-2025-proofflow-dependency-graph-approach-faithful/) 16. **[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* 17 more papers of our library cite it; they have no page here yet. - [← back to](https://md.research.elamur.ai/free/en/papers/lu-2024-process-driven-autoformalization-lean-4/) — Process-Driven Autoformalization in Lean 4