Hi all, FYI, I recently found out about Metamatix <https://github.com/acorrenson/metamatix>, a verified implementation of a metamath proof checker, written in Coq.
I'm not sure how far the project goes, but it's probably of interest for people in this group. BR, _ Thierry -- 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/afe05c58-2988-3f65-89f5-4569b6d507e7%40gmx.net.
