---
title: "Hammering towards QED — paper by Blanchette et al. (2016)"
description: "This survey covers \"hammers,\" tools that let users of proof assistants prove hard lemmas automatically. 3 references, cited by 32 papers here."
authors: ["Jasmin Christian Blanchette", "Cezary Kaliszyk", "Lawrence C. Paulson", "Josef Urban"]
year: 2016
venue: "Journal of Formalized Reasoning 9(1)"
source: "https://jfr.unibo.it/article/view/4593"
licence: "CC BY 3.0 (JFR)"
licence_url: "https://creativecommons.org/licenses/by/3.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/blanchette-2016-hammering-qed/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/blanchette-2016-hammering-qed/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2016](https://md.research.elamur.ai/free/en/papers/2016/page/3/) / Hammering towards QED

# Hammering towards QED

**Authors:** Jasmin Christian Blanchette, [Cezary Kaliszyk](https://md.research.elamur.ai/free/en/authors/cezary-kaliszyk/), Lawrence C. Paulson and [Josef Urban](https://md.research.elamur.ai/free/en/authors/josef-urban/) · **Year:** 2016 · **Venue:** Journal of Formalized Reasoning 9(1) · **Licence:** [CC BY 3.0 (JFR)](https://creativecommons.org/licenses/by/3.0/)

**Links:** [Publisher's page](https://doi.org/10.6092/issn.1972-5787/4593) · [PDF](https://jfr.unibo.it/article/download/4593/5730/17573) · [OpenAlex](https://openalex.org/W2262606152)

**Citations:** 95 citations (OpenAlex, 2026-10-14) · [32](https://md.research.elamur.ai/free/en/papers/blanchette-2016-hammering-qed/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
This survey covers "hammers," tools that let users of proof assistants prove hard lemmas automatically. The user does not have to script the proof search by hand. The tools draw on very large formal libraries, and the name comes from Sledgehammer for Isabelle and HOLyHammer for HOL Light.

The authors break a typical hammer into three stages:
- **Premise selection** picks the library facts likely to help with the current goal, using syntactic, semantic or learned heuristics.
- **Translation** recasts the proof assistant's rich logic into the simpler, usually first-order logic of automatic theorem provers (ATPs).
- **Proof reconstruction** replays the external proof so the proof assistant can certify it.

The paper also traces the history of ATP/ITP integration and reviews published benchmark results. It links the technology to the 1993 QED Manifesto. The authors argue that strong automated reasoning and AI are likely essential for QED-style projects, and that formal libraries are valuable material for building such AI. Good translations into an efficiently automated logic matter in practice whichever foundational framework is chosen.

## Key points
- Hammers prove roughly 40% of top-level lemmas in the Mizar and Flyspeck libraries and about 70% of goals in the Isabelle Judgment Day benchmark. Some of these libraries hold more than 100,000 top-level facts.
- Hales credits automated procedures with 40% of Mizar theorems and 47% of HOL Light/Flyspeck, with similar rates in Isabelle.
- The pipeline has three modules: premise selector, translation module and proof reconstruction module. Not every system includes all three.
- Related systems include MaLARea, the Mizar Proof Advisor and Why3. Further ATP/SMT links exist for HOL Light, HOL4, Coq, ACL2 and PVS.
- Since 2008 the Large Theory Batch category of CASC has benchmarked ATPs on large problems taken from Mizar, Isabelle, HOL Light, SUMO and Cyc.

*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 Cambridge](https://md.research.elamur.ai/free/en/universities/university-of-cambridge/) — University, Cambridge, United Kingdom · 256 works · 123,373 citations
- [Universität Innsbruck](https://md.research.elamur.ai/free/en/universities/universitat-innsbruck/) — University, Innsbruck, Austria · 10 works · 876 citations
- [Cambridge University Press](https://md.research.elamur.ai/free/en/companies/cambridge-university-press/) — Company, Cambridge, United Kingdom · 5 works · 355 citations
- [Czech Technical University in Prague](https://md.research.elamur.ai/free/en/universities/czech-technical-university-in-prague/) — University, Prague, Czechia · 3 works · 402 citations

Also on the byline: [VERIDIS: Modeling and Verification of Distributed Algorithms and Systems](https://ror.org/0440j7g03).

📚 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 (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,685 works

💡 Concepts (1): [💡 Lemma](https://md.research.elamur.ai/free/en/concepts/lemma/) · 24 works

## Cite

Cite as: Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson and Josef Urban. 2016. Hammering towards QED. Journal of Formalized Reasoning 9(1).

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

```bibtex
@article{blanchette2016hammering,
  title = {{Hammering towards QED}},
  author = {Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson and Josef Urban},
  journal = {Journal of Formalized Reasoning 9(1)},
  year = {2016},
  doi = {10.6092/issn.1972-5787/4593},
  url = {https://doi.org/10.6092/issn.1972-5787/4593}
}
```

- [← previous Recognizing Implicit Discourse Relations via Repeated Reading: Neural Networks with Multi-Level Attention](https://md.research.elamur.ai/free/en/papers/liu-2016-recognizing-implicit-discourse-relations-repeated/)
- [next → A Latent Variable Recurrent Neural Network for Discourse-Driven Language Models](https://md.research.elamur.ai/free/en/papers/ji-2016-latent-variable-recurrent-neural-network/)
- [↑ back to papers of 2016](https://md.research.elamur.ai/free/en/papers/2016/page/3/)

## References

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

1. The QED Manifesto. In Bundy [36], pages 238251. [find](https://scholar.google.com/scholar?q=The+QED+Manifesto%2E+In+Bundy+%5B36%5D%2C+pages+238%15251%2E)
2. Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Wolfram Menzel, Wolfgang Reif, Gerhard Schellhorn, and Peter H. Schmitt. Integrating automated Automated DeductionA Basis for Applications and interactive theorem proving. In Wolfgang Bibel and Peter H. Schmitt, editors, , volume II: Systems and Im… [find](https://scholar.google.com/scholar?q=Wolfgang+Ahrendt%2C+Bernhard+Beckert%2C+Reiner+H%C3%A4hnle%2C+Wolfram+Menzel%2C+Wolfgang+Reif%2C+Gerhard+Schellhorn%2C+and+Peter+H%2E+Schmitt%2E+Integrating+automated+Automated+Deduction%16A+Basis+for+Applications+and+inter)
3. Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. [find](https://scholar.google.com/scholar?q=Jesse+Alama%2C+Tom+Heskes%2C+Daniel+K%C3%BChlwein%2C+Evgeni+Tsivtsivadze%2C+and+Josef+Urban%2E)

*Updated 30 October 2026*