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 Starts here 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.
