Primary evidence
- GamePad: A Learning Environment for Theorem ProvingS1 · Primary research · Paper · 2018-06-02
- GamePad Coq learning environmentS1 · Primary research · Repository
GamePad exposes Coq proof traces and interaction as a machine-learning environment
GamePad instruments Coq so proof states, proof steps, mid-level and kernel-level terms and proof trees can be represented as Python data structures.
What happened?
Daniel Huang, Prafulla Dhariwal, Dawn Song and Ilya Sutskever released GamePad, a Python environment for extracting and manipulating Coq proof traces and interacting with Coq. The paper used the environment to synthesize proofs for a simple algebraic rewrite task and to train baseline models for position evaluation and tactic prediction on a formalization of the Feit–Thompson theorem.
GamePad instruments Coq so proof states, proof steps, mid-level and kernel-level terms and proof trees can be represented as Python data structures. A lightweight coqtop wrapper lets learning code send tactics and receive parsed proof states, while released tooling supports extracting data from the Mathematical Components odd-order development.
Why it matters
The project helped establish proof assistants as interactive machine-learning environments rather than only sources of static theorem corpora. That interface pattern became important for later systems that train models by repeatedly observing proof states and acting inside a trusted prover.
Significance rationale: GamePad was an early proof-assistant machine-learning environment that exposed Coq proof states, steps, trees and interactive tactic execution through Python. Its environment-plus-proof-trace design directly preceded larger-scale Coq learning infrastructure such as CoqGym, whose paper identifies GamePad as its closest prior work.
Historical context
Earlier developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- Substantive AI support
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- Machine-learning models predicted proof progress and tactics, and the environment supported automated proof synthesis on a simple rewrite task; the main historical contribution was the reusable Coq interaction and trace infrastructure rather than a new mathematical proof.
- Human contribution
- Researchers instrumented Coq, designed the Python representations and interaction API, prepared the Feit–Thompson-derived data workflow, implemented baseline learning tasks and evaluated the environment.
- Verification
- Paper released · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-15
Technical details
- Systems
- gamepad, coq
- Organizations
- university-of-california-berkeley, openai
- Problems
- coq-theorem-proving
- Methods
- interactive-theorem-proving, tactic-prediction, proof-state-representation, proof-trace-extraction, machine-learning-environment
Sources & artifacts
- GamePad: A Learning Environment for Theorem ProvingS1 · Primary research · Paper · accessed 2026-09-15
- GamePad Coq learning environmentS1 · Primary research · Repository · accessed 2026-09-15
- GamePad Coq learning environment and proof-trace toolingArtifact · Code
Verification history
- 2018-06-02 · Paper released · E2 · Research record
The arXiv research record establishes GamePad, its Coq interaction design and the reported proof-synthesis and prediction experiments.
- 2026-09-15 · Paper released · E3 · Inspectable artifact
The public GamePad repository exposes the Coq tracing setup, Python interaction library, examples and data/model workflow. E3 records artifact-level inspectability rather than independent reproduction of every experiment.
Corrections
No corrections recorded.