Décès de Gilles Dowek

By patricia, on July 21, 2025, at 09:03 PM

C'est avec une immense tristesse que nous avons appris le décès de notre collègue Gilles Dowek, survenu le 21 juillet 2025.

Directeur de recherche chez Inria, professeur attaché à l’ENS Paris-Saclay, fondateur de l’équipe Deducteam et membre du Laboratoire Méthodes Formelles, Gilles Dowek a contribué de manière exceptionnelle à l'essor scientifique de la discipline informatique.

Une contribution scientifique exceptionnelle

Le développement des systèmes de preuves (Coq, Isabelle/HOL, PVS... une vingtaine de systèmes en tout) est un immense progrès dans la quête d'une plus grande rigueur mathématique, mais il remet en cause l'universalité de la vérité mathématique : par le passé, nous avions des démonstrations du petit théorème de Fermat, maintenant, nous avons des démonstrations Coq du petit théorème de Fermat, des démonstrations Isabelle/HOL du petit théorème de Fermat, des démonstrations PVS, etc., chaque système définissant son propre langage de preuves et développant son propre corpus de démonstrations, basées sur différentes prémisses sous-jacentes à ces systèmes.

Gilles Dowek a été dans les tous premiers à proposer des cadres logiques « universels », c’est-à-dire capable d’exprimer toutes ces théories, la déduction modulo théorie et la logique œcuménique. Ceci l’a mené à définir le « Lambda-Pi-calcul modulo », qui va s’imposer en tant que langage de preuve universel robuste et pratique. En se basant sur ce langage, Gilles Dowek lance le projet Dedukti visant à rendre interopérables les principaux systèmes de preuves. Autour de ce projet se développe un écosystème d’outils permettant:

  • la traduction des corpus de preuves d’un système à l’autre
  • l’analyse des prémisses sous-jacentes aux différents systèmes de preuves, et dans certains cas l'élimination de celles-ci, pour parvenir à des preuves plus universelles
  • la re-vérification des démonstrations, augmentant la confiance que nous pouvons avoir dans la correction de ces démonstrations — ce qui constitue un problème pratique non négligeable pour les autorités de certifications.

Une largeur de vue scientifique

Gilles Dowek a également contribué à la théorie du calcul des constructions et des types dépendants et au domaine de la démonstration automatique. Mais son spectre scientifique s’étend bien au-delà du domaine de la logique.

Gilles a par exemple initié et développé la théorie des langages de programmation quantiques, de même qu’un ensemble de résultats mettant à jour des liens entre postulats de physique et calculabilité, comme par exemple une preuve de la thèse de Church-Turing sous hypothèses physiques quantiques. Une rubrique récente dans la revue New Scientist expose ses dernières découvertes sur la nature du temps.

Pour ses contributions exceptionnelles au champ des sciences informatiques et mathématiques, Gilles a obtenu le Grand Prix Inria de l’Académie des Sciences en 2023.

Des livres qui mettent les Sciences au cœur de la vie de la cité

Gilles Dowek a publié ou co-publié de nombreux livres, certains traduits en allemand, anglais, chinois, coréen, espagnol, grec, roumain, italien. Citons :

En outre, Gilles a publié une chronique mensuelle de 2014 à 2021 dans Pour La Science centrée sur les transformations apportées par le numérique: « Homo informaticus ». Son implication pour la divulgation scientifique (par ex. en tant que membre du conseil scientifique de La main à la pâte de 2012 à 2022) a été récompensée par le Grand Prix d’Alembert des Lycéens de la Société Mathématique de France en 2000.

Pour son exploration de nouvelles questions philosophiques posées par le développement de l'informatique, Gilles a reçu la médaille d’Histoire des sciences et d’épistémologie de l’Académie des Sciences en 2024.

La voix de l’informatique

Finalement, Gilles Dowek fait partie du petit nombre de personnes qui ont porté la voix de la discipline informatique en France, et auprès de l’éducation nationale notamment. Avec entre autres Gérard Berry, Professeur au Collège de France, il a fait passer l’idée que l’informatique était une matière comme une autre, et qu’au même titre que la biologie et la physique, elle devait être enseignée au lycée. Ces efforts ont abouti en 2012 avec la création de la spécialité ISN de Terminale S ; Gilles a d’ailleurs été l’un des principaux rédacteurs du programme de cet enseignement et du manuel scolaire de référence.

Avec Gilles, beaucoup perdent un ami cher ; nous perdons un collègue brillant et un esprit fin. Toutes nos chaleureuses pensées vont à ses proches.

Articles rendant hommage à son parcours et à ses engagements

Crédit photo : © Inria / Photo B. Fourrier

Tags: Deces, Obituaries