Proofs

This is my personal repository of formally verified mathematics, including results from category theory, type theory, domain theory, etc. The proofs are verified using the Coq proof assistant.

If you want to set up your own repository of formally verified mathematics, you can simply fork this repository and replace the contents of the proofs directory with your own proofs. Setting up a Coq project from scratch is not particularly straightforward, so this scaffolding can save you time.

If you are new to Coq, the repository contains a tutorial here. I recommend Software Foundations and Certified Programming with Dependent Types for further learning.

Instructions

Make sure you have the dependencies listed below. Then you can run make in this directory to verify all the proofs. If you change anything, run make again to to incrementally verify the affected proofs. You can run the linters with make lint. The build artifacts can be removed with make clean.

To write proofs, you'll want to use an IDE that supports interactive theorem proving. My general recommendation is VsCoq, which is a plugin for Visual Studio Code. However, you may find the built-in CoqIDE easier if you're new to interactive theorem proving, since it has buttons you can click on to step through your proofs.

Dependencies

You'll need the following:

• Coq >= 8.15.0
  • Make sure to update your PATH to include the location of the Coq binaries (coqc, coqdep, etc.).
• GNU Make >= 3.79.1
  • You also need these common Unix tools: echo, find, and rm. If you have make, you probably already have those other programs too.
• Ruby >= 2.6.8
  • This is only needed by make lint.