• View
• Edit
• History
• Print

ForMath: Formalisation of Mathematics

ForMath is an EU FP7 STREP FET-open project lead by Thierry Coquand at University of Gothenburg. March 2010--February 2013, Grant agreement nr. 243847 For any matter related to the project please contact the project manager Ana Bove. (Glossary: FP7 = Seventh Framework Programme; STREP = Specific Targeted Research Projects; FET = Future and Emerging Technologies)

Table of contents:

• Project Summary
• Research Methodology
• List of Beneficiaries
• Scientific Advisory Board

Project Summary

Mathematics is already playing a crucial role in the design of sophisticated systems that are used daily as for example in geometrical modelling, robotics, cryptography, ... This use of mathematics will only increase, and issues of correctness and reliable specification of these systems will become more and more important. Besides its purely conceptual interest, the development of formalised mathematics is a promising way to tackle new technological challenges.

Concretely, the objective of this project is to develop libraries of formalised mathematics concerning algebra, linear algebra, real number computation, and algebraic topology. The libraries that we plan to develop in this proposal are especially chosen to have long-term applications in areas where software interacts with the physical world. The main originality of the work is to structure these libraries as a software development, relying on a basis that has already shown its power in the formal proof of the four-colour theorem, and to address topics that were mostly left untouched by previous research in formal proof or formal methods.

The main milestones of this work will concern formally proved algorithms for solving problems in real arithmetics and in algebraic topology. We have entered an era of mathematical proofs of extraordinary complexity that may indicate a change in our understanding of mathematical reasoning. Two examples of such complex proofs are the four-colour theorem, and the recent solution by T. Hales of the Kepler conjecture, that both involve computers in a crucial way. Can we trust such proofs? To address this problem, mathematicians and computer scientists have started research on formal proofs, where every logical inference step can be checked by a computer. With interactive computer-based proof systems, researchers can verify algorithms whenever a complete mathematical specification is feasible. So practically, the goal of this project is to make formal proof verification available to domains that were hitherto beyond the reach of proof systems.

List of Beneficiaries

• University of Gothenburg (UGOT): Thierry Coquand, Anders Mörtberg, Vincent Siles.
  Project manager Ana Bove.
• Radboud University Nijmegen (SKU): Herman Geuvers, Bas Spitters, Robbert Krebbers, Eelis van der Weegen, Jelle Herold, Evgeny Makarov, Egbert Rijke.
• INRIA: Yves Bertot, Cyril Cohen, Maxime Denčs, Georges Gonthier (Microsoft Research),Victor Magron, Assia Mahboubi, Loďc Pottier, Laurence Rideau, Enrico Tassi, Laurent Théry, Benjamin Werner.
• Universidad de La Rioja (ULR): Julio Rubio, Laureano Lambán, César Domínguez, Jesús Aransay, Vico Pascual, Jónathan Heras, María Poza, Jose Divasón, Rubén Sáenz.

Scientific Advisory Board

Henri Lombardi
Marie-Francoise Roy
Francis Sergeraert