Proofs

This is my personal repository of formally verified mathematics, including results from category theory, type theory, domain theory, etc., and some original research. All the proofs are verified using the Rocq 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 Rocq project from scratch isn't particularly straightforward, so this scaffolding can save you time.

If you're new to Rocq, start with the 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, you can run make again to incrementally verify the affected proofs. 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 recommendation is VsRocq, which is a plugin for Visual Studio Code.

Dependencies

You'll need the following:

• Rocq >= 9.0.0
  • Make sure to update your PATH to include the location of the rocq binary.
• GNU Make >= 3.79.1
  • You also need these common Unix tools: cp, find, and rm. If you have make, you probably already have those other programs too.