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
proofsdirectory 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.
Read in full here:
This thread was posted by one of our members via one of our news source trackers.