coqhammer
Proof automation tool
A tool for automating proof search and verification in dependent type theory using machine learning and external provers.
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
218 stars
8 watching
31 forks
Language: OCaml
last commit: 6 days ago
Linked from 1 awesome list
automationcoqdependent-typeshammerproof-searchtheorem-proververification
Related projects:
| Repository | Description | Stars |
|---|---|---|
 rafaelcgs10/w-in-coq | A Coq formalization of Damas-Milner type system and its algorithm W for verifying the correctness of type inference tools. | 25 |
 coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
 andrew-johnson-4/lsts | A programming language and proof assistant built around type theory and lambda calculus. | 114 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 ecrancemerce/trakt | Automates goal preprocessing in proof automation tactics using a custom-built tool | 14 |
 casper-hansen/autoawq | A Python package implementing Activation-aware Weight Quantization for 4-bit quantized models | 1,758 |
| coq-community/autosubst | Automates formalizing syntactic theories with variable binders in Coq | 52 |
 ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
 coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 188 |
 math-comp/abel | Formalization of mathematical theorems about solvability and Galois theory for polynomials | 28 |
 whonore/coqtail | Enables interactive proof development in Vim similar to other proof assistants. | 274 |
 uwplse/pumpkin-pi | Automatically discovers and proves relationships between types in Coq to simplify proof development and code reuse. | 49 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 384 |
 ml4tp/gamepad | A platform that exposes Coq proofs to machine learning algorithms | 72 |
 mgrabovsky/fm-notes | A collection of notes and resources on formal methods, type theory, and theorem proving using Coq. | 20 |