Human Folly about “Metamath”

Index (us.metamath.org):
the #Metamath proof databases like set.mm are bundled into the 17MB download. #formal-methods
on 02022-05-21
Item (news.ycombinator.com):
discussion of #Metamath Zero. #foundations-of-mathematics #formal-methods
on 02021-01-15
(arxiv.org):
“Specifying verified x86 software from scratch” Mario Carneiro wants to prove a #Metamath verifier correct with #Metamath. #foundations-of-mathematics #formal-methods
on 02021-01-15
(arxiv.org):
“Specifying verified x86 software from scratch” Mario Carneiro wants to prove a #Metamath verifier correct with #Metamath. #foundations-of-mathematics #formal-methods
on 02021-01-15
Mmverify (us.metamath.org):
Raph #Levien’s #Metamath verifier in 300 lines of Python. #formal-methods #foundations-of-mathematics
on 02021-01-15
Lean and Metamath zero (slawekk.wordpress.com):
notes on #formal-methods alternatives for #foundations-of-mathematics, covering #Xena, #Kevin-Buzzard, #LEAN, and #Metamath
on 02021-01-15