GamePad: A learning environment for theorem proving

OpenAI Blog Papers
theorem-proving machine-learning coq proof-synthesis interactive-theorem-prover

Summary

OpenAI introduces GamePad, a learning environment for applying machine learning to theorem proving in the Coq proof assistant, enabling proof synthesis and training baseline models for tactic prediction and position evaluation tasks.

No content available
Original Article Export to Word Export to PDF
View Cached Full Text

Cached at: 04/20/26, 02:43 PM

# GamePad: A learning environment for theorem proving Source: [https://openai.com/index/gamepad/](https://openai.com/index/gamepad/) OpenAI## Abstract 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\.

Similar Articles

Generative language modeling for automated theorem proving

OpenAI Blog

OpenAI presents GPT-f, a transformer-based automated theorem prover for the Metamath formalization language, which discovered new short proofs accepted into the main Metamath library — marking the first time a deep-learning system contributed proofs adopted by a formal mathematics community.

OpenAI Gym Beta

OpenAI Blog

OpenAI releases OpenAI Gym, a public beta toolkit for developing and comparing reinforcement learning algorithms with a growing suite of environments and a platform for reproducible research. The toolkit aims to standardize RL benchmarks and address the lack of diverse, easy-to-use environments for the research community.

Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4

arXiv cs.CL

This paper introduces Discover and Prove (DAP), an open-source agentic framework for automated theorem proving in Lean 4 that tackles 'Hard Mode' problems where the answer must be discovered independently before formal proof construction. The work releases new Hard Mode benchmark variants and achieves state-of-the-art results while revealing a significant gap between LLM answer accuracy (>80%) and formal prover success (<10%).

Learning to play Minecraft with Video PreTraining

OpenAI Blog

OpenAI introduced Video PreTraining (VPT), a semi-supervised method that trains neural networks to play Minecraft by learning from 70,000 hours of unlabeled human gameplay video combined with a small labeled dataset. The model learns complex sequential tasks using the native human interface (keyboard and mouse) and demonstrates capabilities like crafting diamond tools and pillar jumping, representing progress toward general computer-using agents.