Warwick
Tucker

• MATHEMATIQUES

PROJET

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.

BIOGRAPHIE

Warwick Tucker est professeur de mathématiques à l’Université d’Uppsala, Suède. Après avoir soutenu son doctorat dans ces mêmes discipline et université en 1998, en démontrant l’existence de l’attracteur de Lorenz, il a passé deux ans à l’IMPA à Rio de Janeiro, Brésil comme chercheur post-doctoral. De 2000 à 2002, Tucker a été professeur assistant H.C. Wang à Cornell University (Ithaca, USA). Pendant cette période, il a obtenu le prix de la Société suédoise Wallenberg de mathématiques et le prix R.E. Moore pour les applications d’analyse d’intervalles. À son retour en Suède, il a bénéficié d’une bourse de cinq ans de l’Académie royale des sciences. En 2004, il a reçu le prix de la Société mathématique européenne pour ses contributions remarquées à la discipline. En 2007, il a constitué le groupe CAPA à l’Université de Bergen (Norvège). En 2009, ce groupe a déménagé vers son implantation actuelle d’Uppsala où Tucker est élu professeur en 2011, et directeur de son département en 2014.

PUBLICATIONS PRINCIPALES

• Tucker, W., Validated Numerics -- A short introduction to rigorous computations, Princeton University Press, 2011.
• Tucker, W., The Lorenz attractor exists, C. R. Acad. Sci. Paris, t. 328, Série I, 1197--1202, 1999.
• Tucker, W., A Rigorous ODE Solver and Smale's 14th Problem, Foundations of Computational Mathematics, 2:1, 53--117, 2002.
• Bartha, F.A. and Tucker, W., Fixed points of a destabilized Kuramoto-Sivashinsky equation, Applied Mathematics and Computation, 266, 339–349, 2015.
• Galias, Z. and Tucker, W., Is the Hénon map chaotic? , Chaos 25, 033102, 2015.
• Barrio, R., Dena, A. and Tucker, W., A database of rigorous and high-precision periodic orbits of the Lorenz model, Computer Physics Communications, 194, 76-83, 2015.
• Joldes, M., Popescu, V. and Tucker, W., Searching for sinks of Hénon map using a multiple-precision GPU arithmetic library, SIGARCH Comput. Archit. News, 42(4), 63-68, 2014.
• Figueras, J.-L., Tucker, W., and Villadelprat, J., Computer-assisted techniques for the verification of the Chebyshev property of Abelian integrals, Journal of Differential Equations 254(8):3647-3663, 2013.
• Harlow, J., Sainudiin, R., and Tucker, W., Mapped Regular Pavings, Reliable Computing 16:252-282, 2012.
• Johnson, T. and Tucker, W., Rigorous parameter reconstruction for differential equations with noisy data, Automatica, Volume 44, pp. 2422-2426, 2008.
• Mitrea, I. and Tucker, W., Some Counterexamples for the Spectral Radius Conjecture, Differential and Integral Equations, Vol 16, No 12, pp. 1409--1439, 2003.