This is a project by Cayden Codel, advised by Jeremy Avigad and Marijn Heule. It intends to formally verify encodings of Boolean functions, cardinality constraints, and other methods of specifying mathematical problems in propositional logic.

At the root of this project is a file lib_info.txt. The file contains a summary of the library's structure and important definitions in each file.

You can install Lean following the instructions at https://leanprover-community.github.io/get_started.html#regular-install.

Assuming you have Lean installed, you can fetch and build this repository as follows:

  leanproject get ccodel/verified-encodings
  cd verified-encodings
  leanproject build

You can then open folder in VS Code and browse the files.

If Lean complains about mathlib (Lean's community math library) not being installed, you can change your directory to the project's root and type

  leanproject get-mathlib-cache

to locally download mathlib files.

If you have an account with Gitpod, you can instead browse the repository in your browser, running Lean in the cloud. If you don't have an account with Gitpod, clicking the button will prompt you to create one.

Gitpod offers 50 free hours of workspace time every month. When you are done, choose "Stop workspace" from the menu in the upper left corner to stop the clock. Alternatively, Gitpod will stop it for you after 30 minutes, or 3 minutes after you close the browser window or tab.