Welcome to the Friendship Theorem in Coq project website!
This project contains a Coq proof of the Friendship Theorem in graph theory, following Proofs from THE BOOK, 4th ed., Aigner et. al. pp. 257-259, 2010.
This is an open source project, licensed under the MIT License.
The current stable release of Friendship Theorem in Coq can be downloaded from GitHub.
The coqdoc presentation of the source files can be browsed here
Related publications, if any, are listed below.