Intent to package: metamath

[Fredrick Paul Eisele <phreed@ameritech.net>]

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
sometimes
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
anything
I'm doing relates to the axioms that a theory is based on and am
sometimes
suspicious that there may be some overlooked implicit axiom accidentally
introduced along the way (as happened historically with Euclidean
geometry,
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
frustration
a year from now when I've forgotten what I did.  Metamath provides
better
recovery of my efforts than scraps of paper that I can't decipher
anymore.
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>
              or
     <http://www1.shore.net/~ndm/java/mm.html>