---
license: lgpl-2.1
---

The ASTactic model in the paper:  

[Learning to Prove Theorems via Interacting with Proof Assistants](https://arxiv.org/abs/1905.09381)      
[Kaiyu Yang](https://yangky11.github.io/) and [Jia Deng](https://www.cs.princeton.edu/~jiadeng/)  
International Conference on Machine Learning (ICML) 2019   

```bibtex
@inproceedings{yang2019coqgym,
  title={Learning to Prove Theorems via Interacting with Proof Assistants},
  author={Yang, Kaiyu and Deng, Jia},
  booktitle={International Conference on Machine Learning (ICML)},
  year={2019}
}
```

Please visit https://github.com/princeton-vl/CoqGym for details.