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:
If we send this to Mathdialog to start a proof, it will respond with:
To continue with the proof, we send the following logic command:
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:  
To finish the proof, we send the following logic command:
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.

Copyright 2021 by Carlos E. Freites
Legal stuff