---
title: "Who cites MizAR 40 for Mizar 40 — 20 papers of our library"
description: "20 papers of the Elamur Research library cite «MizAR 40 for Mizar 40», found in their bibliographies; the most cited first."
canonical: "https://research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/cited-by/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/cited-by/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [MizAR 40 for Mizar 40](https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/) / cited by

# Who cites «MizAR 40 for Mizar 40»

20 papers of our library cite it (of the 149,439 whose bibliographies we read) · 15 with a page here, the most cited first · [← back to «MizAR 40 for Mizar 40»](https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/)

1. **[Deep Network Guided Proof Search](https://md.research.elamur.ai/free/en/papers/loos-2017-deep-network-guided-proof-search/) [EPiC series in computing](https://md.research.elamur.ai/free/en/venues/epic-series-in-computing/)**Sarah Loos, Geoffrey Irving, Christian Szegedy, et al.*2017 · 139 citations*
2. [**Proof Artifact Co-training for Theorem Proving with Language Models arXiv:2102.06203**Jesse Michael Han, Jason Rute, Yuhuai Wu, et al.*2021 · 82 citations*](https://md.research.elamur.ai/free/en/papers/han-2021-proof-artifact-co-training-theorem/)
3. **[ENIGMA: Efficient Learning-based Inference Guiding Machine](https://md.research.elamur.ai/free/en/papers/jakubuv-2017-enigma-efficient-learning-based-inference/) [Lecture notes in computer science](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/)**Jan Jakubův, Josef Urban*2017 · 67 citations*
4. **[TacticToe: Learning to Prove with Tactics](https://md.research.elamur.ai/free/en/papers/gauthier-2018-tactictoe-learning-prove-tactics/) [Journal of Automated Reasoning](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/)**Thibault Gauthier, Cezary Kaliszyk, Josef Urban, et al.*2018 · 57 citations*
5. [**Reinforcement Learning of Theorem Proving arXiv:1805.07563**Cezary Kaliszyk, Josef Urban, Henryk Michalewski, et al.*2018 · 50 citations*](https://md.research.elamur.ai/free/en/papers/kaliszyk-2018-reinforcement-learning-theorem-proving/)
6. [**Holophrasm: a neural Automated Theorem Prover for higher-order logic arXiv:1608.02644**Daniel Whalen*2016 · 48 citations*](https://md.research.elamur.ai/free/en/papers/whalen-2016-holophrasm-neural-automated-theorem-prover/)
7. [**A Survey on Deep Learning for Theorem Proving arXiv:2404.09939**Zhaoyu Li, Jialiang Sun, Logan Murphy, et al.*2024 · 46 citations*](https://md.research.elamur.ai/free/en/papers/li-2024-survey-deep-learning-theorem-proving/)
8. **[ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://md.research.elamur.ai/free/en/papers/jakubuv-2020-enigma-anonymous-symbol-independent-inference/) [Lecture notes in computer science](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/)**Jan Jakubův, Karel Chvalovský, Miroslav Olšák, et al.*2020 · 42 citations*
9. [**Magnushammer: A Transformer-Based Approach to Premise Selection arXiv:2303.04488**Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, et al.*2023 · 35 citations*](https://md.research.elamur.ai/free/en/papers/mikula-2023-magnushammer-transformer-based-approach-premise/)
10. **[Property Invariant Embedding for Automated Reasoning](https://md.research.elamur.ai/free/en/papers/olsak-2019-property-invariant-embedding-automated-reasoning/) [Frontiers in artificial intelligence and applications](https://md.research.elamur.ai/free/en/venues/frontiers-in-artificial-intelligence-and-applications/)**Miroslav Olšák, Cezary Kaliszyk, Josef Urban*2019 · 30 citations*
11. [**TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning arXiv:2102.09756**Minchao Wu, Michael Norrish, Christian Walder, et al.*2021 · 24 citations*](https://md.research.elamur.ai/free/en/papers/wu-2021-tacticzero-learning-prove-theorems-scratch/)
12. **[Stateful Premise Selection by Recurrent Neural Networks](https://md.research.elamur.ai/free/en/papers/piotrowski-2020-stateful-premise-selection-recurrent-neural/) [EPiC series in computing](https://md.research.elamur.ai/free/en/venues/epic-series-in-computing/)**Bartosz Piotrowski, Josef Urban*2020 · 21 citations*
13. [**Graph2Tac: Online Representation Learning of Formal Math Concepts arXiv:2401.02949**Lasse Blaauwbroek, Miroslav Olšák, Jason Rute, et al.*2024 · 19 citations*](https://md.research.elamur.ai/free/en/papers/blaauwbroek-2024-graph2tac-online-representation-learning-formal/)
14. [**Learning to Prove from Synthetic Theorems arXiv:2006.11259**Eser Aygün, Zafarali Ahmed, Ankit Anand, et al.*2020 · 12 citations*](https://md.research.elamur.ai/free/en/papers/aygun-2020-learning-prove-synthetic-theorems/)
15. [**Premise Selection for a Lean Hammer arXiv:2506.07477**Thomas Zhu, Joshua Clune, Jeremy Avigad, et al.*2025 · 5 citations*](https://md.research.elamur.ai/free/en/papers/zhu-2025-premise-selection-lean-hammer/)

5 more papers of our library cite it; they have no page here yet.

- [← back to](https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/) — MizAR 40 for Mizar 40