[Mathématiques constructives]
[retour]
[Computer Algebra]
Formalisation des mathématiques
La formalisation des mathématiques est étroitement reliée à
la compréhension des mathématiques en tant que système de compréhension
du monde via des méthodes scientifiques, algorithmiques.
Un grand nombre de preuves actuellement publiées ne sont crédibles que sur
la base de l'opinion des experts des domaines considérés.
Les systèmes de preuve formalisées semblent devoir être dans l'avenir un
outil indispensable pour la bonne compréhension du fonctionnement des mathématiques.
De grands théorèmes dont les preuves sont extrêmement longues méritent
d'être mieux compris, et parfois véritablement certifiés.
Sur ce sujet voir les exposés de Jeremy Avigad, Julio Rubio et Georges Gonthier au meeting MAP 2011:
Le meeting MAP 2011 au Lorentz Center.
Le projet FORMATH
Une école d'été au printemps
-
International Spring School.
International Spring School
on
FORMALIZATION OF MATHEMATICS
Sophia Antipolis, France
March 12-16, 2012
A growing population of mathematicians, computer scientists, and
engineers use computers to construct and verify proofs of mathematical
results. Among the various approaches to this activity, a fruitful one
relies on interactive theorem proving. When following this approach,
researchers have to use the formal language of a theorem prover to
encode their mathematical knowledge and the proofs they want to
scrutinize. The mathematical knowledge often contains two parts: a
static part describing structures and a dynamic part describing
algorithms. Then proofs are made in a style that is inspired from
usual mathematical practice but often differs enough that it requires
some training. A key ingredient for the mathematical practitioner is
the amount of mathematical knowledge that is already available in the
system's library.
The Coq system is an interactive theorem prover based on Type
Theory. It was recently used to study the proofs of advanced
mathematical results. In particular, it was used to provide a
mechanically verified proof of the four-color theorem and it is now
being used in a long term effort, called Mathematical Components to
verify results in group theory, with a specific focus on the odd order
theorem, also known as the Feit-Thompson theorem. These two examples
rely on a structured library that covers various aspects of finite set
theory, group theory, arithmetic, and algebra.
The current list of speakers is:
- Jeremy Avigad (Pittsburgh, United States)
- Georges Gonthier (Microsoft Research)
- Thomas C. Hales (University of Pittsburgh)
- Julio Rubio (Universidad de La Rioja)
- Bas Spitters (Radboud Universiteit, Nijmegen)
- Vladimir Voevodsky (Institute for advanced study, Princeton)
- Yves Bertot (Inria)
- Assia Mahboubi (Inria)
- Laurence Rideau (Inria)
- Enrico Tassi (MSR-Inria common laboratory)
- Laurent Théry (Inria)
Publications