“Generative Language Modeling for Automated Theorem Proving”, 2020-09-07 (; similar):
We explore the application of transformer-based language models to automated theorem proving. This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans—the generation of original mathematical terms—might be addressable via generation from language models.
We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance. GPT-f found new short proofs that were accepted into the main Metamath library, which is to our knowledge, the first time a deep-learning based system has contributed proofs that were adopted by a formal mathematics community.
Also notable: the benefits of pretraining on Arxiv etc, despite likely including no or only redundant Metamath, and primarily natural language text, showing transfer learning of general math knowledge to abstract low-level formal proof language. See also: “PACT: Proof Artifact Co-training for Theorem Proving with Language Models”, lean-gptf (for Lean), “SymbolicGPT: A Generative Transformer Model for Symbolic Regression”, “Measuring Mathematical Problem Solving With the MATH Dataset”/“Measuring Coding Challenge Competence With APPS”, “Learning to Prove Theorems by Learning to Generate Theorems”, “TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning”.