CoqGym extracted proof states, environments, goals, tactics and proof trees from open-source Coq projects and exposed them through a programmatic interaction layer.
Kaiyu Yang and Jia Deng released CoqGym, a dataset and interactive environment built from 71,000 human-written proofs across 123 Coq projects, together with ASTactic, a deep-learning model that generates tactics as abstract syntax trees and was reported to prove held-out theorems beyond the reach of the compared built-in automated tactics.
CoqGym extracted proof states, environments, goals, tactics and proof trees from open-source Coq projects and exposed them through a programmatic interaction layer. ASTactic learned proof-step generation from this corpus and composed tactics from runtime syntax rather than relying only on a predetermined list of complete tactics.
CoqGym made learning-based theorem proving on a mature interactive proof assistant substantially more data-rich and reproducible. Its environment-and-corpus design anticipated later projects such as LeanDojo that similarly expose large proof-assistant libraries as reusable machine-learning infrastructure.
Significance rationale: CoqGym turned a large collection of real Coq developments into an interactive machine-learning environment containing tens of thousands of human proofs, while ASTactic generated structured tactics rather than choosing only from a fixed tactic vocabulary. The environment became an important early template for later proof-assistant learning infrastructure.
The arXiv and ICML research records establish CoqGym, ASTactic, the dataset scale and the reported held-out theorem-proving experiments. Machine checking refers to proofs accepted by Coq and does not imply independent reproduction of the reported success rates.
The public CoqGym repository exposes the interaction environment, extraction pipeline, proof corpus tooling and ASTactic implementation. E3 denotes artifact-level inspectability rather than independent verification of every experimental claim.
No corrections recorded.
