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 Lean theorem prover or the Rocq proof assistant. Currently, most of the proofs are written in Rocq.

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_lean or the proofs_rocq directories with your own proofs. Setting up a Rocq project from scratch isn't particularly straightforward, so this scaffolding can save you time.

For people who are new to Lean, I have a tutorial here. Theorem Proving in Lean 4 and Functional Programming in Lean are great resources for further learning.

I also have a Rocq tutorial here. Check out Software Foundations and Certified Programming with Dependent Types as well.

Instructions

Make sure you have the dependencies listed below. Then you can run lake build to verify the Lean proofs or make to verify the Rocq proofs. If you change anything, you can run those commands again to incrementally verify the affected proofs. The build artifacts can be removed with lake clean (for Lean) or make clean (for Rocq).

To write proofs, you'll want to use an IDE that supports interactive theorem proving. For Lean, use the Lean 4 extension for Visual Studio Code. For Rocq, my recommendation is VsRocq, which is also a Visual Studio Code extension.

Dependencies

You'll need the following:

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