# MizAR 40 for Mizar 40

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

## Key facts

- Cited by 23 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Oct 2013.

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

- [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)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Learning to Guide a Saturation-Based Theorem Prover](https://mlsanity.com/paper/2106.03906/) (2021)
- [Graph2Tac: Online Representation Learning of Formal Math Concepts](https://mlsanity.com/paper/2401.02949/) (2024)
- [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)
- [Machine-Learned Premise Selection for Lean](https://mlsanity.com/paper/2304.00994/) (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)
- [Premise Selection for a Lean Hammer](https://mlsanity.com/paper/2506.07477/) (2025)
- [A Study of Continuous Vector Representationsfor Theorem Proving](https://mlsanity.com/paper/2101.09142/) (2021)
- [Machine Learning Meets The Herbrand Universe](https://mlsanity.com/paper/2210.03590/) (2022)
- [BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving](https://mlsanity.com/paper/2403.03401/) (2024)
- [Adversarial Learning to Reason in an Arbitrary Logic](https://mlsanity.com/paper/2204.02737/) (2022)
- [Solving Hard Mizar Problems with Instantiation and Strategy Invention](https://mlsanity.com/paper/2406.17762/) (2024)
- [Efficient Neural Clause-Selection Reinforcement](https://mlsanity.com/paper/2503.07792/) (2025)
- [Governed Deduction: Policy-Grounded Premise Authorization Beyond Relevance](https://mlsanity.com/paper/2609.31029/) (2026)

## Abstract (arXiv)

As a present to Mizar on its 40th anniversary, we develop an AI/ATP system that in 30 seconds of real time on a 14-CPU machine automatically proves 40% of the theorems in the latest official version of the Mizar Mathematical Library (MML). This is a considerable improvement over previous performance of large- theory AI/ATP methods measured on the whole MML. To achieve that, a large suite of AI/ATP methods is employed and further developed. We implement the most useful methods efficiently, to scale them to the 150000 formulas in MML. This reduces the training times over the corpus to 1-3 seconds, allowing a simple practical deployment of the methods in the online automated reasoning service for the Mizar users (MizAR).