Am 9. Oktober 2018 habe ich den Beweis des "Friendship Theorem" in Metamath fertiggestellt. Dieses Theorem gehört zu den 100 mathematischen Theoremen, die formell bewiesen werden sollen (siehe Formalizing 100 Theorems von Freek Wiedijk, Theorem #83). Es ist ein Theorem der Graphentheorie, beschrieben und zuerst bewiesen 1966 von P. Erdös et al. Es wird auch in "Proofs from THE BOOK" von M. Aigner und G. Ziegler und (kurz) in Wikipedia (siehe Freundschaftssatz) erwähnt. Mein Beweis ist eine Formalisierung des Beweises von C. Huneke von 2002 im Artikel "The Friendship Theorem".

Eine aktuelle Übersicht aller mit Metamath bewiesenen Theoreme der "100 Theorem List" ist unter Metamath 100 verfügbar. Das "Friendship Theorem" selbst (und sein Beweis) kann unter friendship eingesehen werden. Formalisiert lautet das Theorem:

The friendship theorem:
In every finite (nonempty) friendship graph there is a vertex which is adjacent to all other vertices.

⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))

Mehr Informationen zu Metamath gibt es auf der Metamath Homepage http://de.metamath.org/index.html bzw. auf der offiziellen Einstiegsseite aller bereits bewiesenen Theoreme http://de.metamath.org/mpegif/mmtheorems.html.