Abstract
This article explores the application of transformer-based language models to automated theorem proving. A primary motivation for this work is addressing a significant limitation of automated theorem provers when compared to human mathematicians: the generation of original mathematical terms. Language models present a potential solution to this challenge.
An automated prover and proof assistant, named GPT‑f, was developed for the Metamath formalization language. Its performance was thoroughly analyzed. GPT‑f successfully discovered new short proofs that were subsequently accepted into the main Metamath library. This achievement represents, to current knowledge, the first instance of a deep-learning based system contributing proofs that have been adopted by a formal mathematics community.
