2018/06/02 by Daniel Huang, Huang, Daniel, Prafulla Dhariwal +5 · 35 citations
Computer Science · Mathematics · #Algebra over a field #Algorithm #Analytic proof #Artificial Intelligence (cs.AI) #Automated proof checking #Automated theorem proving #Calculus (dental) #Computer science #Computer-assisted proof #Construct (python library) #Discrete mathematics #FOS: Computer and information sciences #Formal proof #Geometry #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Machine Learning (cs.LG) #Machine Learning (stat.ML) #Mathematical proof #Mathematics #Mathematics, Computing, and Information Processing #Programming language #Proof assistant #Pure mathematics #Simple (philosophy) #Theoretical computer science #cs.AI #cs.LG #cs.LO #stat.ML
paper · pdf · doi:10.48550/arxiv.1806.00608
published in arXiv (Cornell University) (Cornell University)
openalex publication_date 2018/06/02 · arxiv created 2018/12/21 · arxiv updated 2018/12/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
In this paper, we introduce a system called GamePad that can be used to explore the application of machine learning methods to theorem proving in the Coq proof assistant. Interactive theorem provers such as Coq enable users to construct machine-checkable proofs in a step-by-step manner. Hence, they provide an opportunity to explore theorem proving with human supervision. We use GamePad to synthesize proofs for a simple algebraic rewrite problem and train baseline models for a formalization of the Feit-Thompson theorem. We address position evaluation (i.e., predict the number of proof steps left) and tactic prediction (i.e., predict the next proof step) tasks, which arise naturally in tactic-based theorem proving.