Am 25. November 2019 habe ich den Beweis des Satzes von Cayley-Hamilton (Cayley-Hamilton theorem) in Metamath fertiggestellt. Der Satz von Cayley-Hamilton besagt, dass jede quadratische Matrix ihrer charakteristischen Gleichung genügt (siehe Wikipedia https://de.wikipedia.org/wiki/Satz_von_Cayley-Hamilton). Dieses Theorem gehört zu den 100 mathematischen Theoremen, die formell bewiesen werden sollen (siehe Formalizing 100 Theorems von Freek Wiedijk, Theorem #49).

Eine aktuelle Übersicht aller mit Metamath bewiesenen Theoreme der "100 Theorem List" ist unter Metamath 100 verfügbar. Der Satz von Cayley-Hamilton selbst (und sein Beweis) kann unter cayleyhamilton 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.