After the death of Alexander Grothendieck (13-Nov-2014) the Grothendieck Circle has recommenced its project to collect material from and about this great and unusual man. It remains to be seen how much we can understand from someone who isolated himself from the world so radically.

As a result of the APPA workshop at Vienna Summer of Logic 2014, there is now a book available with the collected contributions by the invited experts (including myself). It is edited by Bruno Woltzenlogel Paleo and David Delahaye, and is published by College Publications. Here is a copy of the abstract from it:

The development of new and improved proof systems, proof formats and proof search methods is one of the most essential goals of Logic. But what is a proof? What makes a proof better than another? How can a proof be found efficiently? How can a proof be used? Logicians from different communities usually provide radically different answers to such questions. Their principles may be folklore within their own communities but are often unknown to outsiders.

This book provides a snapshot of the current state of the art in proof search and proof production as implemented in contemporary automated reasoning tools such as SAT-solvers, SMT-solvers, first-order and higher-order automated theorem provers and proof assistants. Furthermore, various trends in proof theory, such as the calculus of inductive constructions, deduction modulo, deep inference, foundational proof certificates and cut-elimination, are surveyed; and applications of formal proofs are illustrated in the areas of cryptography, verification and mathematical proof mining.

Experts in these topics were invited to present tutorials about proofs during the Vienna Summer of Logic and the chapters in this book reflect their tutorials. Therefore, each chapter is intended to be accessible not only to experts but also to novice researchers from all fields of Logic.

My contribution to the book is a chapter on “Interactive Theorem Proving — from the perspective of Isabelle/Isar”, with the following abstract:

Interactive Theorem Proving (ITP) has a long tradition, going back to the 1970s when interaction was introduced as a concept in computing. The main provers in use today can be traced back over 20–30 years of development. As common traits there are usually strong logical systems at the bottom, with many layers of add-on tools around the logical core, and big applications of formalized mathematics or formal methods. There is a general attitude towards flexibility and open-endedness in the combination of logical tools: typical interactive provers use automated provers and disprovers routinely in their portfolio.

The subsequent exposition of ITP takes Isabelle/Isar as the focal point to explain concepts of the greater “LCF family”, which includes Coq and various HOL systems. Isabelle itself shares much of the relatively simple logical foundations of HOL, but follows Coq in the ambition to deliver a sophisticated system to end-users, without requiring self-assembly of individual parts. Isabelle today is probably the most advanced proof assistant concerning its architecture and extra-logical infrastructure.

The Isar aspect of Isabelle refers first to the structured language for human-readable and machine-checkable proof documents, but also to the Isabelle architecture that emerged around the logical framework in the past 10 years. Thus Isabelle/Isar provides extra structural integrity beyond the core logical framework, with native support for parallel proof processing and asynchronous interaction in its Prover IDE (PIDE).

The Conferences on Intelligent Computer Mathematics (CICM) — with the distinctive sub-conferences Calculemus, DML, MKM — may be seen as a gathering of fringe groups, but a very interesting one. Traditionally, it may serve as a forum for experimentation and unorthodox contributions that are difficult to publish elsewhere.

I have served several times on the PC of Calculemus or MKM, and once as PC chair of MKM. For CICM 2015, I am PC member for Calculemus.

Don’t be confused by the website that is somewhat difficult to navigate! Don’t miss the start of the submission process: 16-Feb-2015 for abstracts, followed by actual papers, followed the  rebuttal phase. The latter is particularly important to readjust the initial verdict by the reviewers, going upwards or downwards, depending on careful reactions of the authors to what was said about their papers.

Born 28-Mar-1928 (Berlin, Germany), died 13-Nov-2014 (Saint-Lizier, France).

In my own studies, I have occasionally encountered the famous name of Grothendieck in lectures about functional analysis and logic. From a bit later, I remember discussions with Helmut Schwichtenberg about Tarski-Grothendieck set theory as the foundation of the formal mathematical language of Mizar.

In 2010, I came again across the name of Alexander Grothendieck several times, when searching the web about my new hometown Bures-sur-Yvette, where I lived until August 2014 only a few hundred meters from the famous IHÉS institute. That was the place where Grothendieck worked for some time at the peak of his mathematical life (until 1970). Afterwards he removed himself more and more from public and scientific life.

Winfried Scharlau has started to publish material about the life of Grothendieck some years ago, with this notable article from 2006/2008. There was also some activity on the web to collect more information, but this was stopped abruptly in 2010 with this angry letter from Grothendieck himself, speaking to the world from a secret place in the Pyrenees.

At least we now know that his last residence was in Lasserre (l’Ariège); see also this article of La Depeche.

Here is another blog with many more links.