Am 21. Februar 2019 habe ich den Beweis der "Cramerschen Regel"  ("Cramer's rule") zur Bestimmung der Lösung von linearen Gleichungssystemen mithilfe von Determinanten 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 #97).

Eine aktuelle Übersicht aller mit Metamath bewiesenen Theoreme der "100 Theorem List" ist unter Metamath 100 verfügbar. Die "Cramersche Regel" selbst (und ihr Beweis) kann unter cramer eingesehen werden.

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.