---
title: "Who cites HOL(y)Hammer: Online ATP Service for HOL Light"
description: "9 papers of the Elamur Research library cite «HOL(y)Hammer: Online ATP Service for HOL Light», found in their bibliographies; the most cited first."
canonical: "https://research.elamur.ai/free/en/papers/kaliszyk-2013-hol-y-hammer-online-atp/cited-by/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/kaliszyk-2013-hol-y-hammer-online-atp/cited-by/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [HOL(y)Hammer: Online ATP Service for HOL Light](https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-hol-y-hammer-online-atp/) / cited by

# Who cites «HOL(y)Hammer: Online ATP Service for HOL Light»

9 papers of our library cite it (of the 149,439 whose bibliographies we read) · 7 with a page here, the most cited first · [← back to «HOL(y)Hammer: Online ATP Service for HOL Light»](https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-hol-y-hammer-online-atp/)

1. **[MizAR 40 for Mizar 40](https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/) [Journal of Automated Reasoning](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/)**Cezary Kaliszyk, Josef Urban*2013 · 112 citations*
2. [**History of Interactive Theorem Proving Handbook of the History of Logic, vol. 9 (Elsevier)**John Harrison, Josef Urban, Freek Wiedijk*2014 · 109 citations*](https://md.research.elamur.ai/free/en/papers/harrison-2014-history-interactive-theorem-proving/)
3. [**Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers arXiv:2205.10893**Albert Q. Jiang, Wenda Li, Szymon Tworkowski, et al.*2022 · 79 citations*](https://md.research.elamur.ai/free/en/papers/jiang-2022-thor-wielding-hammers-integrate-language/)
4. **[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*
5. [**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/)
6. **[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*
7. [**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/)

2 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-hol-y-hammer-online-atp/) — HOL(y)Hammer: Online ATP Service for HOL Light