# Hammering Mizar by Learning Clause Guidance

arXiv: https://arxiv.org/abs/1904.01677 · HTML: https://mlsanity.com/paper/1904.01677/

## Key facts

- Cited by 20 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 Apr 2019.

## Built on by (most cited first, 20 of 20)

- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Learning to Guide a Saturation-Based Theorem Prover](https://mlsanity.com/paper/2106.03906/) (2021)
- [Proving Theorems using Incremental Learning and Hindsight Experience Replay](https://mlsanity.com/paper/2112.10664/) (2021)
- [Vampire With a Brain Is a Good ITP Hammer](https://mlsanity.com/paper/2102.03529/) (2021)
- [Alien Coding](https://mlsanity.com/paper/2301.11479/) (2023)
- [The Role of Entropy in Guiding a Connection Prover](https://mlsanity.com/paper/2105.14706/) (2021)
- [Fast and Slow Enigmas and Parental Guidance](https://mlsanity.com/paper/2107.06750/) (2021)
- [The Isabelle ENIGMA](https://mlsanity.com/paper/2205.01981/) (2022)
- [Learning Theorem Proving Components](https://mlsanity.com/paper/2107.10034/) (2021)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [MizAR 60 for Mizar 50](https://mlsanity.com/paper/2303.06686/) (2023)
- [Learning Conjecturing from Scratch](https://mlsanity.com/paper/2503.01389/) (2025)
- [Towards AI-assisted Neutrino Flavor Theory Design](https://mlsanity.com/paper/2506.08080/) (2025)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Improving ENIGMA-Style Clause Selection While Learning From History](https://mlsanity.com/paper/2102.13564/) (2021)
- [Solving Hard Mizar Problems with Instantiation and Strategy Invention](https://mlsanity.com/paper/2406.17762/) (2024)
- [Translating SUMO-K to Higher-Order Set Theory](https://mlsanity.com/paper/2305.07903/) (2023)
- [Machine Learning for Quantifier Selection in cvc5](https://mlsanity.com/paper/2408.14338/) (2024)
- [Efficient Neural Clause-Selection Reinforcement](https://mlsanity.com/paper/2503.07792/) (2025)

## Abstract (arXiv)

We describe a very large improvement of existing hammer-style proof automation over large ITP libraries by combining learning and theorem proving. In particular, we have integrated state-of-the-art machine learners into the E automated theorem prover, and developed methods that allow learning and efficient internal guidance of E over the whole Mizar library. The resulting trained system improves the real-time performance of E on the Mizar library by 70% in a single-strategy setting.