Mathematische Wahrheiten gelten häufig als unumstößlich. Aber am Ende des Tages stellt sich heraus, dass auch Mathematik menschengemacht ist, und ihre Korrektheit – zumindest bis vor kurzem – einzig darauf beruht, dass Mathematiker in jedem Schritt eine logisch korrekte Folgerung ziehen. Genauso mag ein Computer an sich fehlerfrei rechnen, wenn er aber ein fehlerhaftes Programm ausführt, liefert er nicht das richtige Ergebnis.

Eine Lösung für diese Herausforderungen bieten Beweisassistenten, Computer-Programme, in denen sich formale Schlussfolgerungen mit automatischer Hilfe erstellen lassen und automatisch überprüft werden. Ziel des Kurses ist es, sich in den Beweisassistenten Isabelle einzuarbeiten. Dabei wird mit grundlegenden und elementaren Strukturen und Konzepten, wie Gleichungen, Listen und vollständiger Induktion, begonnen; dann wird sich dran gewagt, zahlentheoretische Begriffe und Beweise, wie Gruppen und den Satz von Lagrange, zu formalisieren; um schließlich diese Ergebnisse auf bekannte Verfahren der Informationssicherheit, wie RSA (Rivest–Shamir–Adleman) und DSA (Digital Signature Algorithm), anzuwenden.

Um diese mutigen Ziele zu erreichen, werden sich die Teilnehmenden bereits vor dem Kurs nicht nur einzelne mathematische Inhalte erarbeiten, sondern bereits anfangen, sich in Kleingruppen mit Isabelle vertraut zu machen. Auch während des Kurses wird sich die Kursarbeit in einen gemeinsamen theoretischen Teil und einen praktischen Teil gliedern, in dem jede/jeder Teilnehmende eigenständig, unterstützt durch die Kursleiter, formalisiert. Der praktische Teil wird wahrscheinlich überwiegen.