Am 2. Juli 2017 wurde mein erster Beitrag zur Metamath-Bibliothek set.mm veröffentlicht, nämlich Theorem 2reu5 und dazu benötigte Hilfssätze. Es geht hier um "Double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification", also um prädikatenlogische Aussagen mit zweifachen Eindeutigkeitsquantoren der Form

Ich beschäftige mich schon seit einiger Zeit mit Metamath, einem einfachen System zum Beweisen mathematischer Aussagen, wobei die Beweise detailliert bis auf die Axiome zurückgeführt werden. Die mit diesem System bereits erzielten Ergebnisse sind ebenfalls beeindruckend. Mehr Informationen dazu gibt es auf der Metamath Homepage http://de.metamath.org/index.html bzw. auf der Einstiegsseite aller bereits bewiesenen Theoreme http://de.metamath.org/mpegif/mmtheorems.html.