| --- |
| 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. |