Thank you, David, for your wishes and your support to publish my contribution. Freek has already updated his web page: http://www.cs.ru.nl/%7Efreek/100/
Alexander On Tuesday, November 26, 2019 at 5:03:22 PM UTC+1, David A. Wheeler wrote: > > 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/ab1dd8b3-4e95-48ad-9982-a268d93644aa%40googlegroups.com.
