Mizar in a Nutshell

By Adam Grabowski, Artur Korniłowicz, Adam Naumowicz. 2010

186 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Language and Linguistics, Natural Language Processing

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. Quoc V. Le
2. Mohit Bansal
3. Yuhuai Wu
4. Jia Deng
5. Yoshua Bengio
6. Percy Liang
7. Sergey Levine
8. Jianfeng Gao

In Language and Linguistics

1. The mathlib Community
2. Ibrahim Abdelaziz
3. Cezary Kaliszyk
4. Veronika Thost
5. Michael Färber
6. Josef Urban
7. Achille Fokoue
8. Maxwell Crouse

In Natural Language Processing

1. Yuhuai Wu
2. Wenda Li
3. Lawrence Charles Paulson
4. Lei Yu
5. Christian Szegedy
6. Achille Fokoue
7. Veronika Thost
8. Ibrahim Abdelaziz

Citations in the corpus

• Solving Quantitative Reasoning Problems with Language Models (2022, methodology): “This can be achieved using specialized programming languages that facilitate the simulation of logical and mathematical thinking using a computer, such as Coq [20], Isabelle [21], HOL4 [22], Lean [23], Metamath [24] and Mizar [25].”
• DeepMath - Deep Sequence Models for Premise Selection (2016, background): “ITP systems include HOL (Light) [15], Isabelle [37], Mizar [13], Coq [7], and ACL2 [23].”
• An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic (2020, methodology): “On Mizar, most graph-based encodings lead to much shorter proofs than their pattern-based counterparts (for the problems they could solve) with GCNs finding the shortest proofs (confirmed by further experiments) followed by MPNN and others; larger values indicate shorter proofs.”
• IsarStep: a Benchmark for High-level Mathematical Reasoning (2021, background): “The declarative style proof is also available in Mizar (Grabowski et al., 2010), where the style originates.”
• ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (2023, methodology): “This work directly depends on Lean’s mathlib , but indirectly benefits from lessons learned from other proofs systems such as Coq [Bertot and Castéran, 2004], Mizar [Grabowski et al., 2010], and Isabelle [Nipkow et al., 2002].”
• Monte Carlo Connection Prover (2016, background): “2008), HOL4 (Slind and Norrish 2008), HOL Light (Harrison 1996), and Mizar (Grabowski et al. 2010) have led to a significant improvement of the usability of ITPs (Blanchette et al.”
• Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling (2019, methodology): “nct regions of a tree-based representation). We evaluate the binary classification performance of our models on the premise selection task with the Mizar dataset arXiv:1911.06904v1 [cs.AI] 15 Nov 2019 [16], and on the proof step classification task with the HolStep dataset [11]. The experiments show t”
• Reinforcement Learning of Theorem Proving (2018, methodology): “Section 4 evaluates the system on a large corpus of problems extracted from the Mizar Mathematical Library [13].”
• Monte Carlo Tableau Proof Search (2016, methodology): “…versions of Vampire [4] and research on the InstGen calculus in iProver [16], but also more practical improvements, such as more efficient and precise term indexing techniques [24], efficient non-clausal tableau proof search [20], or the use of machine learning for problem size reduction [12].”
• The lean mathematical library (2019, methodology): “tructure hierarchy, Mizar uses a soft typing system whereby users register associations that are used by the checker. The library has developed quite an elaborate hierarchy in this way [29] (see also [28, 39]). To our knowledge, there is no formal specification of the inferences that are accepted by”
• Deep Network Guided Proof Search (2017, methodology): “The Mizar Mathematical Library (MML) (Grabowski et al., 2015) is a library of formal mathematics developed on top of the Mizar system (Bancerek et al., 2015).”