Proof and Computation 2022

30 May - 2 June 2022, Schlehdorf monastery (Kloster Schlehdorf)

About | Programme | Photos | Venue | Travel Information | Accommodation | Organisers | Sponsors



Proofs in mathematical practice serve to warrant the truth of mathematical theorems. Proof theory arose with Hilbert's programme to put abstract mathematics on a firm basis by proving consistency in the meta-mathematics and by finite methods only. Gödel's incompleteness theorems have allegedly dashed Hilbert's programme as such but thus have stood at the beginning of a seminal paradigm shift in proof theory: to see mathematical proofs also as a rich source of computational information such as certified algorithms and effective bounds. Contemporary research in this fertile area is known under terms such as dynamical methods, program extraction and proof mining.

Incidentally, today's quest for safety and reliability of data and algorithms is very similar to the debate on foundations of mathematics about a century ago which culminated in Hilbert's and Gödel's advances---today, however, with grave consequences for technology and economy. The key to solving these problems of the digital society up to artificial intelligence is to be found in the logical grounding of mathematics and computer science themselves, the current development of which leads to new joint research methods and perspectives in mathematics and computer science.

In this vein, an international meeting will be held from 30 May to 2 June 2022 at Cohaus Schlehdorf in Bavaria. The aim of this meeting is to bring together eminent scholars and young researchers active in the foundations of mathematics and computer science. There will be ample opportunity to form ad-hoc groups working on specific projects, but also to discuss in more general terms the vision of extracting computational information from proofs. The participants' expertise will include ordinal analysis, predicative foundations, constructive mathematics, type theory, computation in higher types, proof mining and program extraction from proofs.


Slots below include time for discussion.


Both symposium and workshop take place at Cohaus Kloster Schlehdorf. Schlehdorf abbey, originally a Benedictine monastery, then a convent of the Missionary Dominican Sisters of King William's Town, is held by a housing cooperative since 2019. For a brief history and future concept see also here (in German).

Travel information

Please note that FFP2 masks are required in public transport in Germany.

We recommend to buy a Regio-Ticket Werdenfels (€23 + €8 for each additional passenger for groups of up to 5 persons) which is valid in the Munich S-Bahn, regional trains to Kochel, and busses to Schlehdorf. This can be bought at every train ticket vending machine as well as online.
Departure will profit from the €9-Ticket, available from 1 June and valid in local and regional transport throughout Germany.

More information on German Railway DB and rural bus transport can be obtained from For public transport in Munich please consult


Accommodation will be organised by the P&C team. Rooms have been booked at Cohaus Kloster Schlehdorf, Hotel Klosterbräu, and Pension Killer, situated within short walking distance to the venue.



Financial support through the following foundations is gratefully acknowledged:

Kloster Schlehdorf I.jpg
By Berreu, CC BY-SA 3.0, Link