CoqGym
Coq simulator
A learning environment for theorem proving with the Coq proof assistant
A Learning Environment for Theorem Proving with the Coq proof assistant
384 stars
15 watching
50 forks
Language: Coq
last commit: over 1 year ago icml-2019machine-learningtheorem-proving
Related projects:
| Repository | Description | Stars |
|---|---|---|
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
| ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
 ml4tp/gamepad | A platform that exposes Coq proofs to machine learning algorithms | 72 |
 eugeneloy/coq_jupyter | A Jupyter notebook kernel for interactive theorem proving with Coq | 94 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
 math-comp/tutorial_material | Tutorials and materials for teaching Coq-based mathematical component development | 17 |
 whonore/coqtail | Enables interactive proof development in Vim similar to other proof assistants. | 274 |
 plclub/lngen | Tool for generating Coq definitions and proofs for locally nameless representations | 30 |
 coq-community/coq-art | Coq proof assistant book with exercises and examples | 110 |
| coq-community/coq-100-theorems | Repository tracking famous theorems proved using proof assistants. | 55 |
 coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 188 |
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 354 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |