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 :
- Peut-on croire les sondages ? (2002);
- Les métamorphoses du calcul (2007), Grand Prix de Philosophie de l'Académie française, qui porte sur la notion de calcul et ses liens avec la Physique ;
- La logique (2015);
- Le temps des algorithmes (2017), Prix La Science Se Livre 2018 ;
- Ce dont on ne peut parler, il faut l'écrire (2019), qui porte sur la notion de langage ;
- Qui a hacké Garoutzia ?, pièce de théâtre qui porte sur l’Intelligence Artificielle, présentée au Festival Off d’Avignon en juillet 2023 et jouée à La Scène Parisienne du septembre au décembre 2024, mise en scène par Lisa Bretzner.
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
- Hommage à Gilles Dowek (CNRS, 24 juillet 2025)
- L'ENS Paris-Saclay rend hommage à Gilles Dowek (ENS Paris-Saclay, 22 juillet 2025)
- Disparition de Gilles Dowek, figure majeure de l’informatique et de la pensée scientifique (Inria, 22 juillet 2025)
- Disparition de Gilles Dowek : hommage à une pensée libre, rigoureuse et engagée (Ministère chargé de l'Enseignement Supérieur et de la Recherche, 22 juillet 2025)
- Gilles Dowek, informaticien engagé et vulgarisateur, est mort (Le Monde, 21 juillet 2025)
- Gilles Dowek: Au carrefour de l'informatique, de la logique et de la philosophie (Université Paris-Saclay, décembre 2024)
- Gilles Dowek, explorateur des méthodes formelles (Inria, novembre 2023)
- Gilles Dowek, parcours inspirant (ENS Paris-Saclay)
- Gilles Dowek, un maître en logique porté par le hasard (Le Monde, avril 2017)
Crédit photo : © Inria / Photo B. Fourrier