Transcript Slide 1

MetaMath
Presentation for Proof Assistant course
by
Nadya Kalabishka
Plan







Introduction
Metamath program
Other works connected to Metamath
Metamath language
Demo
Metamath music page
Material about Metamath
Introduction
 What is Metamath?
Metamath is a tiny language that can express theorems in
abstract mathematics, accompanied by proofs that can be
verified by a computer program.
It’s a proof checker. It has no specific logic embedded and
can simply be regarded as a device to apply inference rules
to formulas.
 Why is it called Metamath?
It means "metavariable math."
Introduction
 Who is the developer of
metamath program?
Norman Megill of Massachusetts Institute of Technology.
 Why metamath program was
written?
One of the seminal ideas that lead Megill to design
Metamath was the desire to precisely determine the
correctness of some proofs.
Metamath program
Metamath comes along with two main databases set.mm
and ql.mm. Three Internet interfaces ( The Metamath Proof
Explorer, the Hilbert Space Explorer and the Quantum
Logic Explorer ) are provided to explore these two
databases in a human friendly way.
set.mm stores theorems concerning ZFC theory. The
underlying logic is classical propositional calculus and
classical predicate calculus with equality. Its contain about
8000 (As of March 2008) fully formal proofs of
mathematical theorems. set.mm has been maintained for
more than ten years now (the first proofs in set.mm are
dated August 1993). It is mainly a work by Norman Megill
but there are also proofs made by other participants.
Metamath program
Reading set.mm we may have sometimes the impression
that the ambition of its author is essentially to add all the
mathematics one theorem after the other.
ql.mm develops a set of quantum logic theorems.
The Metamath program (version 0.07.44 12-May-2009),
which is an ANSI C program with a command-line
interface. It was used to build and verify the proofs in the
Metamath Proof Explorer.
Metamath program
 Hilbert Space Explorer
The Hilbert Space Explorer presents more than 1,000
theorems pertaining to the Hilbert space theory. Those
theorems are included in set.mm. They are not shown in the
Metamath Proof Explorer because they had been developed
by adding extra-axioms to the standard ZFC axioms of
set.mm. This adding (justified by historical opportunity
reasons) is theoretically useless since the concept of Hilbert
space can be designed with the standard ZFC axioms.
Metamath program
 Quantum Logic Explorer
Quantum logic theorems can be found in the database
ql.mm. The Quantum Logic Explorer is an internet interface
to this database.
In practice it looks like...
Other works connected to
Metamath
 Proof checkers:
Using the design ideas implemented in Metamath, Raph
Levien has implemented what might be the smallest proof
checker in the world, mmverify.py, at only 500 lines of
Python code.
Ghilbert is a similar language based on mmverify.py.
Other works connected to
Metamath
 Proof checkers:
Using Levien seminal works, many other implementations
of the Metamath design principles have been implemented
for a broad variety of languages. Juha Arpiainen has
implemented his own proof checker in Common Lisp called
Bourbaki and Marnix Klooster has coded a proof checker
in Haskell called Hmm.
Metamath language
The Metamath language is based on a very small number of
tokens. There are two tokens to declare the symbols of the
logic:
1. declare the constants ($c)
2. declare the variables ($v).
Syntactic rules and axioms are declared using the $a token,
and inference rules are declared using the $a for the
conclusion and the $e for the premises. Finally, $p is used
to declare a theorem and its proof.
Metamath language
 Proof:
A proof is a sequence of statement labels.
The label sequence in a proof specifies a construction in
reverse Polish notation (RPN). Its works like hand-held
calculators. In the calculator analogy, a hypothesis label is
like a number and an assertion label is like an operation.
RPN process involve the concept of a stack, which is a set
of temporary memory locations that hold results.
Metamath language
 Proof:
When Metamath encounters a hypothesis label it places
or pushes the math symbol sequence of the hypothesis onto
the stack.
Finally, Metamath removes or pops the matched hypotheses
from the stack and pushes the substituted assertion onto the
stack.
Demo
 Very easy example:
Let’s prove that t = t:
Theorem scheme:
The axioms of our theory:
(A1) (t = r -> (t = s -> r = s))
(A2)
(t + 0) = t
We also will use a theorem that if P and (P->Q) then Q (Modus
Ponens)
Demo
 Proof:
1.
2.
3.
4.
5.
(t + 0) = t (by axiom A2)
(t + 0) = t (by axiom A2)
((t + 0) = t -> ((t + 0) = t -> t = t)) (by axiom A1)
((t + 0) = t -> t = t) (by MP applied to
steps 2 and 3)
t = t (by MP applied to
steps 1 and 4)
Material about Metamath
 MetaMath home page:
http://us.metamath.org
 Wiki:
http://wiki.planetmath.org/AsteroidMeta/metamath