To call something Formal Mathematics seems to be redundant. However, the field has its own merits, some of which shall be exemplified in the talk. We will take some initial steps to clarify what we understand by the notion of "proof". Having done this, we go on to formally prove a part of de Morgan's law. Furthermore, the "Donkey Sentence" will raise our awareness for difficulties in formal proofs. Finally, we will briefly get into the topic of Automated Theorem Provers and consider the famous proof of the irrationality of sqrt(2), formalized in Isabelle.