🧑‍🔬 Who cites John Harrison

45 citations of their works from 40 papers of our library (of the 149,439 whose bibliographies we read) · 27 with a page here, the most cited first · ← John Harrison

1. Mathematical Capabilities of ChatGPTConference on Neural Information Processing Systems (NeurIPS)Simon Frieder, Luca Pinchetti, Alexis Chevalier, et al.2023 · 449 citations
2. The Lean mathematical libraryACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)The mathlib Community2019 · 249 citations
3. Generative Language Modeling for Automated Theorem ProvingarXiv:2009.03393Stanislas Polu, Ilya Sutskever2020 · 241 citations
4. Autoformalization with Large Language ModelsarXiv:2205.12615Yuhuai Wu, Albert Q. Jiang, Wenda Li, et al.2022 · 204 citations
5. HyperTree Proof Search for Neural Theorem ProvingConference on Neural Information Processing Systems (NeurIPS)Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, et al.2022 · 151 citations
6. Deep Network Guided Proof SearchEPiC series in computingSarah Loos, Geoffrey Irving, Christian Szegedy, et al.2017 · 139 citations
7. Premise Selection for Theorem Proving by Deep Graph EmbeddingarXiv:1709.09994Mingzhe Wang, Yihe Tang, Jian Wang, et al.2017 · 106 citations
8. Learning to Prove Theorems via Interacting with Proof AssistantsarXiv:1905.09381Kaiyu Yang, Jia Deng2019 · 90 citations
9. LEGO-Prover: Neural Theorem Proving with Growing LibrariesarXiv:2310.00656Haiming Wang, Huajian Xin, Chuanyang Zheng, et al.2023 · 79 citations
10. HOList: An Environment for Machine Learning of Higher-Order Theorem ProvingarXiv:1904.03241Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, et al.2019 · 78 citations
11. First Experiments with Neural Translation of Informal to Formal MathematicsLecture notes in computer scienceQingxiang Wang, Cezary Kaliszyk, Josef Urban2018 · 66 citations
12. Formalising perfectoid spacesACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)Kevin Buzzard, Johan Commelin, Patrick Massot2019 · 48 citations
13. HolStep: A Machine Learning Dataset for Higher-order Logic Theorem ProvingarXiv:1703.00426Cezary Kaliszyk, François Chollet, Christian Szegedy2017 · 48 citations
14. A Survey on Deep Learning for Theorem ProvingarXiv:2404.09939Zhaoyu Li, Jialiang Sun, Logan Murphy, et al.2024 · 46 citations
15. INT: An Inequality Benchmark for Evaluating Generalization in Theorem ProvingarXiv:2007.02924Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba, et al.2020 · 41 citations
16. DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value FunctionAnnual Meeting of the Association for Computational Linguistics (ACL)Haiming Wang, Ye Yuan, Zhengying Liu, et al.2023 · 40 citations
17. Evaluating Language Models for Mathematics through InteractionsarXiv:2306.01694Katherine M. Collins, Albert Q. Jiang, Simon Frieder, et al.2023 · 40 citations
18. Learning to Reason in Large Theories without ImitationarXiv:1905.10501Kshitij Bansal, Christian Szegedy, Markus N. Rabe, et al.2019 · 36 citations
19. Graph Representations for Higher-Order Logic and Theorem ProvingProceedings of the AAAI Conference on Artificial IntelligenceAditya Paliwal, Sarah Loos, Markus Rabe, et al.2019 · 33 citations
20. PaMpeR: Proof Method Recommendation System for Isabelle/HOLarXiv:1806.07239Yutaka Nagashima, Yilun He2018 · 29 citations
21. TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement LearningarXiv:2102.09756Minchao Wu, Michael Norrish, Christian Walder, et al.2021 · 24 citations
22. Autoformalizing Euclidean GeometryarXiv:2405.17216Logan Murphy, Kaiyu Yang, Jialiang Sun, et al.2024 · 23 citations
23. 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
24. Proving Olympiad Algebraic Inequalities without Human DemonstrationsConference on Neural Information Processing Systems (NeurIPS)Chenrui Wei, Mengzhou Sun, Wei Wang2024 · 12 citations
25. Autoformalization in the Era of Large Language Models: A SurveyarXiv:2505.23486Ke Weng, Lun Du, Sirui Li, et al.2025 · 11 citations
26. Proving Olympiad Inequalities by Synergizing LLMs and Symbolic ReasoningarXiv:2502.13834Zenan Li, Zhaoyu Li, Wen Tang, et al.2025 · 11 citations
27. ProofFlow: A Dependency Graph Approach to Faithful Proof AutoformalizationarXiv:2510.15981Rafael Cabral, Tuan Manh Do, Xuejun Yu, et al.2025 · 5 citations

13 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/john-harrison/cited-by/