Daniel Luckhardt

Mathematisches Institut, Georg-August-Universität Göttingen

Course on Isabelle, February 20 to 22

Would you bet 800€ on the correctness of your last proof? If not, haven't you at least once wished to have a method at hand to be really sure of your results?

Theorem provers are computer programs designed to write and verify proofs. You may have already heard about computer based formalization of proofs for some theorems like the four color theorem or, more recently, the Feit-Thompson theorem (a key part in the classification of finite simple groups). Whilst these purely mathematical applications still hold out the prospect of one day changing the way of working in our science, applications in industry are already in existence, for example, the functional correctness of the seL4 microkernel, developed for high security applications, was proved using the proof assistant Isabelle.


The aim of the course is to introduce working mathematicians to the world of interactive and automated theorem proving — mostly from the perspective of Isabelle/HOL, but with some outlook on systems like HOL-Light, Coq, Mizar.

There will be some lectures with background information, while most of the time is dedicated to practical exercises by the participants. Notable topics:

The target audience consists of graduate students and researchers with strong background in pure mathematics. However the concrete prerequisites are quite limited, in particular, knowledge in logic or other related areas is not required.


The course is held from February 20 to 22, 2017 at the Mathematical Institut. A preliminary discussion takes place on Friday, February 17 from 10 am to 12 noon. Attendance is recommended for participants without any background in logic. All classes are located in the Sitzungszimmer.

We are going to use the official release Isabelle2016-1 (December 2016), which is available for Linux, Windows, Mac OS X. Every participant has to bring his own laptop that has a dual core processor and 4 GB RAM as a minimum (ideally four cores and 8 GB RAM). The software should be installed in advance.

Sitzungszimmer, Mathematisches Institut, Bunsenstraße 3-5, Göt­tin­gen
Maximal number of participants
Registrate in Stud.IP. If not applicable, contact organizer.
As number of participant is very limited early registration recommended.
Lecturer and tutor
Makarius Wenzel (Isabelle architect and release manager)
Daniel Luckhardt
RTG Mathematical Structures in Modern Quantum Physics

Preliminary Schedule

Monday Tuesday Wednesday
09:00-10:30 Session 1 Session 1 Session 1
10:30-11:00 Coffee break Coffee break Coffee break
11:00-12:30 Session 2 Session 2 Session 2
12:30-14:30 Lunch break Lunch break Lunch break
14:30-16:00 Session 3 Session 3 Session 3
16:00-16:30 Coffee break Coffee break Coffee break
16:30-18:00 Session 4 Session 4 Session 4