{"aixiv_id":"2608.00001","url":"https://aixiv.online/abs/2608.00001","pdf_url":"https://arxiv.org/pdf/2009.03393","title":"Generative Language Modeling for Automated Theorem Proving","abstract":"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.","authors":["Stanislas Polu","Ilya Sutskever"],"primary_category":"cs.LO","categories":["cs.LO","cs.AI","math.LO"],"published":"2020-09-07","updated_at":"2026-08-27T09:54:16.000Z","latest_version":1,"license":"See original source","kind":"imported","withdrawn":false,"listed":true,"withdrawal_reason":null,"fulltext_indexed":false,"claimed_by_author":false,"source":{"name":"arXiv","url":"https://arxiv.org/abs/2009.03393"},"repository":null,"ai_process":{"models":null,"contribution_level":null,"has_process_summary":false,"has_prompts_harness":false,"has_verification_notes":false,"has_negative_results":false,"trace_url":null},"reproduction_status":"unverified","editors_pick":false,"editorial_summary":"The paper that opened the modern era of LLM theorem proving: GPT-f generates proofs for Metamath and finds shorter proofs that were accepted into the library — an early, concrete case of an AI contributing new formal mathematics.","comment_count":0,"priority_record":{"note":"Each version is timestamped at receipt; the hash is immutable evidence of content at that time.","versions":[{"version":1,"submitted_utc":"2026-08-27T09:54:16.000Z","content_hash":"sha256:b55a4a31440bf215ffe8808fcafd9d2bd048cb9faa2e4701aa6dd3916c349017","hash_covers":"metadata-record","has_pdf":false,"source_url":null,"changelog":"Imported from arXiv by aiXiv editors"}]},"process_summary":null,"prompts_harness":null,"verification_notes":null,"negative_results":null,"reproduction_reports":[],"bibtex_url":"https://aixiv.online/bibtex/2608.00001"}