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.

If you're new to Lean, there are good educational resources available here. I'm writing a tutorial here, but it's currently incomplete.

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 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.