Lorentz Center - Mathematics: Algorithms and Proofs from 28 Nov 2011 through 2 Dec 2011
  Current Workshop  |   Overview   Back  |   Home   |   Search   |     

    Mathematics: Algorithms and Proofs
    from 28 Nov 2011 through 2 Dec 2011


The main goal of the workshop was to `achieve a fruitful interaction between the implementors of computer mathematics, both verified and unverified, and core mathematicians and logicians.' This goal was certainly achieved, the workshop was very lively and stimulating to many participants. Moreover, the meeting was a good venue for the ForMath project to gather and to present their work to a wider audience. With 55 registered participants and 5 to 10 unregistered participants coming in for a couple of days, this was the biggest MAP-meeting since to workshop series was started in 2003. Abstracts and slides of most of the presentations are available from the workshop homepage. The presentations can roughly be divided in three groups.

Computational and constructive mathematics: This includes the two tutorials, by Barakat and Quadrat and by Simpson and Escardo, and the presentations by Avigad, Bauer, Griffin, Mannaa, van der Vorst, Yengui. This kind of work is either an application of the methodologies developed within MAP, or a direction in which we envision that these methodologies will be useful.

Formal proofs: Cohen, Gonthier, Rubio and Théry presented the state of the art in formalizing mathematics in type theory. In all presentations it was essential to have a good overview of the mathematics is before formalizing it. In Rubio's case the computer verification of software for algebraic topology lead to the correction of a mathematical result.

Homotopy type theory: The developing field of homotopy type theory, a marriage between abstract homotopy theory, type theory and higher dimensional category theory, was a very stimulating meeting point for many participants. There were lectures on this topic by Awodey, Harper, Hyland, Kapulkin, Moerdijk and Streicher.

It was a great pleasure to be welcomed in the Lorentz center. Especially, the availability of offices was greatly appreciated by many participants. We would like to heartily thank its very efficient and helpful staff.


Thierry Coquand (Göteborg, Sweden)

Henri Lombardi (Franche-Comte, France)

Marie-Francoise Roy (Rennes, France)

Bas Spitters (Nijmegen, the Netherlands)