I want to wish Alexander van der Vekens a big CONGRATULATIONS for proving the Cayley-Hamilton theorem on 2019-11-25!! This is Metamath 100 proof #49.
That brings our "Metamath 100" total to 72. As of 2019-11-25 this number of proofs is more than Coq (69), Mizar (69), ProofPower (43), Lean (29), nqthm/ACL2 (18), PVS (17), and NuPRL/MetaPRL (8); it is short of only Isabelle (82) and HOL Light (86). More info here: http://us.metamath.org/mm_100.html I've already notified Freek Wiedijk, who tracks progress across various proof systems. You can see the proof here: http://us.metamath.org/mpeuni/cayleyhamilton.html There are still proofs left to do! If you're interested, here's the list of "Metamath 100" proofs not yet done: http://us.metamath.org/mm_100.html#todo --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1iZdJA-0004cz-5r%40rmmprod07.runbox.
