|
Action Concertée Incitative Nouvelles Interfaces des Mathématiques |
|
|
Projet Mao -- Mathématiques assistées par ordinateur |
|
|
Notre projet regroupe des mathématiciens et des informaticiens pour programmer au-dessus du logiciel Coq une interface munie d'une bibliothèque de ressources mathématiques et destinée à accomplir toutes les tâches que le mathématicien professionnel voudra bien lui confier, au premier rang desquelles: (1.) garantir la correction d'une preuve; (2.) compléter les détails d'une preuve; (3.) conduire des calculs certifiés; (4.) faciliter la découverte et l'édition des preuves. A l'heure actuelle, il existe de nombreux assistants de preuves suffisamment puissants en principe pour formaliser toutes les mathématiques mais aucun n'a été adopté par les mathématiciens professionnels. La raison principale est qu'au niveau de la recherche, le temps nécessaire à l'élaboration d'une preuve formelle est encore prohibitif. Nous proposons une stratégie pour réduire cet obstacle. Cette stratégie comporte des améliorations du logiciel Coq lui-même, le développement que nous avons déjà entrepris d'une interface spécifique, et une discipline de programmation mathématique faisant une large place à des tactiques dédiées chacune à une structure algébrique et censées trouver, dans la majorité des cas, la bonne combinaison de ressources concernant la structure concernée. Notre projet regroupe un noyau de mathématiciens du Laboratoire Dieudonné à Nice avec l'équipe Logical de l'Inria-futurs, qui développe Coq, et l'équipe Lemme de l'Inria-Sophia, qui a déjà développé deux interfaces pour Coq.
(dernière mise à jour du site : 4 juillet 2006) |
|
|
|
|