Home

Awesome

<!--- This file was generated from `meta.yml`, please do not edit manually. Follow the instructions on https://github.com/coq-community/templates to regenerate. --->

100 famous theorems proved using Coq

Docker CI Contributing Code of Conduct Zulip

Freek Wiedijk's webpage lists 100 famous theorems and how many of those have been formalised using proof assistants. This repository keeps track of the statements that have been proved using the Coq proof assistant.

You can see the list on this webpage.

Meta

Building instructions

To build all theorems that are hosted in this repository, run the following commands:

git clone https://github.com/coq-community/coq-100-theorems
cd coq-100-theorems
make   # or make -j <number-of-cores-on-your-machine>

Included proofs

This repository also contains Coq proofs of some of the 100 theorems:

How to add a new statement

To add a new statement for one of the therorems, do not modify index.html directly because it is automatically generated. Instead, edit statements.yml. Then, if you have node installed, generate the index file with gen.js > index.html and check it looks as intended in a browser. Finally, make a pull request with both files.

If the proof does not belong to another repository, you can also add a single self-contained .v proof file, in which case you should edit LICENSE.md accordingly.