# MizAR 60 for Mizar 50

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 28 of its 60 references that are in the map.
- First posted on arXiv 12 Mar 2023.

## Builds on (most cited first, 28 of 28)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [XGBoost: A Scalable Tree Boosting System](https://mlsanity.com/paper/1603.02754/) (2016)
- [Learning Phrase Representations using RNN Encoder-Decoder for Statistical Machine Translation](https://mlsanity.com/paper/1406.1078/) (2014)
- [Deep Learning for Symbolic Mathematics](https://mlsanity.com/paper/1912.01412/) (2019)
- [ParamILS: An Automatic Algorithm Configuration Framework](https://mlsanity.com/paper/1401.3492/) (2014)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [TacticToe: Learning to Prove with Tactics](https://mlsanity.com/paper/1804.00596/) (2018)
- [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://mlsanity.com/paper/2002.05406/) (2020)
- [First Neural Conjecturing Datasets and Experiments](https://mlsanity.com/paper/2005.14664/) (2020)
- [Can Neural Networks Understand Logical Entailment?](https://mlsanity.com/paper/1802.08535/) (2018)
- [ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E](https://mlsanity.com/paper/1903.03182/) (2019)
- [MizAR 40 for Mizar 40](https://mlsanity.com/paper/1310.2805/) (2013)
- [Property Invariant Embedding for Automated Reasoning](https://mlsanity.com/paper/1911.12073/) (2019)
- [Hammering Mizar by Learning Clause Guidance](https://mlsanity.com/paper/1904.01677/) (2019)
- [Learning to Reason with HOL4 tactics](https://mlsanity.com/paper/1804.00595/) (2018)
- [ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback](https://mlsanity.com/paper/1802.03375/) (2018)
- [Can Neural Networks Learn Symbolic Rewriting?](https://mlsanity.com/paper/1911.04873/) (2019)
- [Stateful Premise Selection by Recurrent Neural Networks](https://mlsanity.com/paper/2004.08212/) (2020)
- [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)
- [Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic](https://mlsanity.com/paper/1910.11797/) (2019)
- [Fast and Slow Enigmas and Parental Guidance](https://mlsanity.com/paper/2107.06750/) (2021)
- [Learning Program Synthesis for Integer Sequences from Scratch](https://mlsanity.com/paper/2202.11908/) (2022)
- [The Isabelle ENIGMA](https://mlsanity.com/paper/2205.01981/) (2022)
- [Learning Theorem Proving Components](https://mlsanity.com/paper/2107.10034/) (2021)
- [BliStrTune: Hierarchical Invention of Theorem Proving Strategies](https://mlsanity.com/paper/1611.08733/) (2016)
- [ENIGMAWatch: ProofWatch Meets ENIGMA](https://mlsanity.com/paper/1905.09565/) (2019)
- [Make E Smart Again](https://mlsanity.com/paper/2004.08858/) (2020)

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

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [Regularization in Spider-Style Strategy Discovery and Schedule Construction](https://mlsanity.com/paper/2403.12869/) (2024)
- [Solving Hard Mizar Problems with Instantiation and Strategy Invention](https://mlsanity.com/paper/2406.17762/) (2024)
- [Machine Learning for Quantifier Selection in cvc5](https://mlsanity.com/paper/2408.14338/) (2024)

## Abstract (arXiv)

As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60% of the Mizar theorems in the hammer setting. We also automatically prove 75% of the Mizar theorems when the automated provers are helped by using only the premises used in the human-written Mizar proofs. We describe the methods and large-scale experiments leading to these results. This includes in particular the E and Vampire provers, their ENIGMA and Deepire learning modifications, a number of learning-based premise selection methods, and the incremental loop that interleaves growing a corpus of millions of ATP proofs with training increasingly strong AI/TP systems on them. We also present a selection of Mizar problems that were proved automatically.