---
title: "Learning to Prove Theorems by Learning to Generate Theorems"
description: "They introduce MetaGen, a learnable generator for the Metamath language. 43 references, cited by 36 papers here."
authors: ["Mingzhe Wang", "Jia Deng"]
year: 2020
venue: "arXiv:2002.07019"
source: "https://arxiv.org/abs/2002.07019"
doi: "10.48550/arxiv.2002.07019"
arxiv: "2002.07019"
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/wang-2020-learning-prove-theorems-learning-generate/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/wang-2020-learning-prove-theorems-learning-generate/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2020](https://md.research.elamur.ai/free/en/papers/2020/page/6/) / Learning to Prove Theorems by Learning to Generate Theorems

# Learning to Prove Theorems by Learning to Generate Theorems

**Authors:** [Mingzhe Wang](https://md.research.elamur.ai/free/en/authors/mingzhe-wang/) and [Jia Deng](https://md.research.elamur.ai/free/en/authors/jia-hao-deng/) · **Year:** 2020 · **Venue:** arXiv:2002.07019 · **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/2002.07019) · [PDF](https://arxiv.org/pdf/2002.07019v2) · [DOI 10.48550/arxiv.2002.07019](https://doi.org/10.48550/arxiv.2002.07019) · [arXiv 2002.07019](https://arxiv.org/abs/2002.07019) · [OpenAlex](https://openalex.org/W3103412473)

**Citations:** 17 citations (OpenAlex, 2026-10-14) · [36](https://md.research.elamur.ai/free/en/papers/wang-2020-learning-prove-theorems-learning-generate/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Neural theorem provers usually learn by imitating human-written formal proofs. Such data is scarce because formalizing mathematics requires rare expertise and a lot of time. Wang and Deng address this bottleneck by adding machine-made training examples. They introduce MetaGen, a learnable generator for the Metamath language. It builds new theorems by applying substitution steps to existing ones, so every output comes with a guaranteed-correct proof. To make the synthetic data resemble human mathematics, the generator is trained in one of two ways. When human proofs are available, it learns to replay their steps in the forward direction. When only theorem statements exist, it uses reinforcement learning, with a GAN-style discriminator rating how human-like each generated theorem looks. The synthetic proofs then train Holophrasm, a neural Metamath prover. On the iset.mm and set.mm knowledge bases, provers using the extra data consistently prove more test theorems than provers trained on human proofs alone. This suggests that generated data can partly replace costly manual formalization.

## Key points
- Up to 1M unique synthetic theorems were generated for iset.mm. For set.mm, the authors generated 300K (no human proofs), 1M (10% of human proofs) and 10M (full human proof set) theorems.
- With 10% of human proofs on set.mm, adding synthetic data proves 472 theorems. Doubling the human proofs instead proves 476.
- The authors' GPU re-implementation of Holophrasm proves 557 theorems with all human proofs. Removing "trivial" proof steps from the relevance-network training data raises the count from 574 to 600.
- Learned generators beat both the random baseline MetaGen-Rand and a tf-idf/language-model ablation. They improve the relevance metrics (top-k, MRR) and the substitution-network metrics.
- The best prover solves 22.06% of set.mm test theorems, versus 29.22% reported by Polu & Sutskever (2020). The authors note the setups differ: 27,218 proofs versus about 38k, and a 5-minute time limit per run.

*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

- [Princeton University](https://md.research.elamur.ai/free/en/universities/princeton-university/) — University, Princeton, United States · 137 works · 53,849 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: Mingzhe Wang and Jia Deng. 2020. Learning to Prove Theorems by Learning to Generate Theorems. arXiv:2002.07019.

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

```bibtex
@misc{wang2020learning,
  title = {{Learning to Prove Theorems by Learning to Generate Theorems}},
  author = {Mingzhe Wang and Jia Deng},
  year = {2020},
  doi = {10.48550/arxiv.2002.07019},
  eprint = {2002.07019},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2002.07019}
}
```

- [← previous From English To Foreign Languages: Transferring Pre-trained Language Models](https://md.research.elamur.ai/free/en/papers/tran-2020-english-foreign-languages-transferring-pre/)
- [next → Overview of the IWPT 2020 Shared Task on Parsing into Enhanced Universal Dependencies](https://md.research.elamur.ai/free/en/papers/bouma-2020-overview-iwpt-2020-shared-task/)
- [↑ back to papers of 2020](https://md.research.elamur.ai/free/en/papers/2020/page/6/)

## References

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

1. Balunovic, M., Bielik, P., and Vechev, M. Learning to solve smt formulas. In Advances in Neural Information Processing Systems, pp. 10317–10328, 2018. [find](https://scholar.google.com/scholar?q=Balunovic%2C+M%2E%2C+Bielik%2C+P%2E%2C+and+Vechev%2C+M%2E+Learning+to+solve+smt+formulas%2E+In+Advances+in+Neural+Information+Processing+Systems%2C+pp%2E+10317%E2%80%9310328%2C+2018%2E)
2. Bansal, K., Loos, S., Rabe, M., Szegedy, C., and Wilcox, S. Holist: An environment for machine learning of higher order logic theorem proving. In International Conference on Machine Learning, pp. 454–463, 2019a. — [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/)
3. Bansal, K., Loos, S. M., Rabe, M. N., and Szegedy, C. [Learning to reason in large theories without imitation](https://md.research.elamur.ai/free/en/papers/bansal-2019-learning-reason-large-theories-without/). arXiv preprint arXiv:1905.10501, 2019b.
4. Bertot, Y. and Castéran, P. Coq’art: the calculus of inductive constructions, 2004. [find](https://scholar.google.com/scholar?q=Bertot%2C+Y%2E+and+Cast%C3%A9ran%2C+P%2E+Coq%E2%80%99art%3A+the+calculus+of+inductive+constructions%2C+2004%2E)
5. Chvalovskỳ, K., Gauthier, T., and Urban, J. First experiments with data driven conjecturing. 4th Conference on Artificial Intelligence and Theorem Proving, 2019. [find](https://scholar.google.com/scholar?q=Chvalovsky%CC%80%2C+K%2E%2C+Gauthier%2C+T%2E%2C+and+Urban%2C+J%2E+First+experiments+with+data+driven+conjecturing%2E+4th+Conference+on+Artificial+Intelligence+and+Theorem+Proving%2C+2019%2E)
6. Colton, S. Automated theory formation in pure mathematics. Springer Science & Business Media, 2012. [find](https://scholar.google.com/scholar?q=Colton%2C+S%2E+Automated+theory+formation+in+pure+mathematics%2E+Springer+Science+%26+Business+Media%2C+2012%2E)
7. Darvas, Á., Hähnle, R., and Sands, D. A theorem proving approach to analysis of secure information flow. In International Conference on Security in Pervasive Computing, pp. 193–209. Springer, 2005. [find](https://scholar.google.com/scholar?q=Darvas%2C+%C3%81%2E%2C+H%C3%A4hnle%2C+R%2E%2C+and+Sands%2C+D%2E+A+theorem+proving+approach+to+analysis+of+secure+information+flow%2E+In+International+Conference+on+Security+in+Pervasive+Computing%2C+pp%2E+193%E2%80%93209%2E+Springer%2C+2005%2E)
8. Durugkar, I. and Stone, P. Adversarial goal generation for intrinsic motivation. In Thirty-Second AAAI Conference on Artificial Intelligence, 2018. [find](https://scholar.google.com/scholar?q=Durugkar%2C+I%2E+and+Stone%2C+P%2E+Adversarial+goal+generation+for+intrinsic+motivation%2E+In+Thirty%2DSecond+AAAI+Conference+on+Artificial+Intelligence%2C+2018%2E)
9. Fawzi, A., Malinowski, M., Fawzi, H., and Fawzi, O. Learning dynamic polynomial proofs. In Advances in Neural Information Processing Systems, pp. 4181–4190, 2019. [find](https://scholar.google.com/scholar?q=Fawzi%2C+A%2E%2C+Malinowski%2C+M%2E%2C+Fawzi%2C+H%2E%2C+and+Fawzi%2C+O%2E+Learning+dynamic+polynomial+proofs%2E+In+Advances+in+Neural+Information+Processing+Systems%2C+pp%2E+4181%E2%80%934190%2C+2019%2E)
10. Florensa, C., Held, D., Geng, X., and Abbeel, P. [Automatic goal generation for reinforcement learning agents](https://md.research.elamur.ai/free/en/papers/florensa-2017-automatic-goal-generation-reinforcement-learning/). In Dy, J. and Krause, A. (eds.), Proceedings of the 35th International Conference on Machine Learning, volume 80 of Proceedings of Machine Learning Research, pp. 1515–1528, Stockholmsmässan,…
11. Gauthier, T., Kaliszyk, C., and Urban, J. Tactictoe: Learning to reason with hol4 tactics. arXiv preprint arXiv:1804.00595, 2018. [find](https://scholar.google.com/scholar?q=Gauthier%2C+T%2E%2C+Kaliszyk%2C+C%2E%2C+and+Urban%2C+J%2E+Tactictoe%3A+Learning+to+reason+with+hol4+tactics%2E+arXiv+preprint+arXiv%3A1804%2E00595%2C+2018%2E)
12. Goodfellow, I., Pouget-Abadie, J., Mirza, M., Xu, B., Warde-Farley, D., Ozair, S., Courville, A., and Bengio, Y. [Generative adversarial nets](https://md.research.elamur.ai/free/en/papers/goodfellow-2014-generative-adversarial-nets/). In Advances in neural information processing systems, pp. 2672–2680, 2014.
13. Gu, R., Shao, Z., Chen, H., Wu, X. N., Kim, J., Sjöberg, V., and Costanzo, D. Certikos: An extensible architecture for building certified concurrent {OS} kernels. In 12th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 16), pp. 653–669, 2016. [find](https://scholar.google.com/scholar?q=Gu%2C+R%2E%2C+Shao%2C+Z%2E%2C+Chen%2C+H%2E%2C+Wu%2C+X%2E+N%2E%2C+Kim%2C+J%2E%2C+Sj%C3%B6berg%2C+V%2E%2C+and+Costanzo%2C+D%2E+Certikos%3A+An+extensible+architecture+for+building+certified+concurrent+%7BOS%7D+kernels%2E+In+12th+%7BUSENIX%7D+Symposium+on+Operati)
14. Harrison, J. HOL Light: An overview. In Berghofer, S., Nipkow, T., Urban, C., and Wenzel, M. (eds.), Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009, volume 5674 of Lecture Notes in Computer Science, pp. 60–66, Munich, Germany, 2009. Springer-V… [find](https://scholar.google.com/scholar?q=Harrison%2C+J%2E+HOL+Light%3A+An+overview%2E+In+Berghofer%2C+S%2E%2C+Nipkow%2C+T%2E%2C+Urban%2C+C%2E%2C+and+Wenzel%2C+M%2E+%28eds%2E%29%2C+Proceedings+of+the+22nd+International+Conference+on+Theorem+Proving+in+Higher+Order+Logics%2C+TPHOLs+)
15. Huang, D. On learning to prove. arXiv preprint arXiv:1904.11099, 2019. — [arXiv:1904.11099](https://arxiv.org/abs/1904.11099) [find](https://scholar.google.com/scholar?q=Huang%2C+D%2E+On+learning+to+prove%2E+arXiv+preprint+arXiv%3A1904%2E11099%2C+2019%2E+%E2%80%94+%5BarXiv%3A1904%2E11099%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1904%2E11099%29)
16. Irving, G., Szegedy, C., Alemi, A. A., Eén, N., Chollet, F., and Urban, J. Deepmath-deep sequence models for premise selection. In Advances in Neural Information Processing Systems, pp. 2235[– 2243, 2016](https://md.research.elamur.ai/free/en/papers/alemi-2016-deepmath-deep-sequence-models-premise/).
17. Jakubův, J. and Urban, J. arXiv:1904.01677, 2019. — [arXiv:1904.01677](https://arxiv.org/abs/1904.01677) [find](https://scholar.google.com/scholar?q=Jakubu%CC%8Av%2C+J%2E+and+Urban%2C+J%2E+arXiv%3A1904%2E01677%2C+2019%2E+%E2%80%94+%5BarXiv%3A1904%2E01677%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1904%2E01677%29)
18. Hammering mizar by learning clause guidance. Kaliszyk, C. and Urban, J. Learning-assisted theorem proving with millions of lemmas. Journal of symbolic computation, 69:109–128, 2015. [find](https://scholar.google.com/scholar?q=Hammering+mizar+by+learning+clause+guidance%2E+Kaliszyk%2C+C%2E+and+Urban%2C+J%2E+Learning%2Dassisted+theorem+proving+with+millions+of+lemmas%2E+Journal+of+symbolic+computation%2C+69%3A109%E2%80%93128%2C+2015%2E)
19. Kaliszyk, C., Urban, J., and Vyskočil, J. Machine learner for automated reasoning 0.4 and 0.5. arXiv preprint arXiv:1402.2359, 2014. — [arXiv:1402.2359](https://arxiv.org/abs/1402.2359) [find](https://scholar.google.com/scholar?q=Kaliszyk%2C+C%2E%2C+Urban%2C+J%2E%2C+and+Vyskoc%CC%8Cil%2C+J%2E+Machine+learner+for+automated+reasoning+0%2E4+and+0%2E5%2E+arXiv+preprint+arXiv%3A1402%2E2359%2C+2014%2E+%E2%80%94+%5BarXiv%3A1402%2E2359%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1402%2E2359%29)
20. Kaliszyk, C., Urban, J., and Vyskočil, J. Lemmatization for stronger reasoning in large theories. In International Symposium on Frontiers of Combining Systems, pp. 341–356. Springer, 2015. [find](https://scholar.google.com/scholar?q=Kaliszyk%2C+C%2E%2C+Urban%2C+J%2E%2C+and+Vyskoc%CC%8Cil%2C+J%2E+Lemmatization+for+stronger+reasoning+in+large+theories%2E+In+International+Symposium+on+Frontiers+of+Combining+Systems%2C+pp%2E+341%E2%80%93356%2E+Springer%2C+2015%2E)
21. Kaliszyk, C., Urban, J., Michalewski, H., and Olšák, M. [Reinforcement learning of theorem proving](https://md.research.elamur.ai/free/en/papers/kaliszyk-2018-reinforcement-learning-theorem-proving/). In Advances in Neural Information Processing Systems, pp. 8822–8833, 2018.
22. Kern, C. and Greenstreet, M. R. Formal verification in hardware design: a survey. ACM Transactions on Design Automation of Electronic Systems (TODAES), 4(2):123–193, 1999. [find](https://scholar.google.com/scholar?q=Kern%2C+C%2E+and+Greenstreet%2C+M%2E+R%2E+Formal+verification+in+hardware+design%3A+a+survey%2E+ACM+Transactions+on+Design+Automation+of+Electronic+Systems+%28TODAES%29%2C+4%282%29%3A123%E2%80%93193%2C+1999%2E)
23. Kingma, D. P. and Ba, J. arXiv:1412.[6980, 2014](https://md.research.elamur.ai/free/en/papers/kingma-2014-adam-method-stochastic-optimization/).
24. Adam: A method for stochastic optimization. Kocsis, L. and Szepesvári, C. Bandit based monte-carlo planning. In European conference on machine learning, pp. 282–293. Springer, 2006. [find](https://scholar.google.com/scholar?q=Adam%3A+A+method+for+stochastic+optimization%2E+Kocsis%2C+L%2E+and+Szepesv%C3%A1ri%2C+C%2E+Bandit+based+monte%2Dcarlo+planning%2E+In+European+conference+on+machine+learning%2C+pp%2E+282%E2%80%93293%2E+Springer%2C+2006%2E)
25. Lee, D., Szegedy, C., Rabe, M. N., Loos, S. M., and Bansal, K. [Mathematical reasoning in latent space](https://md.research.elamur.ai/free/en/papers/lee-2019-mathematical-reasoning-latent-space/). arXiv preprint arXiv:1909.11851, 2019.
26. Loos, S., Irving, G., Szegedy, C., and Kaliszyk, C. [Deep network guided proof search](https://md.research.elamur.ai/free/en/papers/loos-2017-deep-network-guided-proof-search/). arXiv preprint arXiv:1701.06972, 2017.
27. Megill, N. and Wheeler, D. [Metamath: A Computer Language for Mathematical Proofs](https://md.research.elamur.ai/free/en/papers/megill-2019-metamath-computer-language-mathematical-proofs/). Lulu Press, Morrisville, North Carolina, 2019. [http://us.metamath.org/downloads/metamath.pdf](http://us.metamath.org/downloads/metamath.pdf). [↗](http://us.metamath.org/downloads/metamath.pdf)
28. Paliwal, A., Loos, S., Rabe, M., Bansal, K., and Szegedy, C. [Graph representations for higher-order logic and theorem proving](https://md.research.elamur.ai/free/en/papers/paliwal-2019-graph-representations-higher-order-logic/). arXiv preprint arXiv:1905.10006, 2019.
29. Piotrowski, B. and Urban, J. Atpboost: Learning premise selection in binary setting with atp feedback. In International Joint Conference on Automated Reasoning, pp. 566–574. Springer, 2018. [find](https://scholar.google.com/scholar?q=Piotrowski%2C+B%2E+and+Urban%2C+J%2E+Atpboost%3A+Learning+premise+selection+in+binary+setting+with+atp+feedback%2E+In+International+Joint+Conference+on+Automated+Reasoning%2C+pp%2E+566%E2%80%93574%2E+Springer%2C+2018%2E)
30. Polu, S. and Sutskever, I. [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.
31. Schulz, S. E–a brainiac theorem prover. Ai Communications, 15(2, 3):111–126, 2002. [find](https://scholar.google.com/scholar?q=Schulz%2C+S%2E+E%E2%80%93a+brainiac+theorem+prover%2E+Ai+Communications%2C+15%282%2C+3%29%3A111%E2%80%93126%2C+2002%2E)
32. Slind, K. and Norrish, M. A brief overview of hol4. In International Conference on Theorem Proving in Higher Order Logics, pp. 28–32. Springer, 2008. [find](https://scholar.google.com/scholar?q=Slind%2C+K%2E+and+Norrish%2C+M%2E+A+brief+overview+of+hol4%2E+In+International+Conference+on+Theorem+Proving+in+Higher+Order+Logics%2C+pp%2E+28%E2%80%9332%2E+Springer%2C+2008%2E)
33. Sukhbaatar, S., Lin, Z., Kostrikov, I., Synnaeve, G., Szlam, A., and Fergus, R. Intrinsic motivation and automatic curricula via asymmetric self-play. arXiv preprint arXiv:1703.05407, 2017. [find](https://scholar.google.com/scholar?q=Sukhbaatar%2C+S%2E%2C+Lin%2C+Z%2E%2C+Kostrikov%2C+I%2E%2C+Synnaeve%2C+G%2E%2C+Szlam%2C+A%2E%2C+and+Fergus%2C+R%2E+Intrinsic+motivation+and+automatic+curricula+via+asymmetric+self%2Dplay%2E+arXiv+preprint+arXiv%3A1703%2E05407%2C+2017%2E)
34. Sukhbaatar, S., Denton, E., Szlam, A., and Fergus, R. Learning goal embeddings via self-play for hierarchical reinforcement learning. arXiv preprint arXiv:1811.09083, 2018. — [arXiv:1811.09083](https://arxiv.org/abs/1811.09083) [find](https://scholar.google.com/scholar?q=Sukhbaatar%2C+S%2E%2C+Denton%2C+E%2E%2C+Szlam%2C+A%2E%2C+and+Fergus%2C+R%2E+Learning+goal+embeddings+via+self%2Dplay+for+hierarchical+reinforcement+learning%2E+arXiv+preprint+arXiv%3A1811%2E09083%2C+2018%2E+%E2%80%94+%5BarXiv%3A1811%2E09083%5D%28https%3A)
35. Urban, J. Mptp–motivation, implementation, first experiments. Journal of Automated Reasoning, 33 (3-4):319–339, 2004. [find](https://scholar.google.com/scholar?q=Urban%2C+J%2E+Mptp%E2%80%93motivation%2C+implementation%2C+first+experiments%2E+Journal+of+Automated+Reasoning%2C+33+%283%2D4%29%3A319%E2%80%93339%2C+2004%2E)
36. Urban, J. and Jakubův, J. [First neural conjecturing datasets and experiments](https://md.research.elamur.ai/free/en/papers/urban-2020-first-neural-conjecturing-datasets-experiments/). arXiv preprint arXiv:2005.14664, 2020.
37. Urban, J., Sutcliffe, G., Pudlák, P., and Vyskočil, J. Malarea sg1-machine learner for automated reasoning with semantic guidance. In International Joint Conference on Automated Reasoning, pp. 441–456. Springer, 2008. [arXiv preprint arXiv preprint Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J.…](https://md.research.elamur.ai/free/en/papers/vaswani-2017-attention-all-need/)
38. Whalen, D. [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.
39. Wiedijk, F. Formal proof sketches. In International Workshop on Types for Proofs and Programs, pp. 378–393. Springer, 2003. [find](https://scholar.google.com/scholar?q=Wiedijk%2C+F%2E+Formal+proof+sketches%2E+In+International+Workshop+on+Types+for+Proofs+and+Programs%2C+pp%2E+378%E2%80%93393%2E+Springer%2C+2003%2E)
40. Wiedijk, F. Formalizing 100 theorems. [http://www.cs.ru.nl/~freek/100/](http://www.cs.ru.nl/~freek/100/), 2019. [↗](http://www.cs.ru.nl/~freek/100/)
41. Williams, R. J. Simple statistical gradient-following algorithms for connectionist reinforcement learning. Machine learning, 8(3-4):229–256, 1992. [find](https://scholar.google.com/scholar?q=Williams%2C+R%2E+J%2E+Simple+statistical+gradient%2Dfollowing+algorithms+for+connectionist+reinforcement+learning%2E+Machine+learning%2C+8%283%2D4%29%3A229%E2%80%93256%2C+1992%2E)
42. Yang, K. and Deng, J. [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 International Conference on Machine Learning, 2019.
43. Zombori, Z., Csiszárik, A., Michalewski, H., Kaliszyk, C., and Urban, J. [Towards finding longer proofs](https://md.research.elamur.ai/free/en/papers/zombori-2019-finding-longer-proofs/). arXiv preprint arXiv:1905.13100, 2019.

*Updated 3 November 2026*