The area of Automated Reasoning finds its early origins in Leibniz's ideas. Whitehead and Russell's efforts in the early 20th century to formalise mathematics (in the sense of expressing mathematics in symbolic logic) in their Principia Mathematica resulted in the introduction of type theory. Later on, in the late 1960's, de Bruijn developed the AUTOMATH mathematical language, a predecessor of type theoretical proof assistants. Since then, proof assistants (also known as interactive theorem provers) have come a long way. Nowadays, modern proof assistants such as Isabelle/HOL, Lean and Coq feature extensive libraries of formalised mathematics. Proof assistants are rapidly becoming increasingly popular among mathematicians and mathematics students. We will discuss the use of proof assistants to formalise mathematics referring to the state of the art and to recent developments involving the formalisation of advanced, research-level mathematics. As an example of an Isabelle/HOL formalisation, we will also see a formalisation of Aristotle's Assertoric Syllogistic.
Topics related to this course can be found here and here. Here are the slides.