Logipedia : vers un Wikipédia des démonstrations formelles

Les démonstrations formelles, c’est-à-dire informatisées, sont devenues un outil central en informatique (sûreté, sécurité…) et en mathématiques. Cependant, chaque système – Coq, HOL Light, Isabelle/HOL, PVS… – implémente son langage et sa théorie, limitant les possibilités d’interopérabilité entre systèmes et la durabilité de ces démonstrations. Logipedia est une encyclopédie, en construction, de démonstrations formelles exprimées dans diverses théories. Nous présenterons cette encyclopédie et discuterons de la question scientifique qui se cache derrière ce développement : qu’est-ce qu’une théorie ?

√ Bio :

Gilles Dowek est aujourd’hui directeur de recherche Inria. Au sein de l’équipe-projet Deducteam (Inria Saclay -Île-de-France), il a mené ses recherches sur les rapports entre les langages de programmation et le langage mathématique, sur les systèmes informatisés de traitement de démonstrations mathématiques et sur la sureté des logiciels.

Précédemment, il a été chercheur à l’institut de 1993 à 2002, puis professeur à l’École polytechnique de 2003 à 2010. Il a également exercé aux Etats-Unis, à l’Université Carnegie Mellon à Pittsburgh, dans les laboratoires de la société Computational Logic à Austin et au sein du NIA (National Institute for Aerospace, NASA) à Hampton.

Gilles Dowek est particulièrement engagé dans la médiation scientifique auprès du grand public. Il est l’auteur de plusieurs ouvrages de vulgarisation sur les sciences mathématiques. En 2000, la Société mathématique de France lui a remis le Grand prix d’Alembert des Lycéens pour son action de diffusion des mathématiques auprès des jeunes. Il a reçu le Grand Prix de Philosophie 2007 de l’Académie française pour « Les métamorphoses du calcul, une étonnante histoire de mathématiques » (éditions du Pommier).