Awesome

100 famous theorems proved using Coq

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

• Author(s):
  • Jean-Marie Madiot
  • Frédéric Chardard
• Coq-community maintainer(s):
  • Jean-Marie Madiot (@jmadiot)
• License: MIT License
• Compatible Coq versions: 8.10 or later
• Additional dependencies:
  • Coquelicot 3.1.0 or later
• Coq namespace: Coq100Theorems
• Related publication(s): none

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:

• ballot.v for the Ballot Theorem
• birthday.v for the Birthday Problem
• cardan_ferrari.v for The Solution of a Cubic and the Solution of a Quartic
• div3.v for Divisibility by 3 Rule
• inclusionexclusion.v for the Inclusion/Exclusion Principle
• konigsberg_bridges.v for the Konigsberg Bridges Problem
• mean.v for the Arithmetic Mean/Geometric Mean
• sumarith.v for Sum of an arithmetic series
• sumkthpowers.v for Sum of kth powers

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.