Warwick Tucker

Preuves assistées par ordinateur – une approche hiérarchique

L’objectif du projet de recherche est d’associer les techniques du calcul scientifique moderne à la rigueur des mathématiques et de développer une fondation fonctionnelle pour résoudre des problèmes mathématiques avec l’aide d’ordinateurs. Il s’agit de progresser dans l’analyse du domaine des preuves assistées par ordinateur, à partir d’une forte conviction qu’il s’agit du seul moyen de s’emparer de certains problèmes mathématiques très complexes. L’objectif à long terme est de développer une plateforme avec laquelle on peut aborder un problème informatique à tous les (ou l’un des) trois niveaux de rigueur (calcul numérique, calculs validés, preuves formelles). La première étape sera peut-être de commencer par un calcul numérique pour stimuler le comportement d’un système particulier. Une fois qu’un phénomène intéressant aura été observé, il devrait être possible de passer à un calcul validé, incorporant toute discrétisation ou erreurs d’arrondi. L’étape finale sera de vérifier par une preuve formelle que toutes les étapes précédentes étaient valides.