princeton-vl/CoqGym

Provides a dataset of 123K+ Coq proofs extracted from real projects via SerAPI, enabling machine learning models to learn proof tactics by interacting with the proof assistant through structured JSON and S-expression representations. Built around an interactive environment that tracks proof states, goals, and tactic applications, with pre-trained neural models (ASTactic) that predict proof steps from abstract syntax trees. Includes Docker integration, LMDB-indexed proof data, and utilities for parsing Coq terms and computing dataset statistics.

414 stars. No commits in the last 6 months.