ForMath: Formalisation of Mathematics


ForMath is an EU FP7 STREP FET-open project lead by Thierry Coquand at University of Gothenburg.
March 2010--July 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)
EU Flag FP7 Logo

The project has now ended. The experts appointed by the European Commission judged this project achieved excellent results.



Table of contents:

 

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




Scientific Advisory Board


Henri Lombardi
Marie-Francoise Roy
Francis Sergeraert