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

[home](https://md.research.elamur.ai/free/en/) / [authors](https://md.research.elamur.ai/free/en/authors/) / [Amaury Hayat](https://md.research.elamur.ai/free/en/authors/amaury-hayat/) / cited by

# Who cites Amaury Hayat

134 citations of their works from 130 papers of our library (of the 149,439 whose bibliographies we read) · 77 with a page here, the most cited first · [← Amaury Hayat](https://md.research.elamur.ai/free/en/authors/amaury-hayat/)

1. **[Mathematical Capabilities of ChatGPT](https://md.research.elamur.ai/free/en/papers/frieder-2023-mathematical-capabilities-chatgpt/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Simon Frieder, Luca Pinchetti, Alexis Chevalier, et al.*2023 · 449 citations*
2. **[Tool Learning with Foundation Models](https://md.research.elamur.ai/free/en/papers/qin-2023-tool-learning-foundation-models/) [ACM Computing Surveys](https://md.research.elamur.ai/free/en/venues/acm-computing-surveys/)**Yujia Qin, Shengding Hu, Yankai Lin, et al.*2023 · 383 citations*
3. [**Augmented Language Models: a Survey arXiv:2302.07842**Grégoire Mialon, Roberto Dessì, Maria Lomeli, et al.*2023 · 369 citations*](https://md.research.elamur.ai/free/en/papers/mialon-2023-augmented-language-models-survey/)
4. [**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/)
5. **[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*
6. [**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/)
7. [**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/)
8. **[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*
9. [**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/)
10. [**Progressive-Hint Prompting Improves Reasoning in Large Language Models arXiv:2304.09797**Chuanyang Zheng, Zhengying Liu, Enze Xie, et al.*2023 · 131 citations*](https://md.research.elamur.ai/free/en/papers/zheng-2023-progressive-hint-prompting-improves-reasoning/)
11. [**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/)
12. [**The Alignment Problem from a Deep Learning Perspective arXiv:2209.00626**Richard Ngo, Lawrence Chan, Soren Mindermann*2022 · 121 citations*](https://md.research.elamur.ai/free/en/papers/ngo-2022-alignment-problem-deep-learning-perspective/)
13. [**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/)
14. [**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/)
15. **[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*
16. [**Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning arXiv:2504.11354**Haiming Wang, Mert Unsal, Xiaohan Lin, et al.*2025 · 92 citations*](https://md.research.elamur.ai/free/en/papers/wang-2025-kimina-prover-preview-large-formal/)
17. [**Better & Faster Large Language Models via Multi-token Prediction arXiv:2404.19737**Fabian Gloeckle, Badr Youbi Idrissi, Baptiste Roziere, et al.*2024 · 90 citations*](https://md.research.elamur.ai/free/en/papers/gloeckle-2024-better-faster-large-language-models/)
18. [**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/)
19. [**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/)
20. [**Proof Artifact Co-training for Theorem Proving with Language Models arXiv:2102.06203**Jesse Michael Han, Jason Rute, Yuhuai Wu, et al.*2021 · 82 citations*](https://md.research.elamur.ai/free/en/papers/han-2021-proof-artifact-co-training-theorem/)
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. [**From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models arXiv:2406.16838**Sean Welleck, Amanda Bertsch, Matthew Finlayson, et al.*2024 · 51 citations*](https://md.research.elamur.ai/free/en/papers/welleck-2024-decoding-meta-generation-inference-time/)
24. [**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/)
25. **[TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://md.research.elamur.ai/free/en/papers/wang-2024-theoremllama-transforming-general-purpose-llms/) [Conference on Empirical Methods in Natural Language Processing (EMNLP)](https://md.research.elamur.ai/free/en/venues/emnlp/)**Ruida Wang, Jipeng Zhang, Yizhen Jia, et al.*2024 · 51 citations*
26. **[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*
27. [**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/)
28. [**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/)
29. [**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/)
30. [**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/)
31. [**IsarStep: a Benchmark for High-level Mathematical Reasoning arXiv:2006.09265**Wenda Li, Lei Yu, Yuhuai Wu, et al.*2020 · 43 citations*](https://md.research.elamur.ai/free/en/papers/li-2020-isarstep-benchmark-high-level-mathematical/)
32. **[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*
33. [**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/)
34. [**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/)
35. [**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/)
36. [**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/)
37. **[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*
38. [**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/)
39. [**Deep Symbolic Regression for Recurrent Sequences arXiv:2201.04600**Stéphane d'Ascoli, Pierre-Alexandre Kamienny, Guillaume Lample, et al.*2022 · 27 citations*](https://md.research.elamur.ai/free/en/papers/ascoli-2022-deep-symbolic-regression-recurrent-sequences/)
40. [**End-to-end symbolic regression with transformers arXiv:2204.10532**Pierre-Alexandre Kamienny, Stéphane d'Ascoli, Guillaume Lample, et al.*2022 · 27 citations*](https://md.research.elamur.ai/free/en/papers/kamienny-2022-end-end-symbolic-regression-transformers/)
41. [**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/)
42. **[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*
43. [**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/)
44. **[Learning Formal Mathematics From Intrinsic Motivation](https://md.research.elamur.ai/free/en/papers/poesia-2024-learning-formal-mathematics-intrinsic-motivation/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Gabriel Poesia, David Broman, Nick Haber, et al.*2024 · 23 citations*
45. [**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/)
46. **[AI4Research: A Survey of Artificial Intelligence for Scientific Research](https://md.research.elamur.ai/free/en/papers/chen-2025-ai4research-survey-artificial-intelligence/) [Science China Information Sciences](https://md.research.elamur.ai/free/en/venues/science-china-information-sciences/)**Qiguang Chen, Mingda Yang, Libo Qin, et al.*2025 · 21 citations*
47. [**Leanabell-Prover: Posttraining Scaling in Formal Reasoning arXiv:2504.06122**Jingyuan Zhang, Qi Wang, Xingguang Ji, et al.*2025 · 21 citations*](https://md.research.elamur.ai/free/en/papers/zhang-2025-leanabell-prover-posttraining-scaling-formal/)
48. **[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*
49. **[Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic transformers](https://md.research.elamur.ai/free/en/papers/alfarano-2024-global-lyapunov-functions-long-standing/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Alberto Alfarano, François Charton, Amaury Hayat*2024 · 19 citations*
50. [**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/)
51. **[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*
52. [**Towards a Mathematics Formalisation Assistant using Large Language Models arXiv:2211.07524**Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, et al.*2022 · 19 citations*](https://md.research.elamur.ai/free/en/papers/agrawal-2022-mathematics-formalisation-assistant-large-language/)
53. [**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/)
54. **[APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://md.research.elamur.ai/free/en/papers/ospanov-2025-apollo-automated-llm-lean-collaboration/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh*2025 · 17 citations*
55. **[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*
56. [**Mathematical exploration and discovery at scale arXiv:2511.02864**Bogdan Georgiev, Javier Gómez-Serrano, Terence Tao, et al.*2025 · 16 citations*](https://md.research.elamur.ai/free/en/papers/georgiev-2025-mathematical-exploration-discovery-scale/)
57. [**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/)
58. [**Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics arXiv:2601.14027**Junqi Liu, Zihao Zhou, Zekai Zhu, et al.*2026 · 15 citations*](https://md.research.elamur.ai/free/en/papers/liu-2026-numina-lean-agent-open-general/)
59. **[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*
60. [**DafnyBench: A Benchmark for Formal Software Verification arXiv:2406.08467**Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, et al.*2024 · 15 citations*](https://md.research.elamur.ai/free/en/papers/loughridge-2024-dafnybench-benchmark-formal-software-verification/)
61. [**Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs arXiv:2506.19923**Kaito Baba, Chaoran Liu, Shuhei Kurita, et al.*2025 · 14 citations*](https://md.research.elamur.ai/free/en/papers/baba-2025-prover-agent-agent-based-framework/)
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. [**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/)
64. [**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/)
65. [**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/)
66. [**Proposing and solving olympiad geometry with guided tree search arXiv:2412.10673**Chi Zhang, Jiajun Song, Siyu Li, et al.*2024 · 8 citations*](https://md.research.elamur.ai/free/en/papers/zhang-2024-proposing-solving-olympiad-geometry-guided/)
67. [**SNIP: Bridging Mathematical Symbolic and Numeric Realms with Unified Pre-training arXiv:2310.02227**Kazem Meidani, Parshin Shojaee, Chandan K. Reddy, et al.*2023 · 8 citations*](https://md.research.elamur.ai/free/en/papers/meidani-2023-snip-bridging-mathematical-symbolic-numeric/)
68. **[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*
69. [**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/)
70. [**A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems arXiv:2411.18872**Roozbeh Yousefzadeh, Xuenan Cao, Azim Ospanov*2024 · 7 citations*](https://md.research.elamur.ai/free/en/papers/yousefzadeh-2024-lean-dataset-international-math-olympiad/)
71. [**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/)
72. [**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/)
73. [**StepFun-Prover Preview: Let's Think and Verify Step by Step arXiv:2507.20199**Shijie Shang, Ruosi Wan, Yue Peng, et al.*2025 · 5 citations*](https://md.research.elamur.ai/free/en/papers/shang-2025-stepfun-prover-preview-let-s/)
74. [**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/)
75. **[miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward](https://md.research.elamur.ai/free/en/papers/ospanov-2025-minif2f-lean-revisited-reviewing-limitations/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh*2025 · 4 citations*
76. **[MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation](https://md.research.elamur.ai/free/en/papers/liang-2025-mps-prover-advancing-stepwise-theorem/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Zhenwen Liang, Linfeng Song, Yang Li, et al.*2025 · 4 citations*
77. **[Open Problems Solved by LLMs? A Survey of Verifiable Mathematical Discovery](https://md.research.elamur.ai/free/en/papers/tzachristas-2026-open-problems-solved-llms-survey/) [Big Picture v2: Crafting a Research Narrative](https://md.research.elamur.ai/free/en/venues/bigpicture/)**Ioannis Tzachristas, Georgios Tzachristas, Aifen Sui*2026*

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

- [← back to](https://md.research.elamur.ai/free/en/authors/amaury-hayat/) — Amaury Hayat