Metamath A Computer Language for Pure Mathematics

By Norman D. Megill. 1969

Subfields: Natural Language Processing, Program Analysis & Verification

How researchers see this paper

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

In Natural Language Processing

In Program Analysis & Verification

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].”
Formal Mathematics Statement Curriculum Learning (2022, neutral): “Unlike Metamath (Megill & Wheeler, 2019), which has been studied in the original GPT-f paper (Polu & Sutskever, 2020), Lean beneﬁts from high-level tactics which were shown to be beneﬁcial in the context of the miniF2F benchmark (Zheng et al., 2021)–Lean proofs are typically 10x shorter than Metamat”
History of Interactive Theorem Proving (2014, methodology): “Similar crosslinking is today available for Coq21 (using the coqdoc tool) and for MetaMath [Megill, 1996] developments.22 Practically all large ITP libraries, such as the Isabelle Archive of Formal Proofs23, the Coq Users’ Contributions24, and the HOL Light, Flyspeck and HOL4 libraries, are easily a”
Deep Network Guided Proof Search (2017, background): “Examples include the formal proof of the Kepler conjecture (Hales et al., 2015), or the proof of correctness of the seL4 operating system kernel (Klein et al., 2010). ar X iv :1 70 1.”
GamePad: A Learning Environment for Theorem Proving (2018, unknown): “Holphrasm (Whalen, 2016) uses string encodings of proof states and focuses on tactic argument synthesis (there is essentially only one tactic in the underlying ITP MetaMath (Megill, 2007)).”
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version) (2019, background): “Whalen [21] proposed a purely deep reinforcement learning based solution for theorem proving for the Metamath prover [22].”
Holophrasm: a neural Automated Theorem Prover for higher-order logic (2016, methodology): “The system uses a variant of UCT [12], an algorithm for the tree-based multi-armed bandit problem, to search the space of partial proof trees of a Metamath theorem.”