mlsanityData to 14 Oct 2026

MizAR 40 for Mizar 40

arXiv 1310.2805 ↗First posted 10 Oct 2013cs.AI cs.DL cs.LGcited by 23

Not on the map. Why?

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).

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

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2021: 9; 2022: 3; 2023: 3; 2024: 5; 2025: 2; 2026: 1.

23 papers.

Sort:

By area:

  1. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  2. 2024A Survey on Deep Learning for Theorem Provingcited by 57
  3. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  4. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  5. 2021Learning to Guide a Saturation-Based Theorem Provercited by 15
  6. 2024Graph2Tac: Online Representation Learning of Formal Math Conceptscited by 15
  7. 2021Proving Theorems using Incremental Learning and Hindsight Experience Replaycited by 13
  8. 2021Vampire With a Brain Is a Good ITP Hammercited by 10
  9. 2023Machine-Learned Premise Selection for Leancited by 10
  10. 2021The Role of Entropy in Guiding a Connection Provercited by 8
  11. 2021Fast and Slow Enigmas and Parental Guidancecited by 8
  12. 2022The Isabelle ENIGMAcited by 8
11 more
  1. 2021Learning Theorem Proving Componentscited by 7
  2. 2024Learning Guided Automated Reasoning: A Brief Surveycited by 7
  3. 2023MizAR 60 for Mizar 50cited by 6
  4. 2025Premise Selection for a Lean Hammercited by 6
  5. 2021A Study of Continuous Vector Representationsfor Theorem Provingcited by 4
  6. 2022Machine Learning Meets The Herbrand Universecited by 3
  7. 2024BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Provingcited by 2
  8. 2022Adversarial Learning to Reason in an Arbitrary Logiccited by 1
  9. 2024Solving Hard Mizar Problems with Instantiation and Strategy Inventioncited by 1
  10. 2025Efficient Neural Clause-Selection Reinforcementcited by 0
  11. 2026Governed Deduction: Policy-Grounded Premise Authorization Beyond Relevancecited by 0