---
title: "A Survey on Deep Learning for Theorem Proving — Li 2024"
description: "Research applying neural methods, and especially large language models, to mathematical proof… 258 references, cited by 38 papers here."
authors: ["Zhaoyu Li", "Jialiang Sun", "Logan Murphy", "Qidong Su", "Zenan Li", "Xian Zhang", "Kaiyu Yang", "Xujie Si"]
year: 2024
venue: "arXiv:2404.09939"
source: "https://arxiv.org/abs/2404.09939"
doi: "10.48550/arxiv.2404.09939"
arxiv: "2404.09939"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/li-2024-survey-deep-learning-theorem-proving/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/li-2024-survey-deep-learning-theorem-proving/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2024](https://md.research.elamur.ai/free/en/papers/2024/page/9/) / A Survey on Deep Learning for Theorem Proving

# A Survey on Deep Learning for Theorem Proving

**Authors:** [Zhaoyu Li](https://md.research.elamur.ai/free/en/authors/zhaoyu-li/), [Jialiang Sun](https://md.research.elamur.ai/free/en/authors/jialiang-sun/), [Logan Murphy](https://md.research.elamur.ai/free/en/authors/logan-murphy/), Qidong Su, [Zenan Li](https://md.research.elamur.ai/free/en/authors/zenan-li/), [Xian Zhang](https://md.research.elamur.ai/free/en/authors/xian-zhang/), [Kaiyu Yang](https://md.research.elamur.ai/free/en/authors/kaiyu-yang/) and [Xujie Si](https://md.research.elamur.ai/free/en/authors/xujie-si/) · **Year:** 2024 · **Venue:** arXiv:2404.09939 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/2404.09939) · [PDF](https://arxiv.org/pdf/2404.09939v3) · [DOI 10.48550/arxiv.2404.09939](https://doi.org/10.48550/arxiv.2404.09939) · [arXiv 2404.09939](https://arxiv.org/abs/2404.09939) · [OpenAlex](https://openalex.org/W4394868324)

**Citations:** 8 citations (OpenAlex, 2026-10-14) · [38](https://md.research.elamur.ai/free/en/papers/li-2024-survey-deep-learning-theorem-proving/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Research applying neural methods, and especially large language models, to mathematical proof has grown quickly. It now spans many tasks, datasets and evaluation practices with no unifying picture. This survey organizes more than 180 papers on deep learning for theorem proving into one framework. It covers both informal proving (natural-language mathematics) and formal proving, the latter including automated provers such as E, Vampire, Z3 and CVC5 and proof assistants such as Lean, Isabelle, Coq, HOL Light and Metamath.

The work is grouped into five task families: converting informal mathematics into formal statements (autoformalization), selecting relevant premises, producing individual proof steps, searching for complete proofs, and a residual category of other tasks. The authors also catalogue human-curated and synthetic datasets, review evaluation metrics and how state-of-the-art systems perform, and discuss open problems. These include data scarcity, results that are hard to compare across proof assistants, possible test-set contamination in pretrained LLMs, and few tools that working mathematicians can actually use.

The survey is useful as a single entry point for researchers new to the area. It also sets out a research agenda covering conjecturing, verified code generation and math education.

## Key points
- The survey covers over 180 papers. Yearly publications in the area rose from about 2 in 2016 to 45 in 2023, and growth continued into 2024 (counted up to July).
- A curated paper list is maintained at the DL4TP GitHub repository (github.com/zhaoyu-li/DL4TP).
- Autoformalization work has moved from seq2seq translation of LaTeX into Mizar to few-shot LLM approaches using PaLM, Codex and GPT-4. Examples include LeanEuclid for Euclidean geometry and DSP, which drafts informal proofs with Minerva, maps them to formal sketches and lets ATPs fill the gaps.
- On evaluation, miniF2F exists for several proof assistants, but automation tools can affect scores more than the neural model does. Isabelle's Sledgehammer, which Lean lacks, is one example. Time and attempt budgets can also reorder method rankings.
- Proposed future directions are AI-driven conjecturing, LLM-based verified code generation (Dafny, Verus, F*, Coq) and formal-math tutoring, for example with Lean Copilot.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [University of Toronto](https://md.research.elamur.ai/free/en/universities/university-of-toronto/) — University, Toronto, Canada · 121 works · 179,943 citations
- [Nanjing University](https://md.research.elamur.ai/free/en/universities/nanjing-university/) — University, Nanjing, China · 102 works · 8,589 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang and Xujie Si. 2024. A Survey on Deep Learning for Theorem Proving. arXiv:2404.09939.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{li2024survey,
  title = {{A Survey on Deep Learning for Theorem Proving}},
  author = {Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang and Xujie Si},
  year = {2024},
  doi = {10.48550/arxiv.2404.09939},
  eprint = {2404.09939},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2404.09939}
}
```

- [← previous A Human-Inspired Reading Agent with Gist Memory of Very Long Contexts](https://md.research.elamur.ai/free/en/papers/lee-2024-human-inspired-reading-agent-gist/)
- [next → ARGS: Alignment as Reward-Guided Search](https://md.research.elamur.ai/free/en/papers/khanov-2024-args-alignment-reward-guided-search/)
- [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/9/)

## References

258 references, 123 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Ibrahim Abdelaziz, Veronika Thost, Maxwell Crouse, and Achille Fokoue. An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic. arXiv preprint arXiv:2002.00423, 2020. — [arXiv:2002.00423](https://arxiv.org/abs/2002.00423) [find](https://scholar.google.com/scholar?q=Ibrahim+Abdelaziz%2C+Veronika+Thost%2C+Maxwell+Crouse%2C+and+Achille+Fokoue%2E+An+Experimental+Study+of+Formula+Embeddings+for+Automated+Theorem+Proving+in+First%2DOrder+Logic%2E+arXiv+preprint+arXiv%3A2002%2E00423%2C+)
2. Ibrahim Abdelaziz, Maxwell Crouse, Bassem Makni, Vernon Austel, Cristina Cornelio, Shajith Ikbal, Pavan Kapanipathi, Ndivhuwo Makondo, Kavitha Srinivas, Michael Witbrock, et al. Learning to Guide a Saturation-Based Theorem Prover. IEEE Transactions on Pattern Analysis and Machine Intelligence, 2022. [find](https://scholar.google.com/scholar?q=Ibrahim+Abdelaziz%2C+Maxwell+Crouse%2C+Bassem+Makni%2C+Vernon+Austel%2C+Cristina+Cornelio%2C+Shajith+Ikbal%2C+Pavan+Kapanipathi%2C+Ndivhuwo+Makondo%2C+Kavitha+Srinivas%2C+Michael+Witbrock%2C+et+al%2E+Learning+to+Guide+a+Sa)
3. Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. [GPT-4 Technical Report](https://md.research.elamur.ai/free/en/papers/openai-2023-gpt-4-technical-report/). arXiv preprint arXiv:2303.08774, 2023.
4. Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. [Towards a Mathematics Formalisation Assistant using Large Language Models](https://md.research.elamur.ai/free/en/papers/agrawal-2022-mathematics-formalisation-assistant-large-language/). arXiv preprint arXiv:2211.07524, 2022.
5. Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. [Premise Selection for Mathematics by Corpus Analysis and Kernel Methods](https://md.research.elamur.ai/free/en/papers/alama-2011-premise-selection-mathematics-corpus-analysis/). Journal of Automated Reasoning, 2014.
6. Chenyang An, Zhibo Chen, Qihao Ye, Emily First, Letian Peng, Jiayun Zhang, Zihan Wang, Sorin Lerner, and Jingbo Shang. Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving. arXiv preprint arXiv:2404.07382, 2024. [find](https://scholar.google.com/scholar?q=Chenyang+An%2C+Zhibo+Chen%2C+Qihao+Ye%2C+Emily+First%2C+Letian+Peng%2C+Jiayun+Zhang%2C+Zihan+Wang%2C+Sorin+Lerner%2C+and+Jingbo+Shang%2E+Learn+from+Failure%3A+Fine%2DTuning+LLMs+with+Trial%2Dand%2DError+Data+for+Intuitionistic)
7. Marcin Andrychowicz, Filip Wolski, Alex Ray, Jonas Schneider, Rachel Fong, Peter Welinder, Bob McGrew, Josh Tobin, Pieter Abbeel, and Wojciech Zaremba. [Hindsight Experience Replay](https://md.research.elamur.ai/free/en/papers/andrychowicz-2017-hindsight-experience-replay/). In Proceedings of the International Conference on Neural Information Processing Systems, 2017.
8. Eser Aygün, Zafarali Ahmed, Ankit Anand, Vlad Firoiu, Xavier Glorot, Laurent Orseau, Doina Precup, and Shibl Mourad. [Learning to Prove from Synthetic Theorems](https://md.research.elamur.ai/free/en/papers/aygun-2020-learning-prove-synthetic-theorems/). arXiv preprint arXiv:2006.11259, 2020.
9. Eser Aygün, Ankit Anand, Laurent Orseau, Xavier Glorot, Stephen M Mcaleer, Vlad Firoiu, Lei M Zhang, Doina Precup, and Shibl Mourad. Proving Theorems using Incremental Learning and Hindsight Experience Replay. In Proceedings of the International Conference on Machine Learning, 2022. [find](https://scholar.google.com/scholar?q=Eser+Aygu%CC%88n%2C+Ankit+Anand%2C+Laurent+Orseau%2C+Xavier+Glorot%2C+Stephen+M+Mcaleer%2C+Vlad+Firoiu%2C+Lei+M+Zhang%2C+Doina+Precup%2C+and+Shibl+Mourad%2E+Proving+Theorems+using+Incremental+Learning+and+Hindsight+Experien)
10. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/). arXiv preprint arXiv:2302.12433, 2023.
11. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. [Llemma: An Open Language Model for Mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-llemma-open-language-model-mathematics/). In Proceedings of the International Conference on Learning Representations, 2024.
12. Kshitij Bansal and Christian Szegedy. Learning Alignment between Formal & Informal Mathematics. In Proceedings of the Conference on Artificial Intelligence and Theorem Proving, 2020. [find](https://scholar.google.com/scholar?q=Kshitij+Bansal+and+Christian+Szegedy%2E+Learning+Alignment+between+Formal+%26+Informal+Mathematics%2E+In+Proceedings+of+the+Conference+on+Artificial+Intelligence+and+Theorem+Proving%2C+2020%2E)
13. Kshitij Bansal, Sarah M. Loos, Markus Norman Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving. In Proceedings of the International Conference on Machine Learning, 2019. — [HOList: An Environment for Machine Learning of Higher-Order Theorem Proving](https://md.research.elamur.ai/free/en/papers/bansal-2019-holist-environment-machine-learning-higher/)
14. Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al. [CVC5: A Versatile and Industrial-Strength SMT Solver](https://md.research.elamur.ai/free/en/papers/barbosa-2022-cvc5-versatile-industrial-strength-smt/). In Proceedings of the International Conference on Tools and Algorithms for the Cons…
15. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, et al. The Coq Proof Assistant Reference Manual. INRIA, 1999. [find](https://scholar.google.com/scholar?q=Bruno+Barras%2C+Samuel+Boutin%2C+Cristina+Cornes%2C+Judicae%CC%88l+Courant%2C+Yann+Coscoy%2C+David+Delahaye%2C+Daniel+de+Rauglaudre%2C+Jean%2DChristophe+Fillia%CC%82tre%2C+Eduardo+Gime%CC%81nez%2C+Hugo+Herbelin%2C+et+al%2E+The+Coq+Proof+As)
16. Filip Bártek and Martin Suda. How Much Should This Symbol Weigh? A GNN-Advised Clause Selection. In Proceedings of International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2023. [find](https://scholar.google.com/scholar?q=Filip+Ba%CC%81rtek+and+Martin+Suda%2E+How+Much+Should+This+Symbol+Weigh%3F+A+GNN%2DAdvised+Clause+Selection%2E+In+Proceedings+of+International+Conference+on+Logic+for+Programming%2C+Artificial+Intelligence+and+Reaso)
17. Andrej Bauer, Matej Petković, and Ljupco Todorovski. MLFMF: Data Sets for Machine Learning for Mathematical Formalization. In Proceedings of the International Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2023. [find](https://scholar.google.com/scholar?q=Andrej+Bauer%2C+Matej+Petkovic%CC%81%2C+and+Ljupco+Todorovski%2E+MLFMF%3A+Data+Sets+for+Machine+Learning+for+Mathematical+Formalization%2E+In+Proceedings+of+the+International+Conference+on+Neural+Information+Process)
18. Yoshua Bengio and Nikolay Malkin. [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, 2024.
19. Armin Biere. CaDiCaL at the SAT Race 2019. In Proceedings of SAT Race 2019 – Solver and Benchmark Descriptions, 2019. [find](https://scholar.google.com/scholar?q=Armin+Biere%2E+CaDiCaL+at+the+SAT+Race+2019%2E+In+Proceedings+of+SAT+Race+2019+%E2%80%93+Solver+and+Benchmark+Descriptions%2C+2019%2E)
20. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C Paulson, and Josef Urban. [Hammering Towards QED](https://md.research.elamur.ai/free/en/papers/blanchette-2016-hammering-qed/). Journal of Formalized Reasoning, 2016.
21. Sascha Böhme and Tobias Nipkow. Sledgehammer: Judgement Day. In Proceedings of the International Joint Conference on Automated Reasoning, 2010. [find](https://scholar.google.com/scholar?q=Sascha+Bo%CC%88hme+and+Tobias+Nipkow%2E+Sledgehammer%3A+Judgement+Day%2E+In+Proceedings+of+the+International+Joint+Conference+on+Automated+Reasoning%2C+2010%2E)
22. Kaj Bostrom, Zayne Sprague, Swarat Chaudhuri, and Greg Durrett. Natural Language Deduction through Search over Statement Compositions. In Findings of the Association for Computational Linguistics: EMNLP, 2022. [find](https://scholar.google.com/scholar?q=Kaj+Bostrom%2C+Zayne+Sprague%2C+Swarat+Chaudhuri%2C+and+Greg+Durrett%2E+Natural+Language+Deduction+through+Search+over+Statement+Compositions%2E+In+Findings+of+the+Association+for+Computational+Linguistics%3A+EMN)
23. David Brandfonbrener, Sibi Raja, Tarun Prasad, Chloe Loughridge, Jianang Yang, Simon Henniger, William E Byrd, Robert Zinkov, and Nada Amin. Verified Multi-Step Synthesis using Large Language Models and Monte Carlo Tree Search. arXiv preprint arXiv:2402.08147, 2024. — [arXiv:2402.08147](https://arxiv.org/abs/2402.08147) [find](https://scholar.google.com/scholar?q=David+Brandfonbrener%2C+Sibi+Raja%2C+Tarun+Prasad%2C+Chloe+Loughridge%2C+Jianang+Yang%2C+Simon+Henniger%2C+William+E+Byrd%2C+Robert+Zinkov%2C+and+Nada+Amin%2E+Verified+Multi%2DStep+Synthesis+using+Large+Language+Models+a)
24. Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. [Language Models are Few-Shot Learners](https://md.research.elamur.ai/free/en/papers/brown-2020-language-models-few-shot-learners/). In Proceedings of the International Conference on Neural Information Processing Systems, 2020.
25. N.G. Bruijn, de. The Mathematical Language Automath, Its Usage and Some of Its Extensions. In Proceedings of the Symposium on Automatic Demonstration, 1970. [find](https://scholar.google.com/scholar?q=N%2EG%2E+Bruijn%2C+de%2E+The+Mathematical+Language+Automath%2C+Its+Usage+and+Some+of+Its+Extensions%2E+In+Proceedings+of+the+Symposium+on+Automatic+Demonstration%2C+1970%2E)
26. Kevin Buzzard. Lean in 2024. lean-in-2024/, 2024. [find](https://scholar.google.com/scholar?q=Kevin+Buzzard%2E+Lean+in+2024%2E+lean%2Din%2D2024%2F%2C+2024%2E)
27. Davide Castelvecchi. Mathematicians Welcome Computer-Assisted Proof in ‘Grand Unification’ Theory. Nature, 2021. [find](https://scholar.google.com/scholar?q=Davide+Castelvecchi%2E+Mathematicians+Welcome+Computer%2DAssisted+Proof+in+%E2%80%98Grand+Unification%E2%80%99+Theory%2E+Nature%2C+2021%2E)
28. Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, and Nikhil Swamy. Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming. arXiv preprint arXiv:2405.01787, 2024. [find](https://scholar.google.com/scholar?q=Saikat+Chakraborty%2C+Gabriel+Ebner%2C+Siddharth+Bhat%2C+Sarah+Fakhoury%2C+Sakina+Fatima%2C+Shuvendu+Lahiri%2C+and+Nikhil+Swamy%2E+Towards+Neural+Synthesis+for+SMT%2DAssisted+Proof%2DOriented+Programming%2E+arXiv+preprin)
29. Jiaqi Chen, Tong Li, Jinghui Qin, Pan Lu, Liang Lin, Chongyu Chen, and Xiaodan Liang. [UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression](https://md.research.elamur.ai/free/en/papers/chen-2022-unigeo-unifying-geometry-logical-reasoning/). In Proceedings of the Conference on Empirical Methods in Natural Language Processing, 2022. [https://xenaproject.wordpress.com/2…](https://xenaproject.wordpress.com/2…) [↗](https://xenaproject.wordpress.com/2…)
30. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. [Evaluating Large Language Models Trained on Code](https://md.research.elamur.ai/free/en/papers/chen-2021-evaluating-large-language-models-trained/). arXiv preprint arXiv:2107.03374, 2021.
31. Ting Chen, Simon Kornblith, Mohammad Norouzi, and Geoffrey Hinton. [A Simple Framework for Contrastive Learning of Visual Representations](https://md.research.elamur.ai/free/en/papers/chen-2020-simple-framework-contrastive-learning-visual/). In Proceedings of the International Conference on Machine Learning, 2020.
32. Kyunghyun Cho, Bart Van Merriënboer, Caglar Gulcehre, Dzmitry Bahdanau, Fethi Bougares, Holger Schwenk, and Yoshua Bengio. [Learning Phrase Representations using RNN Encoder–Decoder for Statistical Machine Translation](https://md.research.elamur.ai/free/en/papers/cho-2014-learning-phrase-representations-rnn-encoder/). In Proceedings of the Conference on Empirical Methods in Natural Language Process…
33. Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering. Journal of Automated Reasoning, 2000. [find](https://scholar.google.com/scholar?q=Shang%2DChing+Chou%2C+Xiao%2DShan+Gao%2C+and+Jing%2DZhong+Zhang%2E+A+Deductive+Database+Approach+to+Automated+Geometry+Theorem+Proving+and+Discovering%2E+Journal+of+Automated+Reasoning%2C+2000%2E)
34. Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, et al. [PaLM: Scaling Language Modeling with Pathways](https://md.research.elamur.ai/free/en/papers/chowdhery-2022-palm-scaling-language-modeling-pathways/). Journal of Machine Learning Research, 2023.
35. Karel Chvalovskỳ, Jan Jakubüv, Martin Suda, and Josef Urban. [ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E](https://md.research.elamur.ai/free/en/papers/chvalovsky-2019-enigma-ng-efficient-neural-gradient/). In Proceedings of the International Conference on Automated Deduction, 2019.
36. Karel Chvalovskỳ, Jan Jakubüv, Miroslav Olšák, and Josef Urban. Learning Theorem Proving Components. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 2021. [find](https://scholar.google.com/scholar?q=Karel+Chvalovsky%CC%80%2C+Jan+Jakubu%CC%88v%2C+Miroslav+Ols%CC%8Ca%CC%81k%2C+and+Josef+Urban%2E+Learning+Theorem+Proving+Components%2E+In+Proceedings+of+the+International+Conference+on+Automated+Reasoning+with+Analytic+Tableaux+an)
37. Karel Chvalovskỳ, Konstantin Korovin, Jelle Piepenbrock, and Josef Urban. Guiding an Instantiation Prover with Graph Neural Networks. In Proceedings of International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2023. [find](https://scholar.google.com/scholar?q=Karel+Chvalovsky%CC%80%2C+Konstantin+Korovin%2C+Jelle+Piepenbrock%2C+and+Josef+Urban%2E+Guiding+an+Instantiation+Prover+with+Graph+Neural+Networks%2E+In+Proceedings+of+International+Conference+on+Logic+for+Programmi)
38. Peter Clark, Oyvind Tafjord, and Kyle Richardson. [Transformers as Soft Reasoners over Language](https://md.research.elamur.ai/free/en/papers/clark-2020-transformers-soft-reasoners-over-language/). In Proceedings of the International Joint Conference on Artificial Intelligence, 2020.
39. Katherine M Collins, Albert Q Jiang, Simon Frieder, Lionel Wong, Miri Zilka, Umang Bhatt, Thomas Lukasiewicz, Yuhuai Wu, Joshua B Tenenbaum, William Hart, et al. [Evaluating Language Models for Mathematics through Interactions](https://md.research.elamur.ai/free/en/papers/collins-2023-evaluating-language-models-mathematics-through/). arXiv preprint arXiv:2306.01694, 2023.
40. Maxwell Crouse, Ibrahim Abdelaziz, Cristina Cornelio, Veronika Thost, Lingfei Wu, Kenneth Forbus, and Achille Fokoue. Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling. arXiv preprint arXiv:1911.06904, 2019. — [arXiv:1911.06904](https://arxiv.org/abs/1911.06904) [find](https://scholar.google.com/scholar?q=Maxwell+Crouse%2C+Ibrahim+Abdelaziz%2C+Cristina+Cornelio%2C+Veronika+Thost%2C+Lingfei+Wu%2C+Kenneth+Forbus%2C+and+Achille+Fokoue%2E+Improving+Graph+Neural+Network+Representations+of+Logical+Formulae+with+Subgraph+P)
41. Maxwell Crouse, Ibrahim Abdelaziz, Bassem Makni, Spencer Whitehead, Cristina Cornelio, Pavan Kapanipathi, Kavitha Srinivas, Veronika Thost, Michael Witbrock, and Achille Fokoue. A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving. In Proceedings of the AAAI Conference on Arti… [find](https://scholar.google.com/scholar?q=Maxwell+Crouse%2C+Ibrahim+Abdelaziz%2C+Bassem+Makni%2C+Spencer+Whitehead%2C+Cristina+Cornelio%2C+Pavan+Kapanipathi%2C+Kavitha+Srinivas%2C+Veronika+Thost%2C+Michael+Witbrock%2C+and+Achille+Fokoue%2E+A+Deep+Reinforcement+L)
42. Garett Cunningham, Razvan C Bunescu, and David Juedes. [Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs](https://md.research.elamur.ai/free/en/papers/cunningham-2022-autoformalization-mathematics-code-correctness-experiments/). In Proceedings of the Workshop on Mathematical Natural Language Processing, 2022.
43. Łukasz Czajka and Cezary Kaliszyk. Hammer for Coq: Automation for Dependent Type Theory. Journal of automated reasoning, 2018. [find](https://scholar.google.com/scholar?q=%C5%81ukasz+Czajka+and+Cezary+Kaliszyk%2E+Hammer+for+Coq%3A+Automation+for+Dependent+Type+Theory%2E+Journal+of+automated+reasoning%2C+2018%2E)
44. Bhavana Dalvi, Peter Jansen, Oyvind Tafjord, Zhengnan Xie, Hannah Smith, Leighanna Pipatanangkura, and Peter Clark. [Explaining Answers with Entailment Trees](https://md.research.elamur.ai/free/en/papers/dalvi-2021-explaining-answers-entailment-trees/). In Proceedings of the Conference on Empirical Methods in Natural Language Processing, 2021.
45. Doratossadat Dastgheib and Ehsaneddin Asgari. Keyword-Based Natural Language Premise Selection for an Automatic Mathematical Statement Proving. In Proceedings of TextGraphs-16: Graph-Based Methods for Natural Language Processing, 2022. [find](https://scholar.google.com/scholar?q=Doratossadat+Dastgheib+and+Ehsaneddin+Asgari%2E+Keyword%2DBased+Natural+Language+Premise+Selection+for+an+Automatic+Mathematical+Statement+Proving%2E+In+Proceedings+of+TextGraphs%2D16%3A+Graph%2DBased+Methods+for)
46. Martin Davis. A Computer Program for Presburger’s Algorithm. Symbolic Computation Automation of Reasoning 1, 1957. [find](https://scholar.google.com/scholar?q=Martin+Davis%2E+A+Computer+Program+for+Presburger%E2%80%99s+Algorithm%2E+Symbolic+Computation+Automation+of+Reasoning+1%2C+1957%2E)
47. Martin Davis and Hilary Putnam. A Computing Procedure for Quantification Theory. Journal of the ACM, 1960. [find](https://scholar.google.com/scholar?q=Martin+Davis+and+Hilary+Putnam%2E+A+Computing+Procedure+for+Quantification+Theory%2E+Journal+of+the+ACM%2C+1960%2E)
48. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008. [find](https://scholar.google.com/scholar?q=Leonardo+De+Moura+and+Nikolaj+Bj%C3%B8rner%2E+Z3%3A+An+efficient+SMT+solver%2E+In+Proceedings+of+the+International+Conference+on+Tools+and+Algorithms+for+the+Construction+and+Analysis+of+Systems%2C+2008%2E)
49. Jörg Denzinger, Matthias Fuchs, Christoph Goller, and Stephan Schulz. Learning from Previous Proof Experience: A Survey. Technical Report, 1999. [find](https://scholar.google.com/scholar?q=Jo%CC%88rg+Denzinger%2C+Matthias+Fuchs%2C+Christoph+Goller%2C+and+Stephan+Schulz%2E+Learning+from+Previous+Proof+Experience%3A+A+Survey%2E+Technical+Report%2C+1999%2E)
50. Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. [BERT: Pre-Training of Deep Bidirectional Transformers for Language Understanding](https://md.research.elamur.ai/free/en/papers/devlin-2019-bert-pre-training-deep-bidirectional/). In Proceedings of the Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, 2019.
51. David K Duvenaud, Dougal Maclaurin, Jorge Iparraguirre, Rafael Bombarell, Timothy Hirzel, Alán Aspuru-Guzik, and Ryan P Adams. [Convolutional Networks on Graphs for Learning Molecular Fingerprints](https://md.research.elamur.ai/free/en/papers/duvenaud-2015-convolutional-networks-graphs-learning-molecular/). In Proceedings of the International Conference on Neural Information Processing Systems, 2015.
52. Niklas Eén and Niklas Sörensson. [An Extensible SAT-Solver](https://md.research.elamur.ai/free/en/papers/een-2003-extensible-sat-solver/). In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, 2003.
53. Alhussein Fawzi, Mateusz Malinowski, Hamza Fawzi, and Omar Fawzi. Learning Dynamic Polynomial Proofs. In Proceedings of the International Conference on Neural Information Processing Systems, 2019. [find](https://scholar.google.com/scholar?q=Alhussein+Fawzi%2C+Mateusz+Malinowski%2C+Hamza+Fawzi%2C+and+Omar+Fawzi%2E+Learning+Dynamic+Polynomial+Proofs%2E+In+Proceedings+of+the+International+Conference+on+Neural+Information+Processing+Systems%2C+2019%2E)
54. Deborah Ferreira and André Freitas. Natural Language Premise Selection: Finding Supporting Statements for Mathematical Text. In Proceedings of the Language Resources and Evaluation Conference, 2020a. [find](https://scholar.google.com/scholar?q=Deborah+Ferreira+and+Andre%CC%81+Freitas%2E+Natural+Language+Premise+Selection%3A+Finding+Supporting+Statements+for+Mathematical+Text%2E+In+Proceedings+of+the+Language+Resources+and+Evaluation+Conference%2C+2020a%2E)
55. Deborah Ferreira and André Freitas. [Premise Selection in Natural Language Mathematical Texts](https://md.research.elamur.ai/free/en/papers/ferreira-2020-premise-selection-natural-language-mathematical/). In Proceedings of the Annual Meeting of the Association for Computational Linguistics, 2020b.
56. Deborah Ferreira and André Freitas. STAR: Cross-Modal [STA]tement [R]epresentation for Selecting Relevant Mathematical Premises. In Proceedings of the Conference of the European Chapter of the Association for Computational Linguistic, 2021. [find](https://scholar.google.com/scholar?q=Deborah+Ferreira+and+Andre%CC%81+Freitas%2E+STAR%3A+Cross%2DModal+%5BSTA%5Dtement+%5BR%5Depresentation+for+Selecting+Relevant+Mathematical+Premises%2E+In+Proceedings+of+the+Conference+of+the+European+Chapter+of+the+Associ)
57. Vlad Firoiu, Eser Aygun, Ankit Anand, Zafarali Ahmed, Xavier Glorot, Laurent Orseau, Lei Zhang, Doina Precup, and Shibl Mourad. Training a First-Order Theorem Prover from Synthetic Data. In International Conference on Learning Representations Workshop on Mathematical Reasoning in General Artificial… [find](https://scholar.google.com/scholar?q=Vlad+Firoiu%2C+Eser+Aygun%2C+Ankit+Anand%2C+Zafarali+Ahmed%2C+Xavier+Glorot%2C+Laurent+Orseau%2C+Lei+Zhang%2C+Doina+Precup%2C+and+Shibl+Mourad%2E+Training+a+First%2DOrder+Theorem+Prover+from+Synthetic+Data%2E+In+Internatio)
58. Emily First and Yuriy Brun. Diversity-Driven Automated Formal Verification. In Proceedings of the International Conference on Software Engineering, 2022. [find](https://scholar.google.com/scholar?q=Emily+First+and+Yuriy+Brun%2E+Diversity%2DDriven+Automated+Formal+Verification%2E+In+Proceedings+of+the+International+Conference+on+Software+Engineering%2C+2022%2E)
59. Emily First, Yuriy Brun, and Arjun Guha. TacTok: Semantics-Aware Proof Synthesis. Proceedings of the ACM on Programming Languages, 2020. [find](https://scholar.google.com/scholar?q=Emily+First%2C+Yuriy+Brun%2C+and+Arjun+Guha%2E+TacTok%3A+Semantics%2DAware+Proof+Synthesis%2E+Proceedings+of+the+ACM+on+Programming+Languages%2C+2020%2E)
60. Emily First, Markus Rabe, Talia Ringer, and Yuriy Brun. [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://md.research.elamur.ai/free/en/papers/first-2023-baldur-whole-proof-generation-repair/). In Proceedings of the ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2023.
61. Achille Fokoue, Ibrahim Abdelaziz, Maxwell Crouse, Shajith Ikbal, Akihiro Kishimoto, Guilherme Lima, Ndivhuwo Makondo, and Radu Marinescu. An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations. In Proceedings of the International Joint Conf… [find](https://scholar.google.com/scholar?q=Achille+Fokoue%2C+Ibrahim+Abdelaziz%2C+Maxwell+Crouse%2C+Shajith+Ikbal%2C+Akihiro+Kishimoto%2C+Guilherme+Lima%2C+Ndivhuwo+Makondo%2C+and+Radu+Marinescu%2E+An+Ensemble+Approach+for+Automated+Theorem+Proving+Based+on+E)
62. Simon Frieder, Julius Berner, Philipp Petersen, and Thomas Lukasiewicz. Large Language Models for Mathematicians. arXiv preprint arXiv:2312.04556, 2023a. — [arXiv:2312.04556](https://arxiv.org/abs/2312.04556) [find](https://scholar.google.com/scholar?q=Simon+Frieder%2C+Julius+Berner%2C+Philipp+Petersen%2C+and+Thomas+Lukasiewicz%2E+Large+Language+Models+for+Mathematicians%2E+arXiv+preprint+arXiv%3A2312%2E04556%2C+2023a%2E+%E2%80%94+%5BarXiv%3A2312%2E04556%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F231)
63. Simon Frieder, Luca Pinchetti, Alexis Chevalier, Ryan-Rhys Griffiths, Tommaso Salvatori, Thomas Lukasiewicz, Philipp Christian Petersen, and Julius Berner. [Mathematical Capabilities of ChatGPT](https://md.research.elamur.ai/free/en/papers/frieder-2023-mathematical-capabilities-chatgpt/). In Proceedings of the International Conference on Neural Information Processing Systems Datasets and Bench…
64. Simon Frieder, Martin Trimmel, Rashid Alawadhi, and Klaus Gy. LLM vs ITP. In International Conference on Neural Information Processing Systems Workshop on MATH-AI, 2023c. [find](https://scholar.google.com/scholar?q=Simon+Frieder%2C+Martin+Trimmel%2C+Rashid+Alawadhi%2C+and+Klaus+Gy%2E+LLM+vs+ITP%2E+In+International+Conference+on+Neural+Information+Processing+Systems+Workshop+on+MATH%2DAI%2C+2023c%2E)
65. Siddhartha Gadgil, Anand Rao Tadipatri, Ayush Agrawal, Ashvni Narayanan, and Navin Goyal. Towards Automating Formalisation of Theorem Statements using Large Language Models. In International Conference on Neural Information Processing Systems Workshop on MATH-AI, 2022. [find](https://scholar.google.com/scholar?q=Siddhartha+Gadgil%2C+Anand+Rao+Tadipatri%2C+Ayush+Agrawal%2C+Ashvni+Narayanan%2C+and+Navin+Goyal%2E+Towards+Automating+Formalisation+of+Theorem+Statements+using+Large+Language+Models%2E+In+International+Conferenc)
66. Thibault Gauthier. [Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic](https://md.research.elamur.ai/free/en/papers/gauthier-2019-deep-reinforcement-learning-synthesizing-functions/). In Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2020.
67. Thibault Gauthier. Learned Provability Likelihood for Tactical Search. In Proceedings of the International Symposium on Symbolic Computation in Software Science, 2021. [find](https://scholar.google.com/scholar?q=Thibault+Gauthier%2E+Learned+Provability+Likelihood+for+Tactical+Search%2E+In+Proceedings+of+the+International+Symposium+on+Symbolic+Computation+in+Software+Science%2C+2021%2E)
68. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. [TacticToe: Learning to Prove with Tactics](https://md.research.elamur.ai/free/en/papers/gauthier-2018-tactictoe-learning-prove-tactics/). Journal of Automated Reasoning, 2020.
69. Fabian Gloeckle, Baptiste Roziere, Amaury Hayat, and Gabriel Synnaeve. Temperature-Scaled Large Language Models for Lean Proofstep Prediction. In International Conference on Neural Information Processing Systems Workshop on MATH-AI, 2023. [find](https://scholar.google.com/scholar?q=Fabian+Gloeckle%2C+Baptiste+Roziere%2C+Amaury+Hayat%2C+and+Gabriel+Synnaeve%2E+Temperature%2DScaled+Large+Language+Models+for+Lean+Proofstep+Prediction%2E+In+International+Conference+on+Neural+Information+Process)
70. Xavier Glorot, Ankit Anand, Eser Aygun, Shibl Mourad, Pushmeet Kohli, and Doina Precup. Learning Representations of Logical Formulae using Graph Neural Networks. In International Conference on Neural Information Processing Systems Workshop on Graph Representation Learning, 2019. [find](https://scholar.google.com/scholar?q=Xavier+Glorot%2C+Ankit+Anand%2C+Eser+Aygun%2C+Shibl+Mourad%2C+Pushmeet+Kohli%2C+and+Doina+Precup%2E+Learning+Representations+of+Logical+Formulae+using+Graph+Neural+Networks%2E+In+International+Conference+on+Neural+)
71. Zarathustra A Goertzel and Josef Urban. Usefulness of Lemmas via Graph Neural Networks. In Proceedings of the Conference on Artificial Intelligence and Theorem Proving, 2019. [find](https://scholar.google.com/scholar?q=Zarathustra+A+Goertzel+and+Josef+Urban%2E+Usefulness+of+Lemmas+via+Graph+Neural+Networks%2E+In+Proceedings+of+the+Conference+on+Artificial+Intelligence+and+Theorem+Proving%2C+2019%2E)
72. Zarathustra A Goertzel, Karel Chvalovskỳ, Jan Jakubüv, Miroslav Olšák, and Josef Urban. Fast and Slow ENIGMAs and Parental Guidance. In Proceedings of the International Symposium on Frontiers of Combining Systems, 2021. [find](https://scholar.google.com/scholar?q=Zarathustra+A+Goertzel%2C+Karel+Chvalovsky%CC%80%2C+Jan+Jakubu%CC%88v%2C+Miroslav+Ols%CC%8Ca%CC%81k%2C+and+Josef+Urban%2E+Fast+and+Slow+ENIGMAs+and+Parental+Guidance%2E+In+Proceedings+of+the+International+Symposium+on+Frontiers+of+C)
73. Zarathustra A Goertzel, Jan Jakubüv, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock, and Josef Urban. The Isabelle ENIGMA. In Proceedings of the International Conference on Interactive Theorem Proving, 2022. [find](https://scholar.google.com/scholar?q=Zarathustra+A+Goertzel%2C+Jan+Jakubu%CC%88v%2C+Cezary+Kaliszyk%2C+Miroslav+Ols%CC%8Ca%CC%81k%2C+Jelle+Piepenbrock%2C+and+Josef+Urban%2E+The+Isabelle+ENIGMA%2E+In+Proceedings+of+the+International+Conference+on+Interactive+Theorem+)
74. Georges Gonthier. The Four Colour Theorem: Engineering of a Formal Proof. In Proceedings of the Asian Symposium on Computer Mathematics, 2008. [find](https://scholar.google.com/scholar?q=Georges+Gonthier%2E+The+Four+Colour+Theorem%3A+Engineering+of+a+Formal+Proof%2E+In+Proceedings+of+the+Asian+Symposium+on+Computer+Mathematics%2C+2008%2E)
75. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation, 2016. [find](https://scholar.google.com/scholar?q=Ronghui+Gu%2C+Zhong+Shao%2C+Hao+Chen%2C+Xiongnan+Newman+Wu%2C+Jieung+Kim%2C+Vilhelm+Sjo%CC%88berg%2C+and+David+Costanzo%2E+CertiKOS%3A+An+Extensible+Architecture+for+Building+Certified+Concurrent+OS+Kernels%2E+In+Proceeding)
76. Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. [A Formal Proof of the Kepler Conjecture](https://md.research.elamur.ai/free/en/papers/hales-2015-formal-proof-kepler-conjecture/). In Forum of Mathematics, Pi, 2017.
77. Jesse Michael Han, Tao Xu, Stanislas Polu, Arvind Neelakantan, and Alec Radford. Contrastive Finetuning of Generative Language models for Informal Premise Selection. In Proceedings of the Conference on Artificial Intelligence and Theorem Proving, 2021. [find](https://scholar.google.com/scholar?q=Jesse+Michael+Han%2C+Tao+Xu%2C+Stanislas+Polu%2C+Arvind+Neelakantan%2C+and+Alec+Radford%2E+Contrastive+Finetuning+of+Generative+Language+models+for+Informal+Premise+Selection%2E+In+Proceedings+of+the+Conference+o)
78. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. [Proof Artifact Co-Training for Theorem Proving with Language Models](https://md.research.elamur.ai/free/en/papers/han-2021-proof-artifact-co-training-theorem/). In Proceedings of the International Conference on Learning Representations, 2022.
79. John Harrison. HOL Light: A Tutorial Introduction. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 1996. [find](https://scholar.google.com/scholar?q=John+Harrison%2E+HOL+Light%3A+A+Tutorial+Introduction%2E+In+Proceedings+of+the+International+Conference+on+Formal+Methods+in+Computer%2DAided+Design%2C+1996%2E)
80. Edvard K Holden and Konstantin Korovin. Graph Sequence Learning for Premise Selection. In Proceedings of the Conference on Artificial Intelligence and Theorem Proving, 2023. [find](https://scholar.google.com/scholar?q=Edvard+K+Holden+and+Konstantin+Korovin%2E+Graph+Sequence+Learning+for+Premise+Selection%2E+In+Proceedings+of+the+Conference+on+Artificial+Intelligence+and+Theorem+Proving%2C+2023%2E)
81. Ruixin Hong, Hongming Zhang, Xintong Yu, and Changshui Zhang. MetGen: A Module-Based Entailment Tree Generation Framework for Answer Explanation. In Findings of the Association for Computational Linguistics: NAACL, 2022. [find](https://scholar.google.com/scholar?q=Ruixin+Hong%2C+Hongming+Zhang%2C+Xintong+Yu%2C+and+Changshui+Zhang%2E+MetGen%3A+A+Module%2DBased+Entailment+Tree+Generation+Framework+for+Answer+Explanation%2E+In+Findings+of+the+Association+for+Computational+Lingu)
82. Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. [GamePad: A Learning Environment for Theorem Proving](https://md.research.elamur.ai/free/en/papers/huang-2018-gamepad-learning-environment-theorem-proving/). In Proceedings of the International Conference on Learning Representations, 2019.
83. Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, and Xiaodan Liang. [MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data](https://md.research.elamur.ai/free/en/papers/huang-2024-mustard-mastering-uniform-synthesis-theorem/). In Proceedings of the International Conference on Learning Representations, 2024.
84. Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban. [DeepMath - Deep Sequence Models for Premise Selection](https://md.research.elamur.ai/free/en/papers/alemi-2016-deepmath-deep-sequence-models-premise/). In Proceedings of the International Conference on Neural Information Processing Systems, 2016.
85. Jan Jakubüv and Josef Urban. [ENIGMA: Efficient Learning-Based Inference Guiding Machine](https://md.research.elamur.ai/free/en/papers/jakubuv-2017-enigma-efficient-learning-based-inference/). In Proceedings of the International Conference on Intelligent Computer Mathematics, 2017.
86. Jan Jakubüv and Josef Urban. Hammering Mizar by Learning Clause Guidance. In Proceedings of the International Conference on Interactive Theorem Proving, 2019. [find](https://scholar.google.com/scholar?q=Jan+Jakubu%CC%88v+and+Josef+Urban%2E+Hammering+Mizar+by+Learning+Clause+Guidance%2E+In+Proceedings+of+the+International+Conference+on+Interactive+Theorem+Proving%2C+2019%2E)
87. Jan Jakubüv, Karel Chvalovskỳ, Miroslav Olšák, Bartosz Piotrowski, Martin Suda, and Josef Urban. [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)](https://md.research.elamur.ai/free/en/papers/jakubuv-2020-enigma-anonymous-symbol-independent-inference/). In Proceedings of the International Joint Conference on Automated Reasoning, 2020.
88. Jan Jakubüv, Karel Chvalovskỳ, Zarathustra A Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban. MizAR 60 for Mizar 50. In Proceedings of the International Conference on Interactive Theorem Proving, 2023. [find](https://scholar.google.com/scholar?q=Jan+Jakubu%CC%88v%2C+Karel+Chvalovsky%CC%80%2C+Zarathustra+A+Goertzel%2C+Cezary+Kaliszyk%2C+Mirek+Ols%CC%8Ca%CC%81k%2C+Bartosz+Piotrowski%2C+Stephan+Schulz%2C+Martin+Suda%2C+and+Josef+Urban%2E+MizAR+60+for+Mizar+50%2E+In+Proceedings+of+the+)
89. Albert Q Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. LISA: Language Models of Isabelle Proofs. In Proceedings of the Conference on Artificial Intelligence and Theorem Proving, 2021. [find](https://scholar.google.com/scholar?q=Albert+Q+Jiang%2C+Wenda+Li%2C+Jesse+Michael+Han%2C+and+Yuhuai+Wu%2E+LISA%3A+Language+Models+of+Isabelle+Proofs%2E+In+Proceedings+of+the+Conference+on+Artificial+Intelligence+and+Theorem+Proving%2C+2021%2E)
90. Albert Q Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://md.research.elamur.ai/free/en/papers/jiang-2022-thor-wielding-hammers-integrate-language/). In Proceedings of the International Conference on Neural Information Processing Systems…
91. Albert Q Jiang, Wenda Li, and Mateja Jamnik. [Multilingual Mathematical Autoformalization](https://md.research.elamur.ai/free/en/papers/jiang-2023-multilingual-mathematical-autoformalization/). arXiv preprint arXiv:2311.03755, 2023a.
92. Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/). In Proceedings of the International Conference on Learning Representations, 2023b.
93. Dongwei Jiang, Marcio Fonseca, and Shay B Cohen. [LeanReasoner: Boosting Complex Logical Reasoning with Lean](https://md.research.elamur.ai/free/en/papers/jiang-2024-leanreasoner-boosting-complex-logical-reasoning/). In Proceedings of the Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, 2024.
94. Moa Johansson and Nicholas Smallbone. Exploring Mathematical Conjecturing with Large Language Models. In Proceedings of the International Workshop on Neural-Symbolic Learning and Reasoning, 2023. [find](https://scholar.google.com/scholar?q=Moa+Johansson+and+Nicholas+Smallbone%2E+Exploring+Mathematical+Conjecturing+with+Large+Language+Models%2E+In+Proceedings+of+the+International+Workshop+on+Neural%2DSymbolic+Learning+and+Reasoning%2C+2023%2E)
95. Cezary Kaliszyk and Josef Urban. FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover. In Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2015a. [find](https://scholar.google.com/scholar?q=Cezary+Kaliszyk+and+Josef+Urban%2E+FEMaLeCoP%3A+Fairly+Efficient+Machine+Learning+Connection+Prover%2E+In+Proceedings+of+the+International+Conference+on+Logic+for+Programming%2C+Artificial+Intelligence+and+Re)
96. Cezary Kaliszyk and Josef Urban. [MizAR 40 for Mizar 40](https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/). Journal of Automated Reasoning, 2015b.
97. Cezary Kaliszyk, Josef Urban, Jiřı́ Vyskočil, and Herman Geuvers. Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description. In Proceedings of the International Conference on Intelligent Computer Mathematics, 2014. [find](https://scholar.google.com/scholar?q=Cezary+Kaliszyk%2C+Josef+Urban%2C+Jir%CC%8C%C4%B1%CC%81+Vyskoc%CC%8Cil%2C+and+Herman+Geuvers%2E+Developing+Corpus%2DBased+Translation+Methods+between+Informal+and+Formal+Mathematics%3A+Project+Description%2E+In+Proceedings+of+the+Inte)
98. Cezary Kaliszyk, Josef Urban, and Jiřı́ Vyskočil. Learning to Parse on Aligned Corpora (Rough Diamond). In Proceedings of the International Conference on Interactive Theorem Proving, 2015. [find](https://scholar.google.com/scholar?q=Cezary+Kaliszyk%2C+Josef+Urban%2C+and+Jir%CC%8C%C4%B1%CC%81+Vyskoc%CC%8Cil%2E+Learning+to+Parse+on+Aligned+Corpora+%28Rough+Diamond%29%2E+In+Proceedings+of+the+International+Conference+on+Interactive+Theorem+Proving%2C+2015%2E)
99. Cezary Kaliszyk, François Chollet, and Christian Szegedy. [HolStep: A Machine Learning Dataset for Higher-Order Logic Theorem Proving](https://md.research.elamur.ai/free/en/papers/kaliszyk-2017-holstep-machine-learning-dataset-higher/). In Proceedings of the International Conference on Learning Representations, 2017.
100. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák. [Reinforcement Learning of Theorem Proving](https://md.research.elamur.ai/free/en/papers/kaliszyk-2018-reinforcement-learning-theorem-proving/). In Proceedings of the International Conference on Neural Information Processing Systems, 2018.
101. Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, and Rahul Sharma. Finding Inductive Loop Invariants using Large Language Models. arXiv preprint arXiv:2311.07948, 2023. — [arXiv:2311.07948](https://arxiv.org/abs/2311.07948) [find](https://scholar.google.com/scholar?q=Adharsh+Kamath%2C+Aditya+Senthilnathan%2C+Saikat+Chakraborty%2C+Pantazis+Deligiannis%2C+Shuvendu+K+Lahiri%2C+Akash+Lal%2C+Aseem+Rastogi%2C+Subhajit+Roy%2C+and+Rahul+Sharma%2E+Finding+Inductive+Loop+Invariants+using+Lar)
102. Vladimir Karpukhin, Barlas Oğuz, Sewon Min, Patrick Lewis, Ledell Wu, Sergey Edunov, Danqi Chen, and Wen-tau Yih. [Dense Passage Retrieval for Open-Domain Question Answering](https://md.research.elamur.ai/free/en/papers/karpukhin-2020-dense-passage-retrieval-open-domain/). In Proceedings of the Conference on Empirical Methods in Natural Language Processing, 2020.
103. Christoph Kern and Mark R Greenstreet. Formal Verification in Hardware Design: A Survey. ACM Transactions on Design Automation of Electronic Systems, 1999. [find](https://scholar.google.com/scholar?q=Christoph+Kern+and+Mark+R+Greenstreet%2E+Formal+Verification+in+Hardware+Design%3A+A+Survey%2E+ACM+Transactions+on+Design+Automation+of+Electronic+Systems%2C+1999%2E)
104. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. seL4: Formal Verification of an OS Kernel. In Proceedings of the ACM SIGOPS Symposium on Operating Systems Principles, 2009. [find](https://scholar.google.com/scholar?q=Gerwin+Klein%2C+Kevin+Elphinstone%2C+Gernot+Heiser%2C+June+Andronick%2C+David+Cock%2C+Philip+Derrin%2C+Dhammika+Elkaduwe%2C+Kai+Engelhardt%2C+Rafal+Kolanski%2C+Michael+Norrish%2C+et+al%2E+seL4%3A+Formal+Verification+of+an+OS)
105. Konstantin Korovin. iProver–An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In Proceedings of the International Joint Conference on Automated Reasoning, 2008. [find](https://scholar.google.com/scholar?q=Konstantin+Korovin%2E+iProver%E2%80%93An+Instantiation%2DBased+Theorem+Prover+for+First%2DOrder+Logic+%28System+Description%29%2E+In+Proceedings+of+the+International+Joint+Conference+on+Automated+Reasoning%2C+2008%2E)
106. Laura Kovács and Andrei Voronkov. First-Order Theorem Proving and Vampire. In Proceedings of the International Conference on Computer Aided Verification, 2013. [find](https://scholar.google.com/scholar?q=Laura+Kova%CC%81cs+and+Andrei+Voronkov%2E+First%2DOrder+Theorem+Proving+and+Vampire%2E+In+Proceedings+of+the+International+Conference+on+Computer+Aided+Verification%2C+2013%2E)
107. Liubov Kovriguina, Roman Teucher, and Robert Wardenga. TextGraphs-16 Natural Language Premise Selection Task: Zero-Shot Premise Selection with Prompting Generative Language Models. In Proceedings of TextGraphs-16: Graph-Based Methods for Natural Language Processing, 2022. [find](https://scholar.google.com/scholar?q=Liubov+Kovriguina%2C+Roman+Teucher%2C+and+Robert+Wardenga%2E+TextGraphs%2D16+Natural+Language+Premise+Selection+Task%3A+Zero%2DShot+Premise+Selection+with+Prompting+Generative+Language+Models%2E+In+Proceedings+of+T)
108. Andrzej Stanisław Kucik and Konstantin Korovin. Premise Selection with Neural Networks and Distributed Representation of Features. arXiv preprint arXiv:1807.10268, 2018. — [arXiv:1807.10268](https://arxiv.org/abs/1807.10268) [find](https://scholar.google.com/scholar?q=Andrzej+Stanis%C5%82aw+Kucik+and+Konstantin+Korovin%2E+Premise+Selection+with+Neural+Networks+and+Distributed+Representation+of+Features%2E+arXiv+preprint+arXiv%3A1807%2E10268%2C+2018%2E+%E2%80%94+%5BarXiv%3A1807%2E10268%5D%28https%3A%2F%2Fa)
109. Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes. Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics. In Proceedings of the International Joint Conference on Automated Reasoning, 2012. [find](https://scholar.google.com/scholar?q=Daniel+Ku%CC%88hlwein%2C+Twan+van+Laarhoven%2C+Evgeni+Tsivtsivadze%2C+Josef+Urban%2C+and+Tom+Heskes%2E+Overview+and+Evaluation+of+Premise+Selection+Techniques+for+Large+Theory+Mathematics%2E+In+Proceedings+of+the+Inte)
110. Harsh Kumar, David M Rothschild, Daniel G Goldstein, and Jake M Hofman. Math Education with Large Language Models: Peril or Promise? SSRN Electronic Journal, 2023. [find](https://scholar.google.com/scholar?q=Harsh+Kumar%2C+David+M+Rothschild%2C+Daniel+G+Goldstein%2C+and+Jake+M+Hofman%2E+Math+Education+with+Large+Language+Models%3A+Peril+or+Promise%3F+SSRN+Electronic+Journal%2C+2023%2E)
111. Mitsuru Kusumoto, Keisuke Yahata, and Masahiro Sakai. [Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning](https://md.research.elamur.ai/free/en/papers/kusumoto-2018-automated-theorem-proving-intuitionistic-propositional/). arXiv preprint arXiv:1811.00796, 2018.
112. Sean Lamont, Michael Norrish, Amir Dezfouli, Christian Walder, and Paul Montague. BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving. In Proceedings of the AAAI Conference on Artificial Intelligence, 2024. [find](https://scholar.google.com/scholar?q=Sean+Lamont%2C+Michael+Norrish%2C+Amir+Dezfouli%2C+Christian+Walder%2C+and+Paul+Montague%2E+BAIT%3A+Benchmarking+%28Embedding%29+Architectures+for+Interactive+Theorem%2DProving%2E+In+Proceedings+of+the+AAAI+Conference+on)
113. Guillaume Lample and Alexis Conneau. Cross-Lingual Language Model Pretraining. In Proceedings of the International Conference on Neural Information Processing Systems, 2019. [find](https://scholar.google.com/scholar?q=Guillaume+Lample+and+Alexis+Conneau%2E+Cross%2DLingual+Language+Model+Pretraining%2E+In+Proceedings+of+the+International+Conference+on+Neural+Information+Processing+Systems%2C+2019%2E)
114. Guillaume Lample, Myle Ott, Alexis Conneau, Ludovic Denoyer, and Marc’Aurelio Ranzato. Phrase-Based & Neural Unsupervised Machine Translation. In Proceedings of the Conference on Empirical Methods in Natural Language Processing, 2018. [find](https://scholar.google.com/scholar?q=Guillaume+Lample%2C+Myle+Ott%2C+Alexis+Conneau%2C+Ludovic+Denoyer%2C+and+Marc%E2%80%99Aurelio+Ranzato%2E+Phrase%2DBased+%26+Neural+Unsupervised+Machine+Translation%2E+In+Proceedings+of+the+Conference+on+Empirical+Methods+in+)
115. Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. [Hypertree Proof Search for Neural Theorem Proving](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/). In Proceedings of the International Conference on Neural Information Processing Systems, 2022.
116. Dennis Lee, Christian Szegedy, Markus N Rabe, Sarah M Loos, and Kshitij Bansal. [Mathematical Reasoning in Latent Space](https://md.research.elamur.ai/free/en/papers/lee-2019-mathematical-reasoning-latent-space/). In Proceedings of the International Conference on Learning Representations, 2020.
117. Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. CompCert–A Formally Verified Optimizing Compiler. In Proceeding of the European Congress on Embedded Real Time Software and Systems, 2016. [find](https://scholar.google.com/scholar?q=Xavier+Leroy%2C+Sandrine+Blazy%2C+Daniel+Ka%CC%88stner%2C+Bernhard+Schommer%2C+Markus+Pister%2C+and+Christian+Ferdinand%2E+CompCert%E2%80%93A+Formally+Verified+Optimizing+Compiler%2E+In+Proceeding+of+the+European+Congress+on+Em)
118. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, et al. [Solving Quantitative Reasoning Problems with Language Models](https://md.research.elamur.ai/free/en/papers/lewkowycz-2022-solving-quantitative-reasoning-problems-language/). Proceedings of the International Conference on Neural Information Processing…
119. Weixian Waylon Li, Yftah Ziser, Maximin Coavoux, and Shay B Cohen. BERT Is Not The Count: Learning to Match Mathematical Statements with Proofs. In Proceedings of the Conference of the European Chapter of the Association for Computational Linguistics, 2023. [find](https://scholar.google.com/scholar?q=Weixian+Waylon+Li%2C+Yftah+Ziser%2C+Maximin+Coavoux%2C+and+Shay+B+Cohen%2E+BERT+Is+Not+The+Count%3A+Learning+to+Match+Mathematical+Statements+with+Proofs%2E+In+Proceedings+of+the+Conference+of+the+European+Chapte)
120. Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C Paulson. [IsarStep: A Benchmark for High-Level Mathematical Reasoning](https://md.research.elamur.ai/free/en/papers/li-2020-isarstep-benchmark-high-level-mathematical/). In Proceedings of the International Conference on Learning Representations, 2021a.
121. Zhaoyu Li, Binghong Chen, and Xujie Si. Graph Contrastive Pre-Training for Effective Theorem Reasoning. International Conference on Machine Learning Workshop on Self-Supervised Learning for Reasoning and Perception, 2021b. [find](https://scholar.google.com/scholar?q=Zhaoyu+Li%2C+Binghong+Chen%2C+and+Xujie+Si%2E+Graph+Contrastive+Pre%2DTraining+for+Effective+Theorem+Reasoning%2E+International+Conference+on+Machine+Learning+Workshop+on+Self%2DSupervised+Learning+for+Reasoning+)
122. Zhenwen Liang, Tianyu Yang, Jipeng Zhang, and Xiangliang Zhang. UniMath: A Foundational and Multimodal Mathematical Reasoner. In Proceedings of the Conference on Empirical Methods in Natural Language Processing, 2023. [find](https://scholar.google.com/scholar?q=Zhenwen+Liang%2C+Tianyu+Yang%2C+Jipeng+Zhang%2C+and+Xiangliang+Zhang%2E+UniMath%3A+A+Foundational+and+Multimodal+Mathematical+Reasoner%2E+In+Proceedings+of+the+Conference+on+Empirical+Methods+in+Natural+Language+)
123. Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. [Lean-STaR: Learning to Interleave Thinking and Proving](https://md.research.elamur.ai/free/en/papers/lin-2024-lean-star-learning-interleave-thinking/). arXiv preprint arXiv:2407.10040, 2024a.
124. Qika Lin, Jun Liu, Lingling Zhang, Yudai Pan, Xin Hu, Fangzhi Xu, and Hongwei Zeng. Contrastive Graph Representations for Logical Formulas Embedding. IEEE Transactions on Knowledge and Data Engineering, 2021. [find](https://scholar.google.com/scholar?q=Qika+Lin%2C+Jun+Liu%2C+Lingling+Zhang%2C+Yudai+Pan%2C+Xin+Hu%2C+Fangzhi+Xu%2C+and+Hongwei+Zeng%2E+Contrastive+Graph+Representations+for+Logical+Formulas+Embedding%2E+IEEE+Transactions+on+Knowledge+and+Data+Engineerin)
125. Xiaohan Lin, Qingxing Cao, Yinya Huang, Haiming Wang, Jianqiao Lu, Zhengying Liu, Linqi Song, and Xiaodan Liang. FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving. arXiv preprint arXiv:2406.14408, 2024b. — [arXiv:2406.14408](https://arxiv.org/abs/2406.14408) [find](https://scholar.google.com/scholar?q=Xiaohan+Lin%2C+Qingxing+Cao%2C+Yinya+Huang%2C+Haiming+Wang%2C+Jianqiao+Lu%2C+Zhengying+Liu%2C+Linqi+Song%2C+and+Xiaodan+Liang%2E+FVEL%3A+Interactive+Formal+Verification+Environment+with+Large+Language+Models+via+Theore)
126. Xiaohan Lin, Qingxing Cao, Yinya Huang, Zhicheng Yang, Zhengying Liu, Zhenguo Li, and Xiaodan Liang. ATG: Benchmarking Automated Theorem Generation for Generative Language Models. In Findings of the Association for Computational Linguistics: NAACL, 2024c. [find](https://scholar.google.com/scholar?q=Xiaohan+Lin%2C+Qingxing+Cao%2C+Yinya+Huang%2C+Zhicheng+Yang%2C+Zhengying+Liu%2C+Zhenguo+Li%2C+and+Xiaodan+Liang%2E+ATG%3A+Benchmarking+Automated+Theorem+Generation+for+Generative+Language+Models%2E+In+Findings+of+the+A)
127. Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. [FIMO: A Challenge Formal Dataset for Automated Theorem Proving](https://md.research.elamur.ai/free/en/papers/liu-2023-fimo-challenge-formal-dataset-automated/). arXiv preprint arXiv:2309.04295, 2023.
128. Qinghua Liu, Yang Xu, and Xingxing He. Attention Recurrent Cross-Graph Neural Network for Selecting Premises. International Journal of Machine Learning and Cybernetics, 2022a. [find](https://scholar.google.com/scholar?q=Qinghua+Liu%2C+Yang+Xu%2C+and+Xingxing+He%2E+Attention+Recurrent+Cross%2DGraph+Neural+Network+for+Selecting+Premises%2E+International+Journal+of+Machine+Learning+and+Cybernetics%2C+2022a%2E)
129. Yinhan Liu, Myle Ott, Naman Goyal, Jingfei Du, Mandar Joshi, Danqi Chen, Omer Levy, Mike Lewis, Luke Zettlemoyer, and Veselin Stoyanov. [RoBERTa: A Robustly Optimized BERT Pretraining Approach](https://md.research.elamur.ai/free/en/papers/liu-2019-roberta-robustly-optimized-bert-pretraining/). arXiv preprint arXiv:1907.11692, 2019.
130. Zhou Liu, Yujun Li, Zhengying Liu, Lin Li, and Zhenguo Li. Learning to Prove Trigonometric Identities. arXiv preprint arXiv:2207.06679, 2022b. — [arXiv:2207.06679](https://arxiv.org/abs/2207.06679) [find](https://scholar.google.com/scholar?q=Zhou+Liu%2C+Yujun+Li%2C+Zhengying+Liu%2C+Lin+Li%2C+and+Zhenguo+Li%2E+Learning+to+Prove+Trigonometric+Identities%2E+arXiv+preprint+arXiv%3A2207%2E06679%2C+2022b%2E+%E2%80%94+%5BarXiv%3A2207%2E06679%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2207%2E06679%29)
131. Evan Lohn and Sean Welleck. miniCodeProps: A Minimal Benchmark for Proving Code Properties. arXiv preprint arXiv:2406.11915, 2024. — [arXiv:2406.11915](https://arxiv.org/abs/2406.11915) [find](https://scholar.google.com/scholar?q=Evan+Lohn+and+Sean+Welleck%2E+miniCodeProps%3A+A+Minimal+Benchmark+for+Proving+Code+Properties%2E+arXiv+preprint+arXiv%3A2406%2E11915%2C+2024%2E+%E2%80%94+%5BarXiv%3A2406%2E11915%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2406%2E11915%29)
132. Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. [Deep Network Guided Proof Search](https://md.research.elamur.ai/free/en/papers/loos-2017-deep-network-guided-proof-search/). In Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2017.
133. László Lovász and Alexander Schrijver. Cones of Matrices and Set-Functions and 0–1 Optimization. SIAM journal on optimization, 1991. [find](https://scholar.google.com/scholar?q=La%CC%81szlo%CC%81+Lova%CC%81sz+and+Alexander+Schrijver%2E+Cones+of+Matrices+and+Set%2DFunctions+and+0%E2%80%931+Optimization%2E+SIAM+journal+on+optimization%2C+1991%2E)
134. Jianqiao Lu, Zhengying Liu, Yingjia Wan, Yinya Huang, Haiming Wang, Zhicheng Yang, Jing Tang, and Zhijiang Guo. [Process-Driven Autoformalization in Lean 4](https://md.research.elamur.ai/free/en/papers/lu-2024-process-driven-autoformalization-lean-4/). arXiv preprint arXiv:2406.01940, 2024.
135. Minh-Thang Luong, Eugene Brevdo, and Rui Zhao. Neural Machine Translation (seq2seq) Tutorial. [https://github.com/tensorflow/nmt](https://github.com/tensorflow/nmt), 2017. [↗](https://github.com/tensorflow/nmt)
136. The mathlib Community. [The Lean Mathematical Library](https://md.research.elamur.ai/free/en/papers/community-2019-lean-mathematical-library/). In Proceedings of the ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020.
137. Jack McKeown and Geoff Sutcliffe. Reinforcement Learning for Guiding the E Theorem Prover. In Proceedings of the International Florida Artificial Intelligence Research Society Conference, 2023. [find](https://scholar.google.com/scholar?q=Jack+McKeown+and+Geoff+Sutcliffe%2E+Reinforcement+Learning+for+Guiding+the+E+Theorem+Prover%2E+In+Proceedings+of+the+International+Florida+Artificial+Intelligence+Research+Society+Conference%2C+2023%2E)
138. Norman Megill and David A Wheeler. [Metamath: A Computer Language for Mathematical Proofs](https://md.research.elamur.ai/free/en/papers/megill-2019-metamath-computer-language-mathematical-proofs/). Lulu Press, 2019.
139. Maciej Mikuła, Szymon Antoniak, Szymon Tworkowski, Albert Q Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. [Magnushammer: A Transformer-Based Approach to Premise Selection](https://md.research.elamur.ai/free/en/papers/mikula-2023-magnushammer-transformer-based-approach-premise/). In Proceedings of the International Conference on Learning Representations, 2024.
140. Robin Milner. Implementation and Applications of Scott’s Logic for Computable Functions. In Proceedings of the ACM Conference on Proving Assertions about Programs, 1972. [find](https://scholar.google.com/scholar?q=Robin+Milner%2E+Implementation+and+Applications+of+Scott%E2%80%99s+Logic+for+Computable+Functions%2E+In+Proceedings+of+the+ACM+Conference+on+Proving+Assertions+about+Programs%2C+1972%2E)
141. Bhavana Dalvi Mishra, Oyvind Tafjord, and Peter Clark. Towards Teachable Reasoning Systems: Using a Dynamic Memory of User Feedback for Continual System Improvement. In Proceedings of the Conference on Empirical Methods in Natural Language Processing, 2022. [find](https://scholar.google.com/scholar?q=Bhavana+Dalvi+Mishra%2C+Oyvind+Tafjord%2C+and+Peter+Clark%2E+Towards+Teachable+Reasoning+Systems%3A+Using+a+Dynamic+Memory+of+User+Feedback+for+Continual+System+Improvement%2E+In+Proceedings+of+the+Conference+o)
142. Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Alex Graves, Ioannis Antonoglou, Daan Wierstra, and Martin Riedmiller. Playing Atari with Deep Reinforcement Learning. arXiv preprint arXiv:1312.5602, 2013. [find](https://scholar.google.com/scholar?q=Volodymyr+Mnih%2C+Koray+Kavukcuoglu%2C+David+Silver%2C+Alex+Graves%2C+Ioannis+Antonoglou%2C+Daan+Wierstra%2C+and+Martin+Riedmiller%2E+Playing+Atari+with+Deep+Reinforcement+Learning%2E+arXiv+preprint+arXiv%3A1312%2E5602%2C+)
143. Guangshuai Mo, Yan Xiong, Wenchao Huang, and Lu Ma. Automated Theorem Proving via Interacting with Proof Assistants by Dynamic Strategies. In Proceedings of the International Conference on Big Data Computing and Communications, 2020. [find](https://scholar.google.com/scholar?q=Guangshuai+Mo%2C+Yan+Xiong%2C+Wenchao+Huang%2C+and+Lu+Ma%2E+Automated+Theorem+Proving+via+Interacting+with+Proof+Assistants+by+Dynamic+Strategies%2E+In+Proceedings+of+the+International+Conference+on+Big+Data+Co)
144. Terufumi Morishita, Gaku Morio, Atsuki Yamaguchi, and Yasuhiro Sogawa. Learning Deductive Reasoning from Synthetic Corpus based on Formal Logic. In Proceedings of the International Conference on Machine Learning, 2023. [find](https://scholar.google.com/scholar?q=Terufumi+Morishita%2C+Gaku+Morio%2C+Atsuki+Yamaguchi%2C+and+Yasuhiro+Sogawa%2E+Learning+Deductive+Reasoning+from+Synthetic+Corpus+based+on+Formal+Logic%2E+In+Proceedings+of+the+International+Conference+on+Machi)
145. Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. In Proceedings of the International Conference on Automated Deduction, 2021. — [The Lean 4 Theorem Prover and Programming Language (System Description)](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/)
146. Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. [Autoformalizing Euclidean Geometry](https://md.research.elamur.ai/free/en/papers/murphy-2024-autoformalizing-euclidean-geometry/). In Proceedings of the International Conference on Machine Learning, 2024.
147. Theo X Olausson, Alex Gu, Benjamin Lipkin, Cedegao E Zhang, Armando Solar-Lezama, Joshua B Tenenbaum, and Roger Levy. [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://md.research.elamur.ai/free/en/papers/olausson-2023-linc-neurosymbolic-approach-logical-reasoning/). In Proceedings of the Conference on Empirical Methods in Natural Lan…
148. Miroslav Olšák, Cezary Kaliszyk, and Josef Urban. [Property Invariant Embedding for Automated Reasoning](https://md.research.elamur.ai/free/en/papers/olsak-2019-property-invariant-embedding-automated-reasoning/). In Proceedings of the European Conference on Artificial Intelligence, 2019.
149. Aaron van den Oord, Yazhe Li, and Oriol Vinyals. [Representation Learning with Contrastive Predictive Coding](https://md.research.elamur.ai/free/en/papers/oord-2018-representation-learning-contrastive-predictive-coding/). arXiv preprint arXiv:1807.03748, 2018.
150. Jens Otten and Wolfgang Bibel. leanCoP: Lean Connection-Based Theorem Proving. Journal of Symbolic Computation, 2003. [find](https://scholar.google.com/scholar?q=Jens+Otten+and+Wolfgang+Bibel%2E+leanCoP%3A+Lean+Connection%2DBased+Theorem+Proving%2E+Journal+of+Symbolic+Computation%2C+2003%2E)
151. Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy. [Graph Representations for Higher-Order Logic and Theorem Proving](https://md.research.elamur.ai/free/en/papers/paliwal-2019-graph-representations-higher-order-logic/). In Proceedings of the AAAI Conference on Artificial Intelligence, 2020.
152. Liangming Pan, Alon Albalak, Xinyi Wang, and William Yang Wang. [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://md.research.elamur.ai/free/en/papers/pan-2023-logic-lm-empowering-large-language/). In Findings of the Association for Computational Linguistics: EMNLP, 2023.
153. Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. [BLEU: A Method for Automatic Evaluation of Machine Translation](https://md.research.elamur.ai/free/en/papers/papineni-2002-bleu-method-automatic-evaluation-machine/). In Proceedings of the annual meeting of the Association for Computational Linguistics, 2002.
154. Keiran Paster, Marco Dos Santos, Zhangir Azerbayev, and Jimmy Ba. [OpenWebMath: An Open Dataset of High-Quality Mathematical Web Text](https://md.research.elamur.ai/free/en/papers/paster-2023-openwebmath-open-dataset-high-quality/). In Proceedings of the International Conference on Learning Representations, 2024.
155. Nilay Patel, Jeffrey Flanigan, and Rahul Saha. [A New Approach Towards Autoformalization](https://md.research.elamur.ai/free/en/papers/patel-2023-new-approach-towards-autoformalization/). arXiv preprint arXiv:2310.07957, 2023.
156. Lawrence C Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. [find](https://scholar.google.com/scholar?q=Lawrence+C+Paulson%2E+Isabelle%3A+A+Generic+Theorem+Prover%2E+Springer%2C+1994%2E)
157. Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin. Can Large Language Models Reason about Program Invariants? In Proceedings of the International Conference on Machine Learning, 2023. [find](https://scholar.google.com/scholar?q=Kexin+Pei%2C+David+Bieber%2C+Kensen+Shi%2C+Charles+Sutton%2C+and+Pengcheng+Yin%2E+Can+Large+Language+Models+Reason+about+Program+Invariants%3F+In+Proceedings+of+the+International+Conference+on+Machine+Learning%2C+2)
158. Kebin Peng and Dianfu Ma. Tree-Structure CNN for Automated Theorem Proving. In Proceedings of the International Conference on Neural Information Processing, 2017. [find](https://scholar.google.com/scholar?q=Kebin+Peng+and+Dianfu+Ma%2E+Tree%2DStructure+CNN+for+Automated+Theorem+Proving%2E+In+Proceedings+of+the+International+Conference+on+Neural+Information+Processing%2C+2017%2E)
159. Jelle Piepenbrock, Tom Heskes, Mikoláš Janota, and Josef Urban. Learning Equational Theorem Proving. In Proceedings of the Conference on Artificial Intelligence and Theorem Proving, 2021. [find](https://scholar.google.com/scholar?q=Jelle+Piepenbrock%2C+Tom+Heskes%2C+Mikola%CC%81s%CC%8C+Janota%2C+and+Josef+Urban%2E+Learning+Equational+Theorem+Proving%2E+In+Proceedings+of+the+Conference+on+Artificial+Intelligence+and+Theorem+Proving%2C+2021%2E)
160. Jelle Piepenbrock, Tom Heskes, Mikoláš Janota, and Josef Urban. Guiding An Automated Theorem Prover with Neural Rewriting. In Proceedings of the International Joint Conference on Automated Reasoning, 2022a. [find](https://scholar.google.com/scholar?q=Jelle+Piepenbrock%2C+Tom+Heskes%2C+Mikola%CC%81s%CC%8C+Janota%2C+and+Josef+Urban%2E+Guiding+An+Automated+Theorem+Prover+with+Neural+Rewriting%2E+In+Proceedings+of+the+International+Joint+Conference+on+Automated+Reasoning)
161. Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olšák, Tom Heskes, and Mikolaš Janota. Machine Learning Meets The Herbrand Universe. arXiv preprint arXiv:2210.03590, 2022b. — [arXiv:2210.03590](https://arxiv.org/abs/2210.03590) [find](https://scholar.google.com/scholar?q=Jelle+Piepenbrock%2C+Josef+Urban%2C+Konstantin+Korovin%2C+Miroslav+Ols%CC%8Ca%CC%81k%2C+Tom+Heskes%2C+and+Mikolas%CC%8C+Janota%2E+Machine+Learning+Meets+The+Herbrand+Universe%2E+arXiv+preprint+arXiv%3A2210%2E03590%2C+2022b%2E+%E2%80%94+%5BarXiv%3A22)
162. Bartosz Piotrowski and Josef Urban. [Stateful Premise Selection by Recurrent Neural Networks](https://md.research.elamur.ai/free/en/papers/piotrowski-2020-stateful-premise-selection-recurrent-neural/). In Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2020a.
163. Bartosz Piotrowski and Josef Urban. [Guiding Inferences in Connection Tableau by Recurrent Neural Networks](https://md.research.elamur.ai/free/en/papers/piotrowski-2019-guiding-inferences-connection-tableau-recurrent/). In Proceedings of the International Conference on Intelligent Computer Mathematics, 2020b.
164. Gabriel Poesia, David Broman, Nick Haber, and Noah D Goodman. [Learning formal mathematics from intrinsic motivation](https://md.research.elamur.ai/free/en/papers/poesia-2024-learning-formal-mathematics-intrinsic-motivation/). arXiv preprint arXiv:2407.00695, 2024.
165. Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bosselut. Improving Autoformalization using Type Checking. arXiv preprint arXiv:2406.07222, 2024. [find](https://scholar.google.com/scholar?q=Auguste+Poiroux%2C+Gail+Weiss%2C+Viktor+Kunc%CC%8Cak%2C+and+Antoine+Bosselut%2E+Improving+Autoformalization+using+Type+Checking%2E+arXiv+preprint+arXiv%3A2406%2E07222%2C+2024%2E)
166. Stanislas Polu and Ilya Sutskever. [Generative Language Modeling for Automated Theorem Proving](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/). arXiv preprint arXiv:2009.03393, 2020.
167. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. [Formal Mathematics Statement Curriculum Learning](https://md.research.elamur.ai/free/en/papers/polu-2022-formal-mathematics-statement-curriculum-learning/). In Proceedings of the International Conference on Learning Representations, 2023.
168. Seth Poulsen, Sami Sarsa, James Prather, Juho Leinonen, Brett A Becker, Arto Hellas, Paul Denny, and Brent N Reeves. Solving Proof Block Problems Using Large Language Models. In Proceedings of the ACM Technical Symposium on Computer Science Education, 2024. [find](https://scholar.google.com/scholar?q=Seth+Poulsen%2C+Sami+Sarsa%2C+James+Prather%2C+Juho+Leinonen%2C+Brett+A+Becker%2C+Arto+Hellas%2C+Paul+Denny%2C+and+Brent+N+Reeves%2E+Solving+Proof+Block+Problems+Using+Large+Language+Models%2E+In+Proceedings+of+the+ACM)
169. Krsto Proroković, Michael Wand, and Jürgen Schmidhuber. Improving Stateful Premise Selection with Transformers. In Proceedings of the International Conference on Intelligent Computer Mathematics, 2021. [find](https://scholar.google.com/scholar?q=Krsto+Prorokovic%CC%81%2C+Michael+Wand%2C+and+Ju%CC%88rgen+Schmidhuber%2E+Improving+Stateful+Premise+Selection+with+Transformers%2E+In+Proceedings+of+the+International+Conference+on+Intelligent+Computer+Mathematics%2C+20)
170. Xin Quan, Marco Valentino, Louise A Dennis, and André Freitas. [Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving](https://md.research.elamur.ai/free/en/papers/quan-2024-verification-refinement-natural-language-explanations/). arXiv preprint arXiv:2405.01379, 2024.
171. Markus N Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. [Mathematical Reasoning via Self-Supervised Skip-Tree Training](https://md.research.elamur.ai/free/en/papers/rabe-2020-mathematical-reasoning-self-supervised-skip/). In Proceedings of the International Conference on Learning Representations, 2021.
172. Michael Rawson and Giles Reger. A Neurally-Guided, Parallel Theorem Prover. In Proceedings of the International Symposium on Frontiers of Combining Systems, 2019. [find](https://scholar.google.com/scholar?q=Michael+Rawson+and+Giles+Reger%2E+A+Neurally%2DGuided%2C+Parallel+Theorem+Prover%2E+In+Proceedings+of+the+International+Symposium+on+Frontiers+of+Combining+Systems%2C+2019%2E)
173. Michael Rawson and Giles Reger. Directed Graph Networks for Logical Reasoning (Extended Abstract). In Joint Proceedings of the Workshop on Practical Aspects of Automated Reasoning (PAAR) and the Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020. [find](https://scholar.google.com/scholar?q=Michael+Rawson+and+Giles+Reger%2E+Directed+Graph+Networks+for+Logical+Reasoning+%28Extended+Abstract%29%2E+In+Joint+Proceedings+of+the+Workshop+on+Practical+Aspects+of+Automated+Reasoning+%28PAAR%29+and+the+Satis)
174. Michael Rawson and Giles Reger. lazyCoP: Lazy Paramodulation Meets Neurally Guided Search. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 2021. [find](https://scholar.google.com/scholar?q=Michael+Rawson+and+Giles+Reger%2E+lazyCoP%3A+Lazy+Paramodulation+Meets+Neurally+Guided+Search%2E+In+Proceedings+of+the+International+Conference+on+Automated+Reasoning+with+Analytic+Tableaux+and+Related+Meth)
175. Tom Reichel, R Henderson, Andrew Touchet, Andrew Gardner, and Talia Ringer. Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset. In Proceedings of the International Conference on Interactive Theorem Proving, 2023. [find](https://scholar.google.com/scholar?q=Tom+Reichel%2C+R+Henderson%2C+Andrew+Touchet%2C+Andrew+Gardner%2C+and+Talia+Ringer%2E+Proof+Repair+Infrastructure+for+Supervised+Models%3A+Building+a+Large+Proof+Repair+Dataset%2E+In+Proceedings+of+the+Internationa)
176. Stephen Robertson, Hugo Zaragoza, et al. The Probabilistic Relevance Framework: BM25 and Beyond. Foundations and Trends® in Information Retrieval, 2009. [find](https://scholar.google.com/scholar?q=Stephen+Robertson%2C+Hugo+Zaragoza%2C+et+al%2E+The+Probabilistic+Relevance+Framework%3A+BM25+and+Beyond%2E+Foundations+and+Trends%C2%AE+in+Information+Retrieval%2C+2009%2E)
177. Piotr Rudnicki. An Overview of the Mizar Project. In Proceedings of the Workshop on Types for Proofs and Programs, 1992. [find](https://scholar.google.com/scholar?q=Piotr+Rudnicki%2E+An+Overview+of+the+Mizar+Project%2E+In+Proceedings+of+the+Workshop+on+Types+for+Proofs+and+Programs%2C+1992%2E)
178. Jason Rute, Miroslav Olšák, Lasse Blaauwbroek, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun. [Graph2Tac: Online Representation Learning of Formal Math Concepts](https://md.research.elamur.ai/free/en/papers/blaauwbroek-2024-graph2tac-online-representation-learning-formal/). In Proceedings of the International Conference on Machine Learning, 2024.
179. Swarnadeep Saha, Sayan Ghosh, Shashank Srivastava, and Mohit Bansal. [PRover: Proof Generation for Interpretable Reasoning over Rules](https://md.research.elamur.ai/free/en/papers/saha-2020-prover-proof-generation-interpretable-reasoning/). In Proceedings of the Conference on Empirical Methods in Natural Language Processing, 2020.
180. Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner. [Generating Correctness Proofs with Neural Networks](https://md.research.elamur.ai/free/en/papers/stern-2019-generating-correctness-proofs-neural-networks/). In Proceedings of the ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, 2020.
181. Alex Sanchez-Stern, Emily First, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, and Talia Ringer. [Passport: Improving Automated Formal Verification Using Identifiers](https://md.research.elamur.ai/free/en/papers/stern-2022-passport-improving-automated-formal-verification/). ACM Transactions on Programming Languages and Systems, 2023.
182. Soumya Sanyal, Harman Singh, and Xiang Ren. FaiRR: Faithful and Robust Deductive Reasoning over Natural Language. In Proceedings of the Annual Meeting of the Association for Computational Linguistics, 2022. [find](https://scholar.google.com/scholar?q=Soumya+Sanyal%2C+Harman+Singh%2C+and+Xiang+Ren%2E+FaiRR%3A+Faithful+and+Robust+Deductive+Reasoning+over+Natural+Language%2E+In+Proceedings+of+the+Annual+Meeting+of+the+Association+for+Computational+Linguistics%2C)
183. Abulhair Saparov and He He. [Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought](https://md.research.elamur.ai/free/en/papers/saparov-2022-language-models-greedy-reasoners-systematic/). In Proceedings of the International Conference on Learning Representations, 2023.
184. Gregor vom Scheidt. Experimental Results from Applying GPT-4 to An Unpublished Formal Language. arXiv preprint arXiv:2305.12196, 2023. — [arXiv:2305.12196](https://arxiv.org/abs/2305.12196) [find](https://scholar.google.com/scholar?q=Gregor+vom+Scheidt%2E+Experimental+Results+from+Applying+GPT%2D4+to+An+Unpublished+Formal+Language%2E+arXiv+preprint+arXiv%3A2305%2E12196%2C+2023%2E+%E2%80%94+%5BarXiv%3A2305%2E12196%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2305%2E12196%29)
185. Stephan Schulz. E–A Brainiac Theorem Prover. AI Communications, 2002. [find](https://scholar.google.com/scholar?q=Stephan+Schulz%2E+E%E2%80%93A+Brainiac+Theorem+Prover%2E+AI+Communications%2C+2002%2E)
186. Johann M Schumann. Automated Theorem Proving in Software Engineering. Springer Science & Business Media, 2001. [find](https://scholar.google.com/scholar?q=Johann+M+Schumann%2E+Automated+Theorem+Proving+in+Software+Engineering%2E+Springer+Science+%26+Business+Media%2C+2001%2E)
187. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, YK Li, Y Wu, and Daya Guo. [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://md.research.elamur.ai/free/en/papers/shao-2024-deepseekmath-pushing-limits-mathematical-reasoning/). arXiv preprint arXiv:2402.03300, 2024.
188. Boris Shminke. gym-saturation: Gymnasium Environments for Saturation Provers (System description). In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 2023. [find](https://scholar.google.com/scholar?q=Boris+Shminke%2E+gym%2Dsaturation%3A+Gymnasium+Environments+for+Saturation+Provers+%28System+description%29%2E+In+Proceedings+of+the+International+Conference+on+Automated+Reasoning+with+Analytic+Tableaux+and+Rela)
189. David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al. A General Reinforcement Learning Algorithm That Masters Chess, Shogi, and Go Through Self-Play. Science, 2018. [find](https://scholar.google.com/scholar?q=David+Silver%2C+Thomas+Hubert%2C+Julian+Schrittwieser%2C+Ioannis+Antonoglou%2C+Matthew+Lai%2C+Arthur+Guez%2C+Marc+Lanctot%2C+Laurent+Sifre%2C+Dharshan+Kumaran%2C+Thore+Graepel%2C+et+al%2E+A+General+Reinforcement+Learning+A)
190. Kaitao Song, Xu Tan, Tao Qin, Jianfeng Lu, and Tie-Yan Liu. [MPNet: Masked and Permuted Pre-Training for Language Understanding](https://md.research.elamur.ai/free/en/papers/song-2020-mpnet-masked-permuted-pre-training/). In Proceedings of the International Conference on Neural Information Processing Systems, 2020.
191. Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards Large Language Models as Copilots for Theorem Proving in Lean. arXiv preprint arXiv:2404.[12534, 2024](https://md.research.elamur.ai/free/en/papers/song-2024-lean-copilot-large-language-models/).
192. Henrik Kragh Sørensen, Mikkel Willum Johansen, Renee Hoekzema, and Hester Breman. Augmenting the Human Mathematician. In International Conference on Learning Representations Workshop on Mathematical Reasoning in General Artificial Intelligence, 2021. [find](https://scholar.google.com/scholar?q=Henrik+Kragh+S%C3%B8rensen%2C+Mikkel+Willum+Johansen%2C+Renee+Hoekzema%2C+and+Hester+Breman%2E+Augmenting+the+Human+Mathematician%2E+In+International+Conference+on+Learning+Representations+Workshop+on+Mathematical+R)
193. Martin Suda. Vampire with a Brain Is a Good ITP Hammer. In Proceedings of the International Symposium on Frontiers of Combining Systems, 2021a. [find](https://scholar.google.com/scholar?q=Martin+Suda%2E+Vampire+with+a+Brain+Is+a+Good+ITP+Hammer%2E+In+Proceedings+of+the+International+Symposium+on+Frontiers+of+Combining+Systems%2C+2021a%2E)
194. Martin Suda. Improving ENIGMA-Style Clause Selection While Learning From History. In Proceedings of the International Conference on Automated Deduction, 2021b. [find](https://scholar.google.com/scholar?q=Martin+Suda%2E+Improving+ENIGMA%2DStyle+Clause+Selection+While+Learning+From+History%2E+In+Proceedings+of+the+International+Conference+on+Automated+Deduction%2C+2021b%2E)
195. Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. [Clover: Closed-Loop Verifiable Code Generation](https://md.research.elamur.ai/free/en/papers/sun-2024-clover-closed-loop-verifiable-code/). arXiv preprint arXiv:2310.17807, 2023.
196. Geoff Sutcliffe. The TPTP Problem Library and Associated Infrastructure. Journal of Automated Reasoning, 2017. [find](https://scholar.google.com/scholar?q=Geoff+Sutcliffe%2E+The+TPTP+Problem+Library+and+Associated+Infrastructure%2E+Journal+of+Automated+Reasoning%2C+2017%2E)
197. Ilya Sutskever, Oriol Vinyals, and Quoc V Le. [Sequence to Sequence Learning with Neural Networks](https://md.research.elamur.ai/free/en/papers/sutskever-2014-sequence-sequence-learning-neural-networks/). In Proceedings of the International Conference on Neural Information Processing Systems, 2014.
198. Christian Suttner and Wolfgang Ertel. Automatic Acquisition of Search Guiding Heuristics. In Proceedings of the International Conference on Automated Deduction, 1990. [find](https://scholar.google.com/scholar?q=Christian+Suttner+and+Wolfgang+Ertel%2E+Automatic+Acquisition+of+Search+Guiding+Heuristics%2E+In+Proceedings+of+the+International+Conference+on+Automated+Deduction%2C+1990%2E)
199. Richard S Sutton, David McAllester, Satinder Singh, and Yishay Mansour. Policy Gradient Methods for Reinforcement Learning with Function Approximation. In Proceedings of the International Conference on Neural Information Processing Systems, 1999. [find](https://scholar.google.com/scholar?q=Richard+S+Sutton%2C+David+McAllester%2C+Satinder+Singh%2C+and+Yishay+Mansour%2E+Policy+Gradient+Methods+for+Reinforcement+Learning+with+Function+Approximation%2E+In+Proceedings+of+the+International+Conference+o)
200. Christian Szegedy. A Promising Path Towards Autoformalization and General Artificial Intelligence. In Proceedings of the International Conference on Intelligent Computer Mathematics, 2020. [find](https://scholar.google.com/scholar?q=Christian+Szegedy%2E+A+Promising+Path+Towards+Autoformalization+and+General+Artificial+Intelligence%2E+In+Proceedings+of+the+International+Conference+on+Intelligent+Computer+Mathematics%2C+2020%2E)
201. Christian Szegedy, Markus Rabe, and Henryk Michalewski. Retrieval-Augmented Proof Step Synthesis. In Proceedings of the Conference on Artificial Intelligence and Theorem Proving, 2021. [find](https://scholar.google.com/scholar?q=Christian+Szegedy%2C+Markus+Rabe%2C+and+Henryk+Michalewski%2E+Retrieval%2DAugmented+Proof+Step+Synthesis%2E+In+Proceedings+of+the+Conference+on+Artificial+Intelligence+and+Theorem+Proving%2C+2021%2E)
202. Oyvind Tafjord, Bhavana Dalvi Mishra, and Peter Clark. [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://md.research.elamur.ai/free/en/papers/tafjord-2021-proofwriter-generating-implications-proofs-abductive/). In Findings of the Association for Computational Linguistics: ACL-IJCNLP, 2021.
203. Oyvind Tafjord, Bhavana Dalvi Mishra, and Peter Clark. [Entailer: Answering Questions with Faithful and Truthful Chains of Reasoning](https://md.research.elamur.ai/free/en/papers/tafjord-2022-entailer-answering-questions-faithful/). In Proceedings of the Conference on Empirical Methods in Natural Language Processing, 2022.
204. Kai Sheng Tai, Richard Socher, and Christopher D Manning. Improved Semantic Representations From Tree-Structured Long Short-Term Memory Networks. In Proceedings of the Annual Meeting of the Association for Computational Linguistics and the International Joint Conference on Natural Language Processin… [find](https://scholar.google.com/scholar?q=Kai+Sheng+Tai%2C+Richard+Socher%2C+and+Christopher+D+Manning%2E+Improved+Semantic+Representations+From+Tree%2DStructured+Long+Short%2DTerm+Memory+Networks%2E+In+Proceedings+of+the+Annual+Meeting+of+the+Associatio)
205. Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. [An In-Context Learning Agent for Formal Theorem-Proving](https://md.research.elamur.ai/free/en/papers/thakur-2023-context-learning-agent-formal-theorem/). arXiv preprint arXiv:2310.04353, 2024.
206. Thi Hong Hanh Tran, Matej Martinc, Antoine Doucet, and Senja Pollak. IJS at TextGraphs-16 Natural Language Premise Selection Task: Will Contextual Information Improve Natural Language Premise Selection? In Proceedings of TextGraphs-16: Graph-Based Methods for Natural Language Processing, 2022. [find](https://scholar.google.com/scholar?q=Thi+Hong+Hanh+Tran%2C+Matej+Martinc%2C+Antoine+Doucet%2C+and+Senja+Pollak%2E+IJS+at+TextGraphs%2D16+Natural+Language+Premise+Selection+Task%3A+Will+Contextual+Information+Improve+Natural+Language+Premise+Selectio)
207. Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. [Solving Olympiad Geometry without Human Demonstrations](https://md.research.elamur.ai/free/en/papers/trinh-2024-solving-olympiad-geometry-without-human/). Nature, 2024.
208. Paul Trust, Provia Kadusabe, Haseeb Younis, Rosane Minghim, Evangelos Milios, and Ahmed Zahran. UNLPS at TextGraphs 2022 Shared Task: Unsupervised Natural Language Premise Selection in Mathematical Texts Using Sentence-MPNet. In Proceedings of TextGraphs-16: Graph-Based Methods for Natural Language… [find](https://scholar.google.com/scholar?q=Paul+Trust%2C+Provia+Kadusabe%2C+Haseeb+Younis%2C+Rosane+Minghim%2C+Evangelos+Milios%2C+and+Ahmed+Zahran%2E+UNLPS+at+TextGraphs+2022+Shared+Task%3A+Unsupervised+Natural+Language+Premise+Selection+in+Mathematical+Te)
209. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. [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/). arXiv preprint arXiv:2407.11214, 2024.
210. Szymon Tworkowski, Maciej Mikuła, Tomasz Odrzygóźdź, Konrad Czechowski, Szymon Antoniak, Albert Jiang, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. Formal Premise Selection With Language Models. In Proceedings of the Conference on Artificial Intelligence and Theorem Proving,… [find](https://scholar.google.com/scholar?q=Szymon+Tworkowski%2C+Maciej+Miku%C5%82a%2C+Tomasz+Odrzygo%CC%81z%CC%81dz%CC%81%2C+Konrad+Czechowski%2C+Szymon+Antoniak%2C+Albert+Jiang%2C+Christian+Szegedy%2C+%C5%81ukasz+Kucin%CC%81ski%2C+Piotr+Mi%C5%82os%CC%81%2C+and+Yuhuai+Wu%2E+Formal+Premise+Selection+Wit)
211. Josef Urban and Jan Jakubüv. [First Neural Conjecturing Datasets and Experiments](https://md.research.elamur.ai/free/en/papers/urban-2020-first-neural-conjecturing-datasets-experiments/). In Proceedings of the International Conference on Intelligent Computer Mathematics, 2020.
212. Josef Urban, Jiřı́ Vyskočil, and Petr Štěpánek. MaLeCoP Machine Learning Connection Prover. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 2011. [find](https://scholar.google.com/scholar?q=Josef+Urban%2C+Jir%CC%8C%C4%B1%CC%81+Vyskoc%CC%8Cil%2C+and+Petr+S%CC%8Cte%CC%8Cpa%CC%81nek%2E+MaLeCoP+Machine+Learning+Connection+Prover%2E+In+Proceedings+of+the+International+Conference+on+Automated+Reasoning+with+Analytic+Tableaux+and+Relate)
213. Aaron Van Den Oord, Sander Dieleman, Heiga Zen, Karen Simonyan, Oriol Vinyals, Alex Graves, Nal Kalchbrenner, Andrew Senior, Koray Kavukcuoglu, et al. [WaveNet: A Generative Model for Raw Audio](https://md.research.elamur.ai/free/en/papers/oord-2016-wavenet-generative-model-raw-audio/). arXiv preprint arXiv:1609.03499, 2016.
214. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. [Attention is All You Need](https://md.research.elamur.ai/free/en/papers/vaswani-2017-attention-all-need/). In Proceedings of the International Conference on Neural Information Processing Systems, 2017.
215. Petar Veličković, Guillem Cucurull, Arantxa Casanova, Adriana Romero, Pietro Lio, and Yoshua Bengio. Graph Attention Networks. In Proceedings of the International Conference on Learning Representations, 2018. [find](https://scholar.google.com/scholar?q=Petar+Velic%CC%8Ckovic%CC%81%2C+Guillem+Cucurull%2C+Arantxa+Casanova%2C+Adriana+Romero%2C+Pietro+Lio%2C+and+Yoshua+Bengio%2E+Graph+Attention+Networks%2E+In+Proceedings+of+the+International+Conference+on+Learning+Representati)
216. Rahul Vishwakarma and Subhankar Mishra. Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method. arXiv preprint arXiv:2312.14188, 2023. — [arXiv:2312.14188](https://arxiv.org/abs/2312.14188) [find](https://scholar.google.com/scholar?q=Rahul+Vishwakarma+and+Subhankar+Mishra%2E+Enhancing+Neural+Theorem+Proving+through+Data+Augmentation+and+Dynamic+Sampling+Method%2E+arXiv+preprint+arXiv%3A2312%2E14188%2C+2023%2E+%E2%80%94+%5BarXiv%3A2312%2E14188%5D%28https%3A%2F%2Farxi)
217. Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, et al. [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/). In Proceedings of the Annual Meeting of the Association for Computational Ling…
218. Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang, Jian Yin, Zhenguo Li, et al. [Proving Theorems Recursively](https://md.research.elamur.ai/free/en/papers/wang-2024-proving-theorems-recursively/). arXiv preprint arXiv:2405.14414, 2024.
219. Mingzhe Wang and Jia Deng. [Learning to Prove Theorems by Learning to Generate Theorems](https://md.research.elamur.ai/free/en/papers/wang-2020-learning-prove-theorems-learning-generate/). In Proceedings of the International Conference on Neural Information Processing Systems, 2020.
220. Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. [Premise Selection for Theorem Proving by Deep Graph Embedding](https://md.research.elamur.ai/free/en/papers/wang-2017-premise-selection-theorem-proving-deep/). In Proceedings of the International Conference on Neural Information Processing Systems, 2017.
221. Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. [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/). In Proceedings of the International Conference on Intelligent Computer Mathematics, 2018.
222. Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. [Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar](https://md.research.elamur.ai/free/en/papers/wang-2019-exploration-neural-machine-translation-autoformalization/). In Proceedings of the ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020.
223. Zengzhi Wang, Rui Xia, and Pengfei Liu. Generative AI for Math: Part I–[MathPile: A Billion-Token-Scale Pretraining Corpus for Math](https://md.research.elamur.ai/free/en/papers/wang-2023-mathpile-billion-token-scale-pretraining/). arXiv preprint arXiv:2312.17120, 2023b.
224. Chenrui Wei, Mengzhou Sun, and Wei Wang. [Proving Olympiad Algebraic Inequalities without Human Demonstrations](https://md.research.elamur.ai/free/en/papers/wei-2024-proving-olympiad-algebraic-inequalities-without/). arXiv preprint arXiv:2406.14219, 2024.
225. Sean Welleck and Rahul Saha. [LLMSTEP: LLM Proofstep Suggestions in Lean](https://md.research.elamur.ai/free/en/papers/welleck-2023-llmstep-llm-proofstep-suggestions-lean/). In International Conference on Neural Information Processing Systems Workshop on MATH-AI, 2023.
226. Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://md.research.elamur.ai/free/en/papers/welleck-2021-naturalproofs-mathematical-theorem-proving-natural/). In Proceedings of the International Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2021.
227. Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. [NaturalProver: Grounded Mathematical Proof Generation with Language Models](https://md.research.elamur.ai/free/en/papers/welleck-2022-naturalprover-grounded-mathematical-proof-generation/). In Proceedings of the International Conference on Neural Information Processing Systems, 2022.
228. Daniel Whalen. [Holophrasm: A Neural Automated Theorem Prover for Higher-Order Logic](https://md.research.elamur.ai/free/en/papers/whalen-2016-holophrasm-neural-automated-theorem-prover/). arXiv preprint arXiv:1608.02644, 2016.
229. Minchao Wu and Yuhuai Wu. Latent Action Space for Efficient Planning in Theorem Proving. In Proceedings of the Conference on Artificial Intelligence and Theorem Proving, 2021. [find](https://scholar.google.com/scholar?q=Minchao+Wu+and+Yuhuai+Wu%2E+Latent+Action+Space+for+Efficient+Planning+in+Theorem+Proving%2E+In+Proceedings+of+the+Conference+on+Artificial+Intelligence+and+Theorem+Proving%2C+2021%2E)
230. Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli. [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://md.research.elamur.ai/free/en/papers/wu-2021-tacticzero-learning-prove-theorems-scratch/). Proceedings of the International Conference on Neural Information Processing Systems, 2021a.
231. Yuhuai Wu, Albert Q Jiang, Jimmy Ba, and Roger Grosse. [INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving](https://md.research.elamur.ai/free/en/papers/wu-2020-int-inequality-benchmark-evaluating-generalization/). In Proceedings of the International Conference on Learning Representations, 2021b.
232. Yuhuai Wu, Markus N Rabe, Wenda Li, Jimmy Ba, Roger B Grosse, and Christian Szegedy. [LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning](https://md.research.elamur.ai/free/en/papers/wu-2021-lime-learning-inductive-bias-primitives/). In Proceedings of the International Conference on Machine Learning, 2021c.
233. Yuhuai Wu, Albert Q Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. [Autoformalization with Large Language Models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/). In Proceedings of the International Conference on Neural Information Processing Systems, 2022.
234. Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen. [Lean-github: Compiling github lean repositories for a versatile lean prover](https://md.research.elamur.ai/free/en/papers/wu-2024-lean-github-compiling-github-lean/). arXiv preprint arXiv:2407.17227, 2024.
235. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-advancing-theorem-proving/). arXiv preprint arXiv:2405.14333, 2024a.
236. Huajian Xin, Haiming Wang, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://md.research.elamur.ai/free/en/papers/wang-2023-lego-prover-neural-theorem-proving/). In Proceedings of the International Conference on Learning Representations, 2024b.
237. Jing Xiong, Jianhao Shen, Ye Yuan, Haiming Wang, Yichun Yin, Zhengying Liu, Lin Li, Zhijiang Guo, Qingxing Cao, Yinya Huang, et al. [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/). In Proceedings of the Conference on Empirical Methods in Natural Language Proces…
238. Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. [How Powerful are Graph Neural Networks?](https://md.research.elamur.ai/free/en/papers/xu-2018-powerful-graph-neural-networks/) In Proceedings of the International Conference on Learning Representations, 2019.
239. Linting Xue, Aditya Barua, Noah Constant, Rami Al-Rfou, Sharan Narang, Mihir Kale, Adam Roberts, and Colin Raffel. ByT5: Towards a Token-Free Future with Pre-trained Byte-to-Byte Models. Transactions of the Association for Computational Linguistics, 2022. [find](https://scholar.google.com/scholar?q=Linting+Xue%2C+Aditya+Barua%2C+Noah+Constant%2C+Rami+Al%2DRfou%2C+Sharan+Narang%2C+Mihir+Kale%2C+Adam+Roberts%2C+and+Colin+Raffel%2E+ByT5%3A+Towards+a+Token%2DFree+Future+with+Pre%2Dtrained+Byte%2Dto%2DByte+Models%2E+Transactions+)
240. Kaiyu Yang and Jia Deng. [Learning to Prove Theorems via Interacting with Proof Assistants](https://md.research.elamur.ai/free/en/papers/yang-2019-learning-prove-theorems-interacting-proof/). In Proceedings of the International Conference on Machine Learning, 2019.
241. Kaiyu Yang, Jia Deng, and Danqi Chen. Generating Natural Language Proofs with Verifier-Guided Search. In Proceedings of the Conference on Empirical Methods in Natural Language Processing, 2022. [find](https://scholar.google.com/scholar?q=Kaiyu+Yang%2C+Jia+Deng%2C+and+Danqi+Chen%2E+Generating+Natural+Language+Proofs+with+Verifier%2DGuided+Search%2E+In+Proceedings+of+the+Conference+on+Empirical+Methods+in+Natural+Language+Processing%2C+2022%2E)
242. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/). In Proceedings of the International Conference on Neural Information Processing Systems, 2023.
243. Jianan Yao, Ziqiao Zhou, Weiteng Chen, and Weidong Cui. Leveraging Large Language Models for Automated Proof Synthesis in Rust. arXiv preprint arXiv:2311.03739, 2023. [find](https://scholar.google.com/scholar?q=Jianan+Yao%2C+Ziqiao+Zhou%2C+Weiteng+Chen%2C+and+Weidong+Cui%2E+Leveraging+Large+Language+Models+for+Automated+Proof+Synthesis+in+Rust%2E+arXiv+preprint+arXiv%3A2311%2E03739%2C+2023%2E)
244. Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. [SATLM: Satisfiability-Aided Language Models using Declarative Prompting](https://md.research.elamur.ai/free/en/papers/ye-2023-satlm-satisfiability-aided-language-models/). In Proceedings of the International Conference on Neural Information Processing Systems, 2023.
245. Eric Yeh, Briland Hitaj, Sam Owre, Maena Quemener, and Natarajan Shankar. CoProver: A Recommender System for Proof Construction. In Proceedings of the International Conference on Intelligent Computer Mathematics, 2023. [find](https://scholar.google.com/scholar?q=Eric+Yeh%2C+Briland+Hitaj%2C+Sam+Owre%2C+Maena+Quemener%2C+and+Natarajan+Shankar%2E+CoProver%3A+A+Recommender+System+for+Proof+Construction%2E+In+Proceedings+of+the+International+Conference+on+Intelligent+Computer+)
246. Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. [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/). arXiv preprint arXiv:2406.03847, 2024a.
247. Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, et al. [InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning](https://md.research.elamur.ai/free/en/papers/ying-2024-internlm-math-open-math-large/). arXiv preprint arXiv:2402.06332, 2024b.
248. Roozbeh Yousefzadeh and Xuenan Cao. Large Language Models’ Understanding of Math: Source Criticism and Extrapolation. arXiv preprint arXiv:2311.07618, 2023. [find](https://scholar.google.com/scholar?q=Roozbeh+Yousefzadeh+and+Xuenan+Cao%2E+Large+Language+Models%E2%80%99+Understanding+of+Math%3A+Source+Criticism+and+Extrapolation%2E+arXiv+preprint+arXiv%3A2311%2E07618%2C+2023%2E)
249. Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, and Josef Urban. Learning Proof Transformations and Its Applications in Interactive Theorem Proving. In Proceedings of the International Symposium on Frontiers of Combining Systems, 2023a. [find](https://scholar.google.com/scholar?q=Liao+Zhang%2C+Lasse+Blaauwbroek%2C+Cezary+Kaliszyk%2C+and+Josef+Urban%2E+Learning+Proof+Transformations+and+Its+Applications+in+Interactive+Theorem+Proving%2E+In+Proceedings+of+the+International+Symposium+on+Fr)
250. Lichen Zhang, Shuai Lu, and Nan Duan. Selene: Pioneering Automated Proof in Software Verification. In Proceedings of the Annual Meeting of the Association for Computational Linguistics, 2024. [find](https://scholar.google.com/scholar?q=Lichen+Zhang%2C+Shuai+Lu%2C+and+Nan+Duan%2E+Selene%3A+Pioneering+Automated+Proof+in+Software+Verification%2E+In+Proceedings+of+the+Annual+Meeting+of+the+Association+for+Computational+Linguistics%2C+2024%2E)
251. Shizhuo Dylan Zhang, Talia Ringer, and Emily First. Getting More out of Large Language Models for Proofs. In Proceedings of the Conference on Artificial Intelligence and Theorem Proving, 2023b. [find](https://scholar.google.com/scholar?q=Shizhuo+Dylan+Zhang%2C+Talia+Ringer%2C+and+Emily+First%2E+Getting+More+out+of+Large+Language+Models+for+Proofs%2E+In+Proceedings+of+the+Conference+on+Artificial+Intelligence+and+Theorem+Proving%2C+2023b%2E)
252. Xueliang Zhao, Wenda Li, and Lingpeng Kong. Subgoal-Based Demonstration Learning for Formal Theorem Proving. In Proceedings of the International Conference on Machine Learning, 2024. [find](https://scholar.google.com/scholar?q=Xueliang+Zhao%2C+Wenda+Li%2C+and+Lingpeng+Kong%2E+Subgoal%2DBased+Demonstration+Learning+for+Formal+Theorem+Proving%2E+In+Proceedings+of+the+International+Conference+on+Machine+Learning%2C+2024%2E)
253. Chuanyang Zheng, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, and Yu Li. [Lyra: Orchestrating Dual Correction in Automated Theorem Proving](https://md.research.elamur.ai/free/en/papers/zheng-2023-lyra-orchestrating-dual-correction-automated/). Transactions on Machine Learning Research, 2024.
254. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. [MiniF2F: A Cross-System Benchmark for Formal Olympiad-Level Mathematics](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/). In Proceedings of the International Conference on Learning Representations, 2022.
255. Jin Peng Zhou, Charles E Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don’t Trust: Verify–Grounding LLM Quantitative Reasoning with Autoformalization. In Proceedings of the International Conference on Learning Representations, 2024a. — [Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization](https://md.research.elamur.ai/free/en/papers/zhou-2024-don-t-trust-verify-grounding/)
256. Jin Peng Zhou, Yuhuai Wu, Qiyang Li, and Roger Grosse. REFACTOR: Learning to Extract Theorems from Proofs. In Proceedings of the International Conference on Learning Representations, 2024b. [find](https://scholar.google.com/scholar?q=Jin+Peng+Zhou%2C+Yuhuai+Wu%2C+Qiyang+Li%2C+and+Roger+Grosse%2E+REFACTOR%3A+Learning+to+Extract+Theorems+from+Proofs%2E+In+Proceedings+of+the+International+Conference+on+Learning+Representations%2C+2024b%2E)
257. Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, and Josef Urban. [Towards Finding Longer Proofs](https://md.research.elamur.ai/free/en/papers/zombori-2019-finding-longer-proofs/). In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 2021a.
258. Zsolt Zombori, Josef Urban, and Miroslav Olšák. The Role of Entropy in Guiding a Connection Prover. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 2021b. [find](https://scholar.google.com/scholar?q=Zsolt+Zombori%2C+Josef+Urban%2C+and+Miroslav+Ols%CC%8Ca%CC%81k%2E+The+Role+of+Entropy+in+Guiding+a+Connection+Prover%2E+In+Proceedings+of+the+International+Conference+on+Automated+Reasoning+with+Analytic+Tableaux+and+R)

*Updated 3 November 2026*