Mathematics, Algorithms and Proofs 2012

MAP 2012 - Mathematics, Algorithms and Proofs

Universität Konstanz, Germany, September 17 - September 21, 2012

The conference bropught together people from the communities of formal proofs, constructive mathematics, computer algebra and real algebraic geometry (in a wide meaning). It is a continuation of previous meeting in Dagstuhl (2003 and 2005), Luminy (2004), Castro Urdiales (2006), Leiden (2007 and 2011), Trieste (2008), Monastir (2009) and Logroño (2010). The slogan on this 2012 edition in Konstanz (situated at Lake of Constance, Germany, not far from Zürich, Switzerland) was "MAP meets RAGEA and GEOLMI and presents FORMATH".

The European project FORMATH (Formalization of Mathematics) is an outgrowth of the previous MAP meetings and deals with computer verified development, of both proofs and algorithms, in group theory, algebraic topology, linear algebra and computational analysis. The French project GEOLMI (Geometry and Algebra of Linear Matrix Inequalities with Systems Control Applications) and the German project RAGEA (Real Algebraic Geometry and Emerging Applications) deal among others with positive polynomials, sums of squares, linear matrix inequalities, determinantal and semidefinite representations, noncommutative real algebraic geometry and system control applications.

The objective of the conference is to bridge the gap between conceptual (abstract) and computational (constructive) mathematics by providing a computational understanding of abstract mathematics. We are not only interested in correct algorithms however, but also in the mathematical clarity that these concrete presentations provide. In formal proof management systems like Coq there is an increasing interest to exploit certificates found by numerical solvers (e.g., sums of squares certificates for positivity found by semidefinite programming solvers). The theory behind these certificates was one highlight of this 2012 edition of MAP.