🧑‍🔬 Who cites Bartosz Piotrowski

172 citations of their works from 152 papers of our library (of the 149,439 whose bibliographies we read) · 78 with a page here, the most cited first · ← Bartosz Piotrowski

1. A Survey of Large Language ModelsFrontiers of Computer ScienceWayne Xin Zhao, Kun Zhou, Junyi Li, et al.2023 · 2,875 citations
2. Llemma: An Open Language Model For MathematicsarXiv:2310.10631Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, et al.2023 · 286 citations
3. LeanDojo: Theorem Proving with Retrieval-Augmented Language ModelsConference on Neural Information Processing Systems (NeurIPS)Kaiyu Yang, Aidan M. Swope, Alex Gu, et al.2023 · 253 citations
4. LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic ProversConference on Empirical Methods in Natural Language Processing (EMNLP)Theo X. Olausson, Alex Gu, Benjamin Lipkin, et al.2023 · 172 citations
5. Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language ModelsarXiv:2410.07985Bofei Gao, Feifan Song, Zhe Yang, et al.2024 · 163 citations
6. OpenWebMath: An Open Dataset of High-Quality Mathematical Web TextarXiv:2310.06786Keiran Paster, Marco Dos Santos, Zhangir Azerbayev, et al.2023 · 132 citations
7. DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal DecompositionarXiv:2504.21801Z. Z. Ren, Zhihong Shao, Junxiao Song, et al.2025 · 122 citations
8. DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree SearcharXiv:2408.08152Huajian Xin, Z. Z. Ren, Junxiao Song, et al.2024 · 116 citations
9. PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical CompetitionConference on Neural Information Processing Systems (NeurIPS)George Tsoukalas, Jasper Lee, John Jennings, et al.2024 · 93 citations
10. Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement LearningarXiv:2504.11354Haiming Wang, Mert Unsal, Xiaohan Lin, et al.2025 · 92 citations
11. InternLM-Math: Open Math Large Language Models Toward Verifiable ReasoningarXiv:2402.06332Huaiyuan Ying, Shuo Zhang, Linyang Li, et al.2024 · 90 citations
12. Goedel-Prover: A Frontier Model for Open-Source Automated Theorem ProvingarXiv:2502.07640Yong Lin, Shange Tang, Bohan Lyu, et al.2025 · 84 citations
13. Lean Workbook: A large-scale Lean problem set formalized from natural language math problemsConference on Neural Information Processing Systems (NeurIPS)Huaiyuan Ying, Zijian Wu, Yihan Geng, et al.2024 · 80 citations
14. LEGO-Prover: Neural Theorem Proving with Growing LibrariesarXiv:2310.00656Haiming Wang, Huajian Xin, Chuanyang Zheng, et al.2023 · 79 citations
15. Reasoning Models Can Be Effective Without ThinkingarXiv:2504.09858Wenjie Ma, Jingxuan He, Charlie Snell, et al.2025 · 58 citations
16. Lean-STaR: Learning to Interleave Thinking and ProvingarXiv:2407.10040Haohan Lin, Zhiqing Sun, Sean Welleck, et al.2024 · 51 citations
17. TheoremLlama: Transforming General-Purpose LLMs into Lean4 ExpertsConference on Empirical Methods in Natural Language Processing (EMNLP)Ruida Wang, Jipeng Zhang, Yizhen Jia, et al.2024 · 51 citations
18. Formal Mathematical Reasoning: A New Frontier in AIarXiv:2412.16075Kaiyu Yang, Gabriel Poesia, Jingxuan He, et al.2024 · 49 citations
19. MathPile: A Billion-Token-Scale Pretraining Corpus for MathConference on Neural Information Processing Systems (NeurIPS)Zengzhi Wang, Xuefeng Li, Rui Xia, et al.2023 · 49 citations
20. A Survey on Deep Learning for Theorem ProvingarXiv:2404.09939Zhaoyu Li, Jialiang Sun, Logan Murphy, et al.2024 · 46 citations
21. MathOdyssey: Benchmarking Mathematical Problem-Solving Skills in Large Language Models Using Odyssey Math DataScientific DataMeng Fang, Xiangpeng Wan, Fei Lu, et al.2024 · 46 citations
22. Don't Trust: Verify — Grounding LLM Quantitative Reasoning with AutoformalizationarXiv:2403.18120Jin Peng Zhou, Charles Staats, Wenda Li, et al.2024 · 45 citations
23. STP: Self-play LLM Theorem Provers with Iterative Conjecturing and ProvingarXiv:2502.00212Kefan Dong, Tengyu Ma2025 · 43 citations
24. IsarStep: a Benchmark for High-level Mathematical ReasoningarXiv:2006.09265Wenda Li, Lei Yu, Yuhuai Wu, et al.2020 · 43 citations
25. INT: An Inequality Benchmark for Evaluating Generalization in Theorem ProvingarXiv:2007.02924Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba, et al.2020 · 41 citations
26. Evaluating Language Models for Mathematics through InteractionsarXiv:2306.01694Katherine M. Collins, Albert Q. Jiang, Simon Frieder, et al.2023 · 40 citations
27. First Neural Conjecturing Datasets and ExperimentsLecture notes in computer scienceJosef Urban, Jan Jakubův2020 · 40 citations
28. Lean Copilot: Large Language Models as Copilots for Theorem Proving in LeanarXiv:2404.12534Peiyang Song, Kaiyu Yang, Anima Anandkumar2024 · 39 citations
29. LIME: Learning Inductive Bias for Primitives of Mathematical ReasoningarXiv:2101.06223Yuhuai Wu, Markus Rabe, Wenda Li, et al.2021 · 39 citations
30. Multilingual Mathematical AutoformalizationarXiv:2311.03755Albert Q. Jiang, Wenda Li, Mateja Jamnik2023 · 37 citations
31. Functional Benchmarks for Robust Evaluation of Reasoning Performance, and the Reasoning GaparXiv:2402.19450Saurabh Srivastava, Annarose M B, Anto P, et al.2024 · 35 citations
32. Magnushammer: A Transformer-Based Approach to Premise SelectionarXiv:2303.04488Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, et al.2023 · 35 citations
33. Herald: A Natural Language Annotated Lean 4 DatasetarXiv:2410.10878Guoxiong Gao, Yutong Wang, Jiedong Jiang, et al.2024 · 33 citations
34. Process-Driven Autoformalization in Lean 4arXiv:2406.01940Jianqiao Lu, Yingjia Wan, Zhengying Liu, et al.2024 · 33 citations
35. FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language ModelsarXiv:2505.02735Zhouliang Yu, Ruotian Peng, Keyi Ding, et al.2025 · 31 citations
36. Aristotle: IMO-level Automated Theorem ProvingSuperIntelligence - Robotics - Safety & AlignmentTudor Achim, Alex Best, Alberto Bietti, et al.2025 · 29 citations
37. Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem ProvingarXiv:2305.16366Xueliang Zhao, Wenda Li, Lingpeng Kong2023 · 29 citations
38. Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language ModelsAnnual Meeting of the Association for Computational Linguistics (ACL)Haoxiang Sun, Yingqian Min, Zhipeng Chen, et al.2026 · 25 citations
39. Lyra: Orchestrating Dual Correction in Automated Theorem ProvingarXiv:2309.15806Chuanyang Zheng, Haiming Wang, Enze Xie, et al.2023 · 24 citations
40. Autoformalizing Euclidean GeometryarXiv:2405.17216Logan Murphy, Kaiyu Yang, Jialiang Sun, et al.2024 · 23 citations
41. LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN proverarXiv:2407.17227Zijian Wu, Jiayu Wang, Dahua Lin, et al.2024 · 23 citations
42. Towards Finding Longer ProofsLecture notes in computer scienceZsolt Zombori, Adrián Csiszárik, Henryk Michalewski, et al.2019 · 21 citations
43. CombiBench: Benchmarking LLM Capability for Combinatorial MathematicsarXiv:2505.03171Junqi Liu, Xiaohan Lin, Jonas Bayer, et al.2025 · 20 citations
44. Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic ConsistencyConference on Neural Information Processing Systems (NeurIPS)Zenan Li, Yifan Wu, Zhaoyu Li, et al.2024 · 19 citations
45. Graph2Tac: Online Representation Learning of Formal Math ConceptsarXiv:2401.02949Lasse Blaauwbroek, Miroslav Olšák, Jason Rute, et al.2024 · 19 citations
46. Proving Theorems RecursivelyConference on Neural Information Processing Systems (NeurIPS)Haiming Wang, Huajian Xin, Zhengying Liu, et al.2024 · 19 citations
47. FormalAlign: Automated Alignment Evaluation for AutoformalizationarXiv:2410.10135Jianqiao Lu, Yingjia Wan, Yinya Huang, et al.2024 · 18 citations
48. miniCTX: Neural Theorem Proving with (Long-)ContextsarXiv:2408.03350Jiewen Hu, Thomas Zhu, Sean Welleck2024 · 18 citations
49. APOLLO: Automated LLM and Lean Collaboration for Advanced Formal ReasoningConference on Neural Information Processing Systems (NeurIPS)Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh2025 · 17 citations
50. ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of DataConference on Neural Information Processing Systems (NeurIPS)Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, et al.2025 · 16 citations
51. Solving Formal Math Problems by Decomposition and Iterative ReflectionarXiv:2507.15225Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, et al.2025 · 16 citations
52. Prover Agent: An Agent-Based Framework for Formal Mathematical ProofsarXiv:2506.19923Kaito Baba, Chaoran Liu, Shuhei Kurita, et al.2025 · 14 citations
53. U-MATH: A University-Level Benchmark for Evaluating Mathematical Skills in LLMsarXiv:2412.03205Konstantin Chernyshev, Vitaliy Polshkov, Ekaterina Artemova, et al.2024 · 13 citations
54. CriticLean: Critic-Guided Reinforcement Learning for Mathematical FormalizationAnnual Meeting of the Association for Computational Linguistics (ACL)Zhongyuan Peng, Yifan Yao, Kaijing Ma, et al.2026 · 12 citations
55. Autoformalization in the Era of Large Language Models: A SurveyarXiv:2505.23486Ke Weng, Lun Du, Sirui Li, et al.2025 · 11 citations
56. Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical DefinitionsConference on Empirical Methods in Natural Language Processing (EMNLP)Lan Zhang, Marco Valentino, Andre Freitas2025 · 11 citations
57. Consistent Autoformalization for Constructing Mathematical LibrariesConference on Empirical Methods in Natural Language Processing (EMNLP)Lan Zhang, Xin Quan, Andre Freitas2024 · 11 citations
58. MIND: Math Informed syNthetic Dialogues for Pretraining LLMsarXiv:2410.12881Syeda Nahida Akter, Shrimai Prabhumoye, John Kamalu, et al.2024 · 11 citations
59. REAL-Prover: Retrieval Augmented Lean Prover for Mathematical ReasoningarXiv:2505.20613Ziju Shen, Naohao Huang, Fanyi Yang, et al.2025 · 10 citations
60. SubgoalXL: Subgoal-based Expert Learning for Theorem ProvingarXiv:2408.11172Xueliang Zhao, Lin Zheng, Haige Bo, et al.2024 · 10 citations
61. Examining False Positives under Inference Scaling for Mathematical ReasoningConference on Empirical Methods in Natural Language Processing (EMNLP)Yu Wang, Nan Yang, Liang Wang, et al.2025 · 9 citations
62. Mathesis: Towards Formal Theorem Proving from Natural LanguagesarXiv:2506.07047Yu Xuejun, Jianyuan Zhong, Zijin Feng, et al.2025 · 9 citations
63. ReForm: Reflective Autoformalization with Prospective Bounded Sequence OptimizationarXiv:2510.24592Guoxin Chen, Jing Wu, Xinjie Chen, et al.2025 · 8 citations
64. A Survey on Feedback-based Multi-step Reasoning for Large Language Models on MathematicsarXiv:2502.14333Ting-Ruen Wei, Haowei Liu, Xuyang Wu, et al.2025 · 7 citations
65. Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math CapabilityConference on Empirical Methods in Natural Language Processing (EMNLP)Ruida Wang, Yuxin Li, Yi R. Fung, et al.2025 · 7 citations
66. Reviving DSP for Advanced Theorem Proving in the Era of Reasoning ModelsConference on Neural Information Processing Systems (NeurIPS)Chenrui Cao, Liangcheng Song, Zenan Li, et al.2025 · 7 citations
67. StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning FusionarXiv:2508.04440Yutong Wu, Di Huang, Ruosi Wan, et al.2025 · 7 citations
68. Autoformalizer with Tool FeedbackarXiv:2510.06857Qi Guo; Jianing Wang; Jianfei Zhang; Deyang Kong; Xiangzhou Huang; Xiangyu Xi; Wei Wang; Jingang Wang; Xunliang Cai; Shikun Zhang;, Wei Ye2025 · 6 citations
69. Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning ModelsAnnual Meeting of the Association for Computational Linguistics (ACL)Dadi Guo, Jiayu Liu, Zhiyuan Fan, et al.2026 · 5 citations
70. MASA: LLM-Driven Multi-Agent Systems for AutoformalizationConference on Empirical Methods in Natural Language Processing (EMNLP)Lan Zhang, Marco Valentino, Andre Freitas2025 · 5 citations
71. Premise Selection for a Lean HammerarXiv:2506.07477Thomas Zhu, Joshua Clune, Jeremy Avigad, et al.2025 · 5 citations
72. miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path ForwardConference on Neural Information Processing Systems (NeurIPS)Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh2025 · 4 citations
73. MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data CurationConference on Neural Information Processing Systems (NeurIPS)Zhenwen Liang, Linfeng Song, Yang Li, et al.2025 · 4 citations
74. ReProbe: Efficient Test-Time Scaling of Multi-Step Reasoning by Probing Internal States of Large Language ModelsAnnual Meeting of the Association for Computational Linguistics (ACL)Jingwei Ni, Ekaterina Fadeeva, Tianyi Wu, et al.2026 · 1 citation
75. Beyond Memorization: Testing LLM Reasoning on Unseen Theory of Computation TasksFindings of the Association for Computational LinguisticsShlok Shelat, Jay Raval, Souvik Roy, et al.2026
76. FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in LeanAnnual Meeting of the Association for Computational Linguistics (ACL)Jordan Meadows, Lan Zhang, Andre Freitas2026
77. Open Problems Solved by LLMs? A Survey of Verifiable Mathematical DiscoveryBig Picture v2: Crafting a Research NarrativeIoannis Tzachristas, Georgios Tzachristas, Aifen Sui2026
78. Reliable Use of Lemmas via Eligibility Reasoning and Section-Aware Reinforcement LearningAnnual Meeting of the Association for Computational Linguistics (ACL)Zhikun Xu, Xiaodong Yu, Ben Zhou, et al.2026

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

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/authors/bartosz-piotrowski/cited-by/