Annotation
Seminar is intended for those interested in interactive proof systems that allow formal verification of mathematical proofs. The content of the seminar is a hands on introduction to the Isabelle/HOL proof assistant at the user level allowing the formalization of specific selected topics.