---
title: "Thor — paper by Jiang et al. (2022) — summary and ideas"
description: "To build the training data, the authors run Sledgehammer on every proof state in the training proofs. 44 references, cited by 58 papers here."
authors: ["Albert Q. Jiang", "Wenda Li", "Szymon Tworkowski", "Konrad Czechowski", "Tomasz Odrzygóźdź", "Piotr Miłoś", "Yuhuai Wu", "Mateja Jamnik"]
year: 2022
venue: "arXiv:2205.10893"
source: "https://arxiv.org/abs/2205.10893"
doi: "10.48550/arxiv.2205.10893"
arxiv: "2205.10893"
licence: "CC BY 4.0 (arXiv)"
licence_url: "https://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/jiang-2022-thor-wielding-hammers-integrate-language/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/jiang-2022-thor-wielding-hammers-integrate-language/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2022](https://md.research.elamur.ai/free/en/papers/2022/page/5/) / Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers

# Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers

**Authors:** [Albert Q. Jiang](https://md.research.elamur.ai/free/en/authors/albert-q-jiang/), [Wenda Li](https://md.research.elamur.ai/free/en/authors/wenda-li/), Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, [Yuhuai Wu](https://md.research.elamur.ai/free/en/authors/yuhuai-wu/) and [Mateja Jamnik](https://md.research.elamur.ai/free/en/authors/mateja-jamnik/) · **Year:** 2022 · **Venue:** arXiv:2205.10893 · **Licence:** [CC BY 4.0 (arXiv)](https://creativecommons.org/licenses/by/4.0/)

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

**Citations:** 21 citations (OpenAlex, 2026-10-14) · [58](https://md.research.elamur.ai/free/en/papers/jiang-2022-thor-wielding-hammers-integrate-language/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Language-model provers for interactive theorem provers (ITPs) are weak at premise selection, which means finding the few useful lemmas in libraries holding hundreds of thousands of facts. A model cannot memorise that many facts, and listing candidate premises in the prompt quickly goes past its context length. Thor hands this job to hammers. A hammer sends the goal to external automated theorem provers (ATPs) and keeps only the premises their proofs actually use. To build the training data, the authors run Sledgehammer on every proof state in the training proofs. Wherever it succeeds, the target proof step is replaced with a special `<hammer>` token. The language model learns when to output this token, and during proof search the token triggers a real Sledgehammer call. The authors built Thor for Isabelle and tested it on PISA and MiniF2F. On PISA it raised the language model's success rate from 39.0% to 57.0%. On MiniF2F it reached 29.9%, slightly above an expert-iteration system, while using much less compute. The result shows that combining neural and symbolic provers is cheap and effective, and the method can be ported to any ITP that has a hammer.

## Key points
- The motivating measurement: only 1.9% of model-generated steps that cite premises moved the proof forward, compared with 28.2% of steps that cite none.
- On PISA, Thor solved 57.0% of problems, up from 39.0%, and 8.2% of problems could be solved neither by the language model alone nor by Sledgehammer alone.
- On MiniF2F (test set), Thor raised the base language model from 24.2% to 29.9%, compared with 29.6% for expert iteration (Polu et al., 2022). The authors estimate that matching that expert-iteration setup in Isabelle would take about 100 human hours of formalisation and 500 TPU hours.
- The protocol should carry over to other ITPs with hammers, such as HOL(y)Hammer for HOL Light and CoqHammer for Coq, but it was tested only on Isabelle.
- Thor can only use premise-selection tools that produce valid proof steps directly, so ranking methods like SInE or search tools like SErAPIS cannot be plugged in. Expert iteration or proof artifact co-training could be added on top of Thor.

*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

- [Google](https://md.research.elamur.ai/free/en/companies/google/) — Company, Mountain View, United States · 492 works · 440,463 citations
- [Stanford University](https://md.research.elamur.ai/free/en/universities/stanford-university/) — University, Stanford, United States · 506 works · 330,053 citations
- [University of Cambridge](https://md.research.elamur.ai/free/en/universities/university-of-cambridge/) — University, Cambridge, United Kingdom · 256 works · 123,373 citations
- [University of Warsaw](https://md.research.elamur.ai/free/en/universities/university-of-warsaw/) — University, Warsaw, Poland · 8 works · 575 citations
- [Polish Academy of Sciences](https://md.research.elamur.ai/free/en/government/polish-academy-of-sciences/) — Government body, Warsaw, Poland · 12 works · 599 citations

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

🧭 Topics (2): [🧠 Language models & pretraining](https://md.research.elamur.ai/free/en/topics/language-models/) · 3,894 works · [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,685 works

## Cite

Cite as: Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu and Mateja Jamnik. 2022. Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. arXiv:2205.10893.

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

```bibtex
@misc{jiang2022thor,
  title = {{Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers}},
  author = {Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu and Mateja Jamnik},
  year = {2022},
  doi = {10.48550/arxiv.2205.10893},
  eprint = {2205.10893},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2205.10893}
}
```

- [← previous Out-of-Distribution Detection and Selective Generation for Conditional Language Models](https://md.research.elamur.ai/free/en/papers/ren-2022-out-distribution-detection-selective-generation/)
- [next → Domain Adaptation with Pre-trained Transformers for Query-Focused Abstractive Text Summarization](https://md.research.elamur.ai/free/en/papers/laskar-2022-domain-adaptation-pre-trained-transformers/)
- [↑ back to papers of 2022](https://md.research.elamur.ai/free/en/papers/2022/page/5/)

## References

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

1. Jeremy Avigad, Kevin Donnelly, David Gray, and Paul Raff. A formally verified proof of the prime number theorem. ACM Transactions on Computational Logic (TOCL), 9(1):2–es, 2007. [find](https://scholar.google.com/scholar?q=Jeremy+Avigad%2C+Kevin+Donnelly%2C+David+Gray%2C+and+Paul+Raff%2E+A+formally+verified+proof+of+the+prime+number+theorem%2E+ACM+Transactions+on+Computational+Logic+%28TOCL%29%2C+9%281%29%3A2%E2%80%93es%2C+2007%2E)
2. 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/). J. Formaliz. Reason., 9(1):101–148, 2016. doi: 10.6092/issn.1972-5787/4593. URL https://doi.org/10.6092/issn.1972-5787/4593. [↗](https://doi.org/10.6092/issn.1972-5787/4593)
3. Stephen A Cook. The complexity of theorem-proving procedures. In Proceedings of the third annual ACM symposium on Theory of computing, pages 151–158, 1971. [find](https://scholar.google.com/scholar?q=Stephen+A+Cook%2E+The+complexity+of+theorem%2Dproving+procedures%2E+In+Proceedings+of+the+third+annual+ACM+symposium+on+Theory+of+computing%2C+pages+151%E2%80%93158%2C+1971%2E)
4. Lukasz Czajka and Cezary Kaliszyk. Hammer for coq: Automation for dependent type theory. J. Autom. Reason., 61(1-4):423–453, 2018. doi: 10.1007/s10817-018-9458-4. URL https://doi.org/10.1007/s10817-018-9458-4. [↗](https://doi.org/10.1007/s10817-018-9458-4)
5. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394–397, 1962. [find](https://scholar.google.com/scholar?q=Martin+Davis%2C+George+Logemann%2C+and+Donald+Loveland%2E+A+machine+program+for+theorem%2Dproving%2E+Communications+of+the+ACM%2C+5%287%29%3A394%E2%80%93397%2C+1962%2E)
6. Leo Gao, Stella Biderman, Sid Black, Laurence Golding, Travis Hoppe, Charles Foster, Jason Phang, Horace He, Anish Thite, Noa Nabeshima, Shawn Presser, and Connor Leahy. The pile: An 800gb dataset of diverse text for language modeling, 2021. URL https://arxiv.org/abs/ 2101.00027. [↗](https://arxiv.org/abs/)
7. Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. In Xavier Leroy and Alwen Tiu, editors, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pages 49–57. [find](https://scholar.google.com/scholar?q=Thibault+Gauthier+and+Cezary+Kaliszyk%2E+Premise+selection+and+external+provers+for+HOL4%2E+In+Xavier+Leroy+and+Alwen+Tiu%2C+editors%2C+Proceedings+of+the+2015+Conference+on+Certified+Programs+and+Proofs%2C+CPP)
8. ACM, 2015. doi: 10.1145/2676724.2693173. URL https://doi.org/10.1145/2676724.2693173. — [doi:10.1145/2676724.2693173](https://doi.org/10.1145/2676724.2693173) [↗](https://doi.org/10.1145/2676724.2693173)
9. Herbert L Gelernter. Realization of a geometry theorem proving machine. In IFIP congress, pages 273–281, 1959. [find](https://scholar.google.com/scholar?q=Herbert+L+Gelernter%2E+Realization+of+a+geometry+theorem+proving+machine%2E+In+IFIP+congress%2C+pages+273%E2%80%93281%2C+1959%2E)
10. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, et al. A machine-checked proof of the odd order theorem. In International conference on interactive theorem proving, pages 163–179. Spring… [find](https://scholar.google.com/scholar?q=Georges+Gonthier%2C+Andrea+Asperti%2C+Jeremy+Avigad%2C+Yves+Bertot%2C+Cyril+Cohen%2C+Fran%C3%A7ois+Garillot%2C+St%C3%A9phane+Le+Roux%2C+Assia+Mahboubi%2C+Russell+O%E2%80%99Connor%2C+Sidi+Ould+Biha%2C+et+al%2E+A+machine%2Dchecked+proof+of+the+)
11. Georges Gonthier et al. Formal proof–the four-color theorem. Notices of the AMS, 55(11):1382–1393, 2008. [find](https://scholar.google.com/scholar?q=Georges+Gonthier+et+al%2E+Formal+proof%E2%80%93the+four%2Dcolor+theorem%2E+Notices+of+the+AMS%2C+55%2811%29%3A1382%E2%80%931393%2C+2008%2E)
12. 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/). CoRR, abs/2102.06203, 2021. URL https://arxiv.org/abs/2102.06203. [↗](https://arxiv.org/abs/2102.06203)
13. Kryštof Hoder and Andrei Voronkov. Sine qua non for large theory reasoning. In International Conference on Automated Deduction, pages 299–314. Springer, 2011. [find](https://scholar.google.com/scholar?q=Kry%C5%A1tof+Hoder+and+Andrei+Voronkov%2E+Sine+qua+non+for+large+theory+reasoning%2E+In+International+Conference+on+Automated+Deduction%2C+pages+299%E2%80%93314%2E+Springer%2C+2011%2E)
14. Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban. Deepmath-deep sequence models for premise selection. Advances in neural information processing systems, 29, 2016. — [DeepMath - Deep Sequence Models for Premise Selection](https://md.research.elamur.ai/free/en/papers/alemi-2016-deepmath-deep-sequence-models-premise/)
15. Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. 6th Conference on Artificial Intelligence and Theorem Proving, 2021. [find](https://scholar.google.com/scholar?q=Albert+Q%2E+Jiang%2C+Wenda+Li%2C+Jesse+Michael+Han%2C+and+Yuhuai+Wu%2E+Lisa%3A+Language+models+of+isabelle+proofs%2E+6th+Conference+on+Artificial+Intelligence+and+Theorem+Proving%2C+2021%2E)
16. Cezary Kaliszyk and Josef Urban. Hol(y)hammer: Online ATP service for HOL light. Math. Comput. Sci., 9(1):5–22, 2015. doi: 10.1007/s11786-014-0182-0. URL https://doi.org/10.1007/ s11786-014-0182-0. [find](https://scholar.google.com/scholar?q=Cezary+Kaliszyk+and+Josef+Urban%2E+Hol%28y%29hammer%3A+Online+ATP+service+for+HOL+light%2E+Math%2E+Comput%2E+Sci%2E%2C+9%281%29%3A5%E2%80%9322%2C+2015%2E+doi%3A+10%2E1007%2Fs11786%2D014%2D0182%2D0%2E+URL+https%3A%2F%2Fdoi%2Eorg%2F10%2E1007%2F+s11786%2D014%2D0182%2D0%2E)
17. Cezary Kaliszyk, François Chollet, and Christian Szegedy. Holstep: A machine learning dataset for higher-order logic theorem proving. arXiv preprint arXiv:1703.00426, 2017. [find](https://scholar.google.com/scholar?q=Cezary+Kaliszyk%2C+Fran%C3%A7ois+Chollet%2C+and+Christian+Szegedy%2E+Holstep%3A+A+machine+learning+dataset+for+higher%2Dorder+logic+theorem+proving%2E+arXiv+preprint+arXiv%3A1703%2E00426%2C+2017%2E)
18. 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 22nd symposium on Operating systems principles, pages 207–… [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)
19. Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes. Overview and evaluation of premise selection techniques for large theory mathematics. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Automated Reasoning - 6th International Joint Conference, IJCAR 20… [find](https://scholar.google.com/scholar?q=Daniel+K%C3%BChlwein%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+Bernhard+Gramlich%2C+Dale+)
20. Springer, 2012. doi: 10.1007/978-3-642-31365-3\\_30. URL https://doi.org/10.1007/978-3-642-31365-3_30. — [doi:10.1007/978-3-642-31365-3\\_30](https://doi.org/10.1007/978-3-642-31365-3_30) [↗](https://doi.org/10.1007/978-3-642-31365-3_30)
21. Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Isarstep: a benchmark for high-level mathematical reasoning. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. [find](https://scholar.google.com/scholar?q=Wenda+Li%2C+Lei+Yu%2C+Yuhuai+Wu%2C+and+Lawrence+C%2E+Paulson%2E+Isarstep%3A+a+benchmark+for+high%2Dlevel+mathematical+reasoning%2E+In+9th+International+Conference+on+Learning+Representations%2C+ICLR+2021%2C+Virtual+Event)
22. OpenReview.net, 2021. URL [https://openreview.net/](https://openreview.net/) forum?id=Pzj6fzU6wkj. [↗](https://openreview.net/)
23. Jia Meng and Lawrence C. Paulson. Translating higher-order clauses to first-order clauses. J. Autom. Reason., 40(1):35–60, 2008. doi: 10.1007/s10817-007-9085-y. URL https://doi.org/10. 1007/s10817-007-9085-y. — [doi:10.1007/s10817-007-9085-y](https://doi.org/10.1007/s10817-007-9085-y) [find](https://scholar.google.com/scholar?q=Jia+Meng+and+Lawrence+C%2E+Paulson%2E+Translating+higher%2Dorder+clauses+to+first%2Dorder+clauses%2E+J%2E+Autom%2E+Reason%2E%2C+40%281%29%3A35%E2%80%9360%2C+2008%2E+doi%3A+10%2E1007%2Fs10817%2D007%2D9085%2Dy%2E+URL+https%3A%2F%2Fdoi%2Eorg%2F10%2E+1007%2Fs10817%2D007)
24. Olga Ohrimenko, Peter J Stuckey, and Michael Codish. Propagation via lazy clause generation. Constraints, 14(3):357–391, 2009. [find](https://scholar.google.com/scholar?q=Olga+Ohrimenko%2C+Peter+J+Stuckey%2C+and+Michael+Codish%2E+Propagation+via+lazy+clause+generation%2E+Constraints%2C+14%283%29%3A357%E2%80%93391%2C+2009%2E)
25. Lawrence C. Paulson. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In Renate A. Schmidt, Stephan Schulz, and Boris Konev, editors, Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR-2010, Edinburgh, Sco… [find](https://scholar.google.com/scholar?q=Lawrence+C%2E+Paulson%2E+Three+years+of+experience+with+sledgehammer%2C+a+practical+link+between+automatic+and+interactive+theorem+provers%2E+In+Renate+A%2E+Schmidt%2C+Stephan+Schulz%2C+and+Boris+Konev%2C+editors%2C+Pr)
26. EasyChair, 2010. doi: 10.29007/tnfd. URL https://doi.org/10.29007/tnfd. [↗](https://doi.org/10.29007/tnfd)
27. 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/). CoRR, abs/2009.03393, 2020. URL https://arxiv.org/abs/2009.03393. [↗](https://arxiv.org/abs/2009.03393)
28. 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/). CoRR, abs/2202.01344, 2022. URL https://arxiv.org/abs/2202.01344. [↗](https://arxiv.org/abs/2202.01344)
29. Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, Ilya Sutskever, et al. Language models are unsupervised multitask learners. OpenAI blog, 1(8):9, 2019. [find](https://scholar.google.com/scholar?q=Alec+Radford%2C+Jeffrey+Wu%2C+Rewon+Child%2C+David+Luan%2C+Dario+Amodei%2C+Ilya+Sutskever%2C+et+al%2E+Language+models+are+unsupervised+multitask+learners%2E+OpenAI+blog%2C+1%288%29%3A9%2C+2019%2E)
30. Peter Scholze. Liquid tensor experiment. Experimental Mathematics, 0(0):1–6, 2021. doi: 10.1080/ 10586458.2021.1926016. URL https://doi.org/10.1080/10586458.2021.1926016. — [doi:10.1080/10586458.2021.1926016](https://doi.org/10.1080/10586458.2021.1926016) [↗](https://doi.org/10.1080/10586458.2021.1926016)
31. David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, Timothy P. Lillicrap, Karen Simonyan, and Demis Hassabis. Mastering chess and shogi by self-play with a general reinforcement learning algori… — [Mastering chess and shogi by self-play with a general reinforcement learning algorithm](https://md.research.elamur.ai/free/en/papers/al-2017-mastering-chess-shogi-self-play/)
32. Yiannos Stathopoulos, Angeliki Koutsoukou-Argyraki, and LC Paulson. Serapis: A concept-oriented search engine for the isabelle libraries based on natural language. In Online proceedings of the Isabelle Workshop, 2020. [find](https://scholar.google.com/scholar?q=Yiannos+Stathopoulos%2C+Angeliki+Koutsoukou%2DArgyraki%2C+and+LC+Paulson%2E+Serapis%3A+A+concept%2Doriented+search+engine+for+the+isabelle+libraries+based+on+natural+language%2E+In+Online+proceedings+of+the+Isabell)
33. Jianlin Su, Yu Lu, Shengfeng Pan, Bo Wen, and Yunfeng Liu. [Roformer: Enhanced transformer with rotary position embedding](https://md.research.elamur.ai/free/en/papers/su-2021-roformer-enhanced-transformer-rotary-position/), 2021. URL https://arxiv.org/abs/2104.09864. [↗](https://arxiv.org/abs/2104.09864)
34. Geoff Sutcliffe and Yury Puzis. SRASS - A semantic relevance axiom selection system. In Frank Pfenning, editor, Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, volume 4603 of Lecture Notes in Computer Science, pages… [find](https://scholar.google.com/scholar?q=Geoff+Sutcliffe+and+Yury+Puzis%2E+SRASS+%2D+A+semantic+relevance+axiom+selection+system%2E+In+Frank+Pfenning%2C+editor%2C+Automated+Deduction+%2D+CADE%2D21%2C+21st+International+Conference+on+Automated+Deduction%2C+Bre)
35. Springer, 2007. doi: 10.1007/978-3-540-73595-3\\_20. URL https://doi.org/10.1007/978-3-540-73595-3_20. — [doi:10.1007/978-3-540-73595-3\\_20](https://doi.org/10.1007/978-3-540-73595-3_20) [↗](https://doi.org/10.1007/978-3-540-73595-3_20)
36. Geoff Sutcliffe, Josef Urban, and Stephan Schulz, editors. Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007, volume 257 of CEUR Workshop Proceedings, 2007. CEUR-WS.org. URL [http://ceur-ws.org/Vol-257](http://ceur-ws.org/Vol-257). [↗](http://ceur-ws.org/Vol-257)
37. Alfred Tarski. Truth and proof. Scientific American, 220(6):63–77, 1969. [find](https://scholar.google.com/scholar?q=Alfred+Tarski%2E+Truth+and+proof%2E+Scientific+American%2C+220%286%29%3A63%E2%80%9377%2C+1969%2E)
38. Josef Urban. Malarea: a metasystem for automated reasoning in large theories. In ESARLT, 2007. [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+Malarea%3A+a+metasystem+for+automated+reasoning+in+large+theories%2E+In+ESARLT%2C+2007%2E)
39. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jirí Vyskocil. Malarea SG1- machine learner for automated reasoning with semantic guidance. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, Augu… [find](https://scholar.google.com/scholar?q=Josef+Urban%2C+Geoff+Sutcliffe%2C+Petr+Pudl%C3%A1k%2C+and+Jir%C3%AD+Vyskocil%2E+Malarea+SG1%2D+machine+learner+for+automated+reasoning+with+semantic+guidance%2E+In+Alessandro+Armando%2C+Peter+Baumgartner%2C+and+Gilles+Dowek%2C+e)
40. Springer, 2008. doi: 10.1007/978-3-540-71070-7\\_37. URL https://doi.org/10.1007/978-3-540-71070-7_37. — [doi:10.1007/978-3-540-71070-7\\_37](https://doi.org/10.1007/978-3-540-71070-7_37) [↗](https://doi.org/10.1007/978-3-540-71070-7_37)
41. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. [Attention is all you need](https://md.research.elamur.ai/free/en/papers/vaswani-2017-attention-all-need/), 2017. URL https://arxiv.org/abs/ 1706.03762. [↗](https://arxiv.org/abs/)
42. Ben Wang and Aran Komatsuzaki. GPT-J-6B: A 6 Billion Parameter Autoregressive Language Model. [https://github.com/kingoflolz/mesh-transformer-jax](https://github.com/kingoflolz/mesh-transformer-jax), May 2021. [↗](https://github.com/kingoflolz/mesh-transformer-jax)
43. Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. Advances in neural information processing systems, 30, 2017. [find](https://scholar.google.com/scholar?q=Mingzhe+Wang%2C+Yihe+Tang%2C+Jian+Wang%2C+and+Jia+Deng%2E+Premise+selection+for+theorem+proving+by+deep+graph+embedding%2E+Advances+in+neural+information+processing+systems%2C+30%2C+2017%2E)
44. 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 International Conference on Learning Representations, 2022. URL [https://openreview.net/forum?id=9ZPegFuFTFv](https://openreview.net/forum?id=9ZPegFuFTFv). [↗](https://openreview.net/forum?id=9ZPegFuFTFv)

*Updated 2 November 2026*