Action Concertée Incitative

Nouvelles Interfaces des Mathématiques

Projet Mao -- Mathématiques assistées par ordinateur

Description courte du projet

1- Nous comptons doter la version 9 de Coq d'un système de modules beaucoup plus puissant, d'un polymorphisme d'univers explicite, et d'un meilleur langage de tactiques.

2- Nous comptons que notre interface sera dès la prochaine rentrée universitaire assez robuste pour résister aux cohortes d'étudiants de première année. Elle devrait ensuite rapidement être utilisable dans tout le cursus mathématique.

3- Nous allons mettre en place dès cette année notre site qui rendra disponible sans procédure d'installation tout ce dont nous disposons pour faire des mathématiques formelles.

4- Nous comptons continuer à développer les bases de la géométrie algébrique et parallèlement produire des mathématiques formelles originales à travers nos cobayes. Nous comptons recruter et former de plus en plus de cobayes au fur et à mesure du développement de notre environnement (accessoirement nous pensons que cette pratique des mathématiques formelles sera un atout pour l'avenir de ces doctorants).

5- Nous espérons produire régulièrement des contributions méta-théoriques.

Nous pensons disposer de tous les atouts nécessaires pour réussir dans notre entreprise. En effet notre projet repose sur trois mathématiciens de réputation internationale (Hirschowitz, Simpson, Xiao). Ces mathématiciens sont totalement immergés dans le milieu mathématique et disposent de la possibilité supplémentaire de diffuser nos idées et nos produits par le biais de l'enseignement. Nous utilisons l'assistant de preuves Coq, qui est l'un des plus performants sur le marché. L'équipe LogiCal de l'Inria, qui développe Coq participe à notre projet qui constitue pour elle un défi important. Tandis que l'équipe Lemme de l'Inria-Sophia, qui a une grande expérience en la matière, élabore l'interface dont nous avons besoin. L'expérience de collaboration informelle mise en place depuis deux ans entre nos trois équipes nous permet de nous prétendre capables de faire les choix qui s'imposent en concertation et en tirant pleinement parti de la diversité de nos compétences.

(dernière mise à jour du site : 14 décembre 2004)

Coordinateur du projet

Partenaires

Objectifs

Projets

Démos

Contexte

Présentations

Activités