WELCOME TO THE MATHDIALOG
FRONT PAGE WEB SITE
Mathdialog is an interactive theorem prover. The goal is to translate a theorem and its proof, which
you must already have, into the CZFC language using Mathdialog. In formal and natural language
mathematics (the mathematical language in which mathematical books are written or in which mathematical
classes are given), hypotheses can be anywhere. In CZFC, hypotheses must be in specific places. In
particular, this means that in CZFC theorems, their hypotheses and thesis are identified. In a proof,
those hypotheses are the starting point, and the thesis is the main goal. The proof steps are executed
with "logic commands", each of which can be executed under its proper conditions and add new hypotheses
and/or a new goal to the proof. When one of those hypotheses matches the main goal, the theorem is
considered proved. That is why you must know the theorem and its proof in natural language before
attempting it in Mathdialog, because there you do not prove, you translate theorems and proofs into the
CZFC mathematical language. For each proof step in the natural mathematical language, you must find a
set of logic commands that map to it. In other words, the task is finding the right set of logic commands
for each step in your natural language proof.
In Mathdialog there is almost nothing obvious. For example, from the natural language definition
X⊂Y if and only if ∀z∈X:z∈Y
it is obvious that if A⊂B and B⊂C and x∈A, then x∈C. If we are required to justify it, we might say: “If x∈A,
then by the definition of A⊂B, x∈B. But if x∈B, then by the definition of B⊂C, x∈C”. That is a very simple
“natural language proof”. Now we will translate it to the CZFC language using Mathdialog. A theorem in CZFC
consists of a name, the hypotheses, and the thesis. In our case, it would look like:
THEOR[SUBSET_P1;A⊂B, B⊂C, x∈A; x∈C]
If we send this to Mathdialog to start a proof, it will respond with:
GOAL: x∈C
HYPOTHESES: A⊂B, B⊂C, x∈A
To continue with the proof, we send the following logic command:
BY_THEOR[x∈B]
Mathdialog will assume x∈B as a hypothesis if and only if there is a theorem whose thesis is x∈B and whose
hypotheses are a subset of the ones already present in our ongoing proof. Then it compares the new hypothesis
x∈B with the goal, in this case, x∈C, and adds it to the set of our existing hypotheses:
HYPOTHESES: A⊂B,B⊂C,x∈A,x∈B
To finish the proof, we send the following logic command:
BY_THEOR[x∈C]
After checking that there is a theorem whose thesis is x∈C, Mathdialog realizes it matches the goal x∈C
and that makes it completes the proof.
This is an illustrative example to give an idea of what it feels like to translate a proof. The process is
called human-to-machine proof because a human user has to feed the machine. The CZFC proof is just the
list of the two logic commands sent: "BY_THEOR[x∈B], BY_THEOR[x∈C]", which Mathdialog stores. From this
simple list, Mathdialog automatically builds an interactive hypertext environment that can show the proof
to other people without knowing anything about Mathdialog or CZFC, furthermore the environment can clear to
the users nearly all their possible doubts about that proof autonomously. This environment is called
machine-to-human proof. You can consult the stored proof right now.
In Mathdialog, you can start building some simple human-to-machine proofs.
Bellow, there are links to the main sources to learn about how to do them:
the article "The interesting and fun game of Mathdialog proofs" and the
Logic-Commands Reference Guide. You can also find a link to a video about how
a human-to-machine proof is done, and to the Mathdialog Practice Area where
you can create your human-to-machine proofs, that others can consult in a
automatically created version named machine-to-human proofs. It shows
your proof in an interactive way that do not need previous knowledge of
Mathdialog.
As many times happen in mathematics, the challenges in Mathdialog are not
only hard but inspiring, exciting, amazing and unexpected.
