Metamath
by Norman Megill · first published 2005
5mentions
2recommended by
3HN commenters
2018–2024first – last mentioned
67% recommend33% neutral
Affiliate links. As an Amazon Associate I earn from qualifying purchases.
If you're interested in the main book on Metamath, it is "Metamath: A Computer Language for Mathematical Proofs" by Norman Megill & David A. Wheeler. You can get the hardcover here: http://www.lulu.com/shop/norman-megill-and-david-a-wheeler/m... Full…
on “Metamath Zero, a bootstrapping theorem prover” ↗…verifier software, but from the perspective of us humans we don't choose when a proof checks out or not in a formal system, mathematics does. EDIT: if you are into ML and like this idea, certainly check out MetaMath, the book is very accessible, and the author (Norman Megill) is extremely friendly and helpful. It takes perhaps a few days to a week to learn, study, and reimplement the verifier. One does not at all…
on “NLP's Clever Hans Moment Has Arrived” ↗Related: Metamath (http://www.metamath.org) is a tiny formal language for writing proofs in symbolic logic, as well as a tiny proof checker for the language. The author, Norm Megill, has used Metamath to formalize many…
on “The Foundations of Mathematics (2007) [pdf]” ↗Appeal to "actual" authority is still appeal to authority. Consider an unproven theorem in the MetaMath database. Now consider an amateur mathematician, or perhaps a high school student finding and formalizing a proof. Irrespective of how (un)interesting the theorem is, Norman Megill and the users of MetaMath…
on “The Sounds That Haunted US Diplomats in Cuba? Lovelorn Crickets, Scientists Say” ↗Correct. The good news that Elements still works otherwise, you just need to add the missing axiom. But many other "proofs" have been found to be false. The book "Metamath: A Computer Language for Mathematical Proofs" (by Norm Megill and yours truly) is available at: https://us.metamath.org/downloads/metamath.pdf - see section 1.2.2, "Trusting the Mathematician". We list…
on “New Foundations is consistent – a difficult mathematical proof proved using Lean” ↗