MizAR 40 for Mizar 40

Abstract

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

References in corpus (2)

• Learning-Assisted Automated Reasoning with Flyspeck
• Premise Selection for Mathematics by Corpus Analysis and Kernel Methods

Cited by in corpus (23)

• DeepMath - Deep Sequence Models for Premise Selection
• TacticToe: Learning to Prove with Tactics
• Premise Selection and External Provers for HOL4
• Holophrasm: a neural Automated Theorem Prover for higher-order logic
• Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling
• Hammering Mizar by Learning Clause Guidance
• HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
• Tactic Learning and Proving for the Coq Proof Assistant
• A Survey on Theorem Provers in Formal Methods
• The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq
• Learning Guided Automated Reasoning: A Brief Survey
• Learning to Prove from Synthetic Theorems
• ProofWatch: Watchlist Guidance for Large Theories in E
• TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
• Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
• Goal Translation for a Hammer for Coq (Extended Abstract)
• Premise selection with neural networks and distributed representation of features
• Parallelizing Mizar
• A Study of Continuous Vector Representationsfor Theorem Proving
• Mining State-Based Models from Proof Corpora
• A Curiously Effective Backtracking Strategy for Connection Tableaux
• Vampire With a Brain Is a Good ITP Hammer
• ENIGMA: Efficient Learning-based Inference Guiding Machine