Abstract

We explore the application of transformer-based language models to automatedtheorem proving. This work is motivated by the possibility that a majorlimitation of automated theorem provers compared to humans -- the generation oforiginal mathematical terms -- might be addressable via generation fromlanguage models. We present an automated prover and proof assistant, GPT-f, forthe Metamath formalization language, and analyze its performance. GPT-f foundnew short proofs that were accepted into the main Metamath library, which is toour knowledge, the first time a deep-learning based system has contributedproofs that were adopted by a formal mathematics community.

 

Quick Read (beta)