mlsanityData to 14 Oct 2026

MizAR 60 for Mizar 50

arXiv 2303.06686 ↗First posted 12 Mar 2023cs.AI cs.LG cs.LOcited by 6

Not on the map. Why?

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.

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

28 of 60 references.

References · 28

  1. 2017Attention Is All You Needcited by 60,361
  2. 2016XGBoost: A Scalable Tree Boosting Systemcited by 5,166
  3. 2014Learning Phrase Representations using RNN Encoder-Decoder for Statistical Machine Translationcited by 4,057
  4. 2019Deep Learning for Symbolic Mathematicscited by 270
  5. 2014ParamILS: An Automatic Algorithm Configuration Frameworkcited by 89
  6. 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 53
  7. 2018TacticToe: Learning to Prove with Tacticscited by 44
  8. 2020ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)cited by 26
  9. 2020First Neural Conjecturing Datasets and Experimentscited by 26
  10. 2018Can Neural Networks Understand Logical Entailment?cited by 24
  11. 2019ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for Ecited by 24
  12. 2013MizAR 40 for Mizar 40cited by 23
16 more
  1. 2019Property Invariant Embedding for Automated Reasoningcited by 22
  2. 2019Hammering Mizar by Learning Clause Guidancecited by 20
  3. 2018Learning to Reason with HOL4 tacticscited by 14
  4. 2018ATPboost: Learning Premise Selection in Binary Setting with ATP Feedbackcited by 12
  5. 2019Can Neural Networks Learn Symbolic Rewriting?cited by 12
  6. 2020Stateful Premise Selection by Recurrent Neural Networkscited by 11
  7. 2021Vampire With a Brain Is a Good ITP Hammercited by 10
  8. 2023Alien Codingcited by 9
  9. 2019Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logiccited by 8
  10. 2021Fast and Slow Enigmas and Parental Guidancecited by 8
  11. 2022Learning Program Synthesis for Integer Sequences from Scratchcited by 8
  12. 2022The Isabelle ENIGMAcited by 8
  13. 2021Learning Theorem Proving Componentscited by 7
  14. 2016BliStrTune: Hierarchical Invention of Theorem Proving Strategiescited by 5
  15. 2019ENIGMAWatch: ProofWatch Meets ENIGMAcited by 5
  16. 2020Make E Smart Againcited by 4

Built on by

Cited by year

Citing papers per year: 2024: 6.

6 papers.

  1. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 81
  2. 2024A Survey on Deep Learning for Theorem Provingcited by 57
  3. 2024Learning Guided Automated Reasoning: A Brief Surveycited by 7
  4. 2024Regularization in Spider-Style Strategy Discovery and Schedule Constructioncited by 2
  5. 2024Solving Hard Mizar Problems with Instantiation and Strategy Inventioncited by 1
  6. 2024Machine Learning for Quantifier Selection in cvc5cited by 0