This project intends to formally verify encodings of logic gates, cardinality constraints, and other methods of specifying a mathematical problem into propositional logic.

I am working on this project to fulfill the requirements of a research master's degree at Carnegie Mellon University. My research page can be found at http://www.crcodel.com. My advisors' research pages are found at https://www.andrew.cmu.edu/user/avigad/ and https://www.cs.cmu.edu/~mheule/, respectively.

To install, clone the repo, then type

> leanproject install mathlib

at the root directory to install the mathematical libraries and other components of Lean that are needed. You will need Lean installed. Visit this site (site URL?) for instructions on how to install Lean.

If you have an account with Gitpod or are willing to sign up for one, you can browse the repository in your browser, running Lean in the cloud.