[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Intent to package: metamath

MetaMath is:
  - a computer language for pure mathematics
  - a rigorous mathematical proof verifier 
  - a tool for writing mathematical proofs
  - a metamathematical philosophy
  - a manual of abstract mathematics

MetaMath was written by Norman D. Megill <ndm@shore.net>.
Quoting from the Preface of the manual:
"Why did I develop Metamath?  I enjoy abstract mathematics, but I
get lost in a barrage of definitions and start to lose confidence that
my proofs are correct.  Or I reach a point where I lose sight of how
I'm doing relates to the axioms that a theory is based on and am
suspicious that there may be some overlooked implicit axiom accidentally
introduced along the way (as happened historically with Euclidean
whose omission of Pasch's axiom went unnoticed for 2000 years).  I'm
also somewhat lazy and wish to avoid the effort involved in 
re-verifying the gaps in informal proofs "left to the reader"; I prefer
to figure them out just once and not have to go through the same
a year from now when I've forgotten what I did.  Metamath provides
recovery of my efforts than scraps of paper that I can't decipher
But mostly I find very appealing the idea of rigorously archiving,
mathematical knowledge in a computer database, providing precision,
certainty, and elimination of human error."

URI: <ftp://ftp.shore.net/members/ndm/Readme.txt>

Reply to: