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:
- Isabelle/HOL as background theory for specifications in typed set-theory;
- Isabelle/Pure as logical framework for Natural Deduction;
- Isabelle/Isar as structured proof language for formalized mathematics;
- Isabelle/PIDE as integrated tool platform for mechanized reasoning and functional programming;
- Isabelle document preparation as formal version of LaTeX.
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.
- Maximal number of participants
- Lecturer and tutor
- Sitzungszimmer, Mathematisches Institut, Bunsenstraße 3-5, Göttingen
- Registrate in Stud.IP.
If not applicable, contact organizer.
As number of participant is very limited early registration recommended.
- Makarius Wenzel (Isabelle architect and release manager)
- Daniel Luckhardt
- RTG Mathematical Structures in Modern Quantum Physics
|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|