This page hosts information on Martin Skrodzki's talk "What is … formal mathematics?" at the "What is …?" seminar. This talk will help you better understand the talk by Christoph Benzmüller.
Where & When
Friday, December 16, 2016, 1.00pm @ BMS Loft at Urania
Abstract
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.