meta.yml

---
fullname: 100 famous theorems proved using Coq
shortname: coq-100-theorems
organization: coq-community
community: true
action: true

synopsis: Coq theorems from the list of 100 famous theorems

description: |-
  [Freek Wiedijk's webpage](http://www.cs.ru.nl/~freek/100/) lists
  [100 famous theorems](http://pirate.shu.edu/~kahlnath/Top100.html)
  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](https://coq.inria.fr/).

  You can see the list on [this webpage](https://madiot.fr/coq100).

authors:
- name: Jean-Marie Madiot
- name: Frédéric Chardard

maintainers:
- name: Jean-Marie Madiot
  nickname: jmadiot

opam-file-maintainer: palmskog@gmail.com

opam-file-version: dev

license:
  fullname: MIT License
  identifier: MIT

supported_coq_versions:
  text: 8.10 or later
  opam: '{>= "8.10"}'

tested_coq_opam_versions:
- version: dev
- version: '8.16'
- version: '8.15'
- version: '8.14'
- version: '8.13'
- version: '8.12'
- version: '8.11'
- version: '8.10'

dependencies:
- opam:
    name: coq-coquelicot
    version: '{>= "3.1.0"}'
  description: |-
    [Coquelicot 3.1.0 or later](http://coquelicot.saclay.inria.fr)

namespace: Coq100Theorems

build: |-
 ## Building instructions

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

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

keywords:
- name: famous theorems

categories:
- name: Mathematics/Algebra

documentation: |
  ## Included proofs

  This repository also contains Coq proofs of some of the 100 theorems:
  - [ballot.v](ballot.v) for the [Ballot Theorem](https://en.wikipedia.org/wiki/Bertrand%27s_ballot_theorem)
  - [birthday.v](birthday.v) for the [Birthday Problem](https://en.wikipedia.org/wiki/Birthday_problem)
  - [cardan_ferrari.v](cardan_ferrari.v) for The Solution of a [Cubic](https://en.wikipedia.org/wiki/Cubic_equation) and the Solution of a [Quartic](https://en.wikipedia.org/wiki/Quartic_equation)
  - [div3.v](div3.v) for [Divisibility by 3 Rule](https://en.wikipedia.org/wiki/Divisibility_rule#Divisibility_by_3_or_9)
  - [inclusionexclusion.v](inclusionexclusion.v) for the [Inclusion/Exclusion Principle](https://en.wikipedia.org/wiki/Inclusion%E2%80%93exclusion_principle#Statement)
  - [konigsberg_bridges.v](konigsberg_bridges.v) for the [Konigsberg Bridges Problem](https://en.wikipedia.org/wiki/Seven_Bridges_of_K%C3%B6nigsberg)
  - [mean.v](mean.v) for the [Arithmetic Mean/Geometric Mean](https://en.wikipedia.org/wiki/Inequality_of_arithmetic_and_geometric_means#The_inequality)
  - [sumarith.v](sumarith.v) for [Sum of an arithmetic series](https://en.wikipedia.org/wiki/Arithmetic_progression#Sum)
  - [sumkthpowers.v](sumkthpowers.v) for [Sum of kth powers](https://en.wikipedia.org/wiki/Bernoulli_polynomials#Sums_of_pth_powers)
---