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