---
title: "Who cites Jason Rute — 108 papers of our library"
description: "108 papers of the Elamur Research library cite the works of Jason Rute, found in their bibliographies; the most cited first."
canonical: "https://research.elamur.ai/free/en/authors/jason-rute/cited-by/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/authors/jason-rute/cited-by/)

[home](https://md.research.elamur.ai/free/en/) / [authors](https://md.research.elamur.ai/free/en/authors/) / [Jason Rute](https://md.research.elamur.ai/free/en/authors/jason-rute/) / cited by

# Who cites Jason Rute

121 citations of their works from 108 papers of our library (of the 149,439 whose bibliographies we read) · 73 with a page here, the most cited first · [← Jason Rute](https://md.research.elamur.ai/free/en/authors/jason-rute/)

1. [**On the Opportunities and Risks of Foundation Models arXiv:2108.07258**Rishi Bommasani, Drew A. Hudson, Ehsan Adeli, et al.*2021 · 3,160 citations*](https://md.research.elamur.ai/free/en/papers/bommasani-2021-opportunities-risks-foundation-models/)
2. **[Solving Quantitative Reasoning Problems with Language Models](https://md.research.elamur.ai/free/en/papers/lewkowycz-2022-solving-quantitative-reasoning-problems-language/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Aitor Lewkowycz, Anders Andreassen, David Dohan, et al.*2022 · 992 citations*
3. [**Llemma: An Open Language Model For Mathematics arXiv:2310.10631**Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, et al.*2023 · 286 citations*](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-llemma-open-language-model-mathematics/)
4. **[Large Language Models for Mathematical Reasoning: Progresses and Challenges](https://md.research.elamur.ai/free/en/papers/ahn-2024-large-language-models-mathematical-reasoning/) [Conference of the European Chapter of the Association for Computational Linguistics (EACL)](https://md.research.elamur.ai/free/en/venues/eacl/)**Janice Ahn, Rishu Verma, Renze Lou, et al.*2024 · 280 citations*
5. [**MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics arXiv:2109.00110**Kunhao Zheng, Jesse Michael Han, Stanislas Polu*2021 · 257 citations*](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/)
6. **[LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Kaiyu Yang, Aidan M. Swope, Alex Gu, et al.*2023 · 253 citations*
7. **[The Lean mathematical library](https://md.research.elamur.ai/free/en/papers/community-2019-lean-mathematical-library/) [ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)](https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/)**The mathlib Community*2019 · 249 citations*
8. [**Autoformalization with Large Language Models arXiv:2205.12615**Yuhuai Wu, Albert Q. Jiang, Wenda Li, et al.*2022 · 204 citations*](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/)
9. **[LILA: A Unified Benchmark for Mathematical Reasoning](https://md.research.elamur.ai/free/en/papers/mishra-2022-lila-unified-benchmark-mathematical-reasoning/) [Conference on Empirical Methods in Natural Language Processing (EMNLP)](https://md.research.elamur.ai/free/en/venues/emnlp/)**Swaroop Mishra, Matthew Finlayson, Pan Lu, et al.*2022 · 179 citations*
10. [**Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs arXiv:2210.12283**Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, et al.*2022 · 178 citations*](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/)
11. [**Baldur: Whole-Proof Generation and Repair with Large Language Models arXiv:2303.04910**Emily First, Markus N. Rabe, Talia Ringer, et al.*2023 · 175 citations*](https://md.research.elamur.ai/free/en/papers/first-2023-baldur-whole-proof-generation-repair/)
12. **[HyperTree Proof Search for Neural Theorem Proving](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, et al.*2022 · 151 citations*
13. [**ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics arXiv:2302.12433**Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, et al.*2023 · 142 citations*](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/)
14. **[Deep Network Guided Proof Search](https://md.research.elamur.ai/free/en/papers/loos-2017-deep-network-guided-proof-search/) [EPiC series in computing](https://md.research.elamur.ai/free/en/venues/epic-series-in-computing/)**Sarah Loos, Geoffrey Irving, Christian Szegedy, et al.*2017 · 139 citations*
15. [**Formal Mathematics Statement Curriculum Learning arXiv:2202.01344**Stanislas Polu, Jesse Michael Han, Kunhao Zheng, et al.*2022 · 133 citations*](https://md.research.elamur.ai/free/en/papers/polu-2022-formal-mathematics-statement-curriculum-learning/)
16. [**DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data arXiv:2405.14333**Huajian Xin, Daya Guo, Zhihong Shao, et al.*2024 · 111 citations*](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-advancing-theorem-proving/)
17. [**Premise Selection for Theorem Proving by Deep Graph Embedding arXiv:1709.09994**Mingzhe Wang, Yihe Tang, Jian Wang, et al.*2017 · 106 citations*](https://md.research.elamur.ai/free/en/papers/wang-2017-premise-selection-theorem-proving-deep/)
18. **[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*
19. [**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/)
20. [**Learning to Prove Theorems via Interacting with Proof Assistants arXiv:1905.09381**Kaiyu Yang, Jia Deng*2019 · 90 citations*](https://md.research.elamur.ai/free/en/papers/yang-2019-learning-prove-theorems-interacting-proof/)
21. **[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/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Huaiyuan Ying, Zijian Wu, Yihan Geng, et al.*2024 · 80 citations*
22. [**LEGO-Prover: Neural Theorem Proving with Growing Libraries arXiv:2310.00656**Haiming Wang, Huajian Xin, Chuanyang Zheng, et al.*2023 · 79 citations*](https://md.research.elamur.ai/free/en/papers/wang-2023-lego-prover-neural-theorem-proving/)
23. [**Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers arXiv:2205.10893**Albert Q. Jiang, Wenda Li, Szymon Tworkowski, et al.*2022 · 79 citations*](https://md.research.elamur.ai/free/en/papers/jiang-2022-thor-wielding-hammers-integrate-language/)
24. [**HOList: An Environment for Machine Learning of Higher-Order Theorem Proving arXiv:1904.03241**Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, et al.*2019 · 78 citations*](https://md.research.elamur.ai/free/en/papers/bansal-2019-holist-environment-machine-learning-higher/)
25. **[First Experiments with Neural Translation of Informal to Formal Mathematics](https://md.research.elamur.ai/free/en/papers/wang-2018-first-experiments-neural-translation-informal/) [Lecture notes in computer science](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/)**Qingxiang Wang, Cezary Kaliszyk, Josef Urban*2018 · 66 citations*
26. **[NaturalProver: Grounded Mathematical Proof Generation with Language Models](https://md.research.elamur.ai/free/en/papers/welleck-2022-naturalprover-grounded-mathematical-proof-generation/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Sean Welleck, Jiacheng Liu, Ximing Lu, et al.*2022 · 62 citations*
27. [**FIMO: A Challenge Formal Dataset for Automated Theorem Proving arXiv:2309.04295**Chengwu Liu, Jianhao Shen, Huajian Xin, et al.*2023 · 53 citations*](https://md.research.elamur.ai/free/en/papers/liu-2023-fimo-challenge-formal-dataset-automated/)
28. [**Lean-STaR: Learning to Interleave Thinking and Proving arXiv:2407.10040**Haohan Lin, Zhiqing Sun, Sean Welleck, et al.*2024 · 51 citations*](https://md.research.elamur.ai/free/en/papers/lin-2024-lean-star-learning-interleave-thinking/)
29. **[BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://md.research.elamur.ai/free/en/papers/xin-2025-bfs-prover-scalable-best-first/) [Annual Meeting of the Association for Computational Linguistics (ACL)](https://md.research.elamur.ai/free/en/venues/acl/)**Ran Xin, Chenguang Xi, Jie Yang, et al.*2025 · 49 citations*
30. [**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/)
31. **[Formalising perfectoid spaces](https://md.research.elamur.ai/free/en/papers/buzzard-2019-formalising-perfectoid-spaces/) [ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)](https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/)**Kevin Buzzard, Johan Commelin, Patrick Massot*2019 · 48 citations*
32. [**HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving arXiv:1703.00426**Cezary Kaliszyk, François Chollet, Christian Szegedy*2017 · 48 citations*](https://md.research.elamur.ai/free/en/papers/kaliszyk-2017-holstep-machine-learning-dataset-higher/)
33. [**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/)
34. [**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/)
35. [**INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving arXiv:2007.02924**Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba, et al.*2020 · 41 citations*](https://md.research.elamur.ai/free/en/papers/wu-2020-int-inequality-benchmark-evaluating-generalization/)
36. **[DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function](https://md.research.elamur.ai/free/en/papers/wang-2023-dt-solver-automated-theorem-proving/) [Annual Meeting of the Association for Computational Linguistics (ACL)](https://md.research.elamur.ai/free/en/venues/acl/)**Haiming Wang, Ye Yuan, Zhengying Liu, et al.*2023 · 40 citations*
37. [**Evaluating Language Models for Mathematics through Interactions arXiv:2306.01694**Katherine M. Collins, Albert Q. Jiang, Simon Frieder, et al.*2023 · 40 citations*](https://md.research.elamur.ai/free/en/papers/collins-2023-evaluating-language-models-mathematics-through/)
38. [**Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean arXiv:2404.12534**Peiyang Song, Kaiyu Yang, Anima Anandkumar*2024 · 39 citations*](https://md.research.elamur.ai/free/en/papers/song-2024-lean-copilot-large-language-models/)
39. [**Learning to Reason in Large Theories without Imitation arXiv:1905.10501**Kshitij Bansal, Christian Szegedy, Markus N. Rabe, et al.*2019 · 36 citations*](https://md.research.elamur.ai/free/en/papers/bansal-2019-learning-reason-large-theories-without/)
40. [**Magnushammer: A Transformer-Based Approach to Premise Selection arXiv:2303.04488**Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, et al.*2023 · 35 citations*](https://md.research.elamur.ai/free/en/papers/mikula-2023-magnushammer-transformer-based-approach-premise/)
41. [**Process-Driven Autoformalization in Lean 4 arXiv:2406.01940**Jianqiao Lu, Yingjia Wan, Zhengying Liu, et al.*2024 · 33 citations*](https://md.research.elamur.ai/free/en/papers/lu-2024-process-driven-autoformalization-lean-4/)
42. **[Graph Representations for Higher-Order Logic and Theorem Proving](https://md.research.elamur.ai/free/en/papers/paliwal-2019-graph-representations-higher-order-logic/) [Proceedings of the AAAI Conference on Artificial Intelligence](https://md.research.elamur.ai/free/en/venues/proceedings-of-the-aaai-conference-on-artificial-intelligence/)**Aditya Paliwal, Sarah Loos, Markus Rabe, et al.*2019 · 33 citations*
43. [**Linear algebra with transformers arXiv:2112.01898**François Charton*2021 · 31 citations*](https://md.research.elamur.ai/free/en/papers/charton-2021-linear-algebra-transformers/)
44. **[Aristotle: IMO-level Automated Theorem Proving](https://md.research.elamur.ai/free/en/papers/achim-2025-aristotle-imo-level-automated-theorem/) [SuperIntelligence - Robotics - Safety & Alignment](https://md.research.elamur.ai/free/en/venues/superintelligence-robotics-safety-alignment/)**Tudor Achim, Alex Best, Alberto Bietti, et al.*2025 · 29 citations*
45. [**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/)
46. [**Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving arXiv:2305.16366**Xueliang Zhao, Wenda Li, Lingpeng Kong*2023 · 29 citations*](https://md.research.elamur.ai/free/en/papers/zhao-2023-decomposing-enigma-subgoal-based-demonstration/)
47. [**PaMpeR: Proof Method Recommendation System for Isabelle/HOL arXiv:1806.07239**Yutaka Nagashima, Yilun He*2018 · 29 citations*](https://md.research.elamur.ai/free/en/papers/nagashima-2018-pamper-proof-method-recommendation-system/)
48. [**Lyra: Orchestrating Dual Correction in Automated Theorem Proving arXiv:2309.15806**Chuanyang Zheng, Haiming Wang, Enze Xie, et al.*2023 · 24 citations*](https://md.research.elamur.ai/free/en/papers/zheng-2023-lyra-orchestrating-dual-correction-automated/)
49. [**TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning arXiv:2102.09756**Minchao Wu, Michael Norrish, Christian Walder, et al.*2021 · 24 citations*](https://md.research.elamur.ai/free/en/papers/wu-2021-tacticzero-learning-prove-theorems-scratch/)
50. [**Autoformalizing Euclidean Geometry arXiv:2405.17216**Logan Murphy, Kaiyu Yang, Jialiang Sun, et al.*2024 · 23 citations*](https://md.research.elamur.ai/free/en/papers/murphy-2024-autoformalizing-euclidean-geometry/)
51. [**LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover arXiv:2407.17227**Zijian Wu, Jiayu Wang, Dahua Lin, et al.*2024 · 23 citations*](https://md.research.elamur.ai/free/en/papers/wu-2024-lean-github-compiling-github-lean/)
52. [**LeanReasoner: Boosting Complex Logical Reasoning with Lean arXiv:2403.13312**Dongwei Jiang, Marcio Fonseca, Shay B. Cohen*2024 · 22 citations*](https://md.research.elamur.ai/free/en/papers/jiang-2024-leanreasoner-boosting-complex-logical-reasoning/)
53. [**LLMSTEP: LLM proofstep suggestions in Lean arXiv:2310.18457**Sean Welleck, Rahul Saha*2023 · 22 citations*](https://md.research.elamur.ai/free/en/papers/welleck-2023-llmstep-llm-proofstep-suggestions-lean/)
54. **[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*
55. **[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*
56. [**Graph2Tac: Online Representation Learning of Formal Math Concepts arXiv:2401.02949**Lasse Blaauwbroek, Miroslav Olšák, Jason Rute, et al.*2024 · 19 citations*](https://md.research.elamur.ai/free/en/papers/blaauwbroek-2024-graph2tac-online-representation-learning-formal/)
57. **[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*
58. **[Machine learning and information theory concepts towards an AI Mathematician](https://md.research.elamur.ai/free/en/papers/bengio-2024-machine-learning-information-theory-concepts/) [Bulletin of the American Mathematical Society](https://md.research.elamur.ai/free/en/venues/bulletin-of-the-american-mathematical-society/)**Yoshua Bengio, Nikolay Malkin*2024 · 18 citations*
59. [**miniCTX: Neural Theorem Proving with (Long-)Contexts arXiv:2408.03350**Jiewen Hu, Thomas Zhu, Sean Welleck*2024 · 18 citations*](https://md.research.elamur.ai/free/en/papers/hu-2024-minictx-neural-theorem-proving-long/)
60. **[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*
61. [**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/)
62. **[Proving Olympiad Algebraic Inequalities without Human Demonstrations](https://md.research.elamur.ai/free/en/papers/wei-2024-proving-olympiad-algebraic-inequalities-without/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Chenrui Wei, Mengzhou Sun, Wei Wang*2024 · 12 citations*
63. [**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/)
64. [**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/)
65. **[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*
66. [**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/)
67. **[Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models](https://md.research.elamur.ai/free/en/papers/cao-2025-reviving-dsp-advanced-theorem-proving/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Chenrui Cao, Liangcheng Song, Zenan Li, et al.*2025 · 7 citations*
68. [**Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers arXiv:2509.06493**Ran Xin, Zeyu Zheng, Yanchen Nie, et al.*2025 · 7 citations*](https://md.research.elamur.ai/free/en/papers/xin-2025-scaling-up-multi-turn-off/)
69. [**A New Approach Towards Autoformalization arXiv:2310.07957**Nilay Patel, Rahul Saha, Jeffrey Flanigan*2023 · 7 citations*](https://md.research.elamur.ai/free/en/papers/patel-2023-new-approach-towards-autoformalization/)
70. [**Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving arXiv:2507.02726**Matthieu Zimmer, Xiaotong Ji, Rasul Tutunov, et al.*2025 · 5 citations*](https://md.research.elamur.ai/free/en/papers/zimmer-2025-bourbaki-self-generated-goal-conditioned/)
71. [**Premise Selection for a Lean Hammer arXiv:2506.07477**Thomas Zhu, Joshua Clune, Jeremy Avigad, et al.*2025 · 5 citations*](https://md.research.elamur.ai/free/en/papers/zhu-2025-premise-selection-lean-hammer/)
72. [**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/)
73. [**ImProver: Agent-Based Automated Proof Optimization arXiv:2410.04753**Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, et al.*2024 · 5 citations*](https://md.research.elamur.ai/free/en/papers/ahuja-2024-improver-agent-based-automated-proof/)

35 more citing papers of our library have no page here yet.

- [← back to](https://md.research.elamur.ai/free/en/authors/jason-rute/) — Jason Rute