Une recherche informatique et mathématique collective : le calcul du cinquième « castor affairé »

Jean-Paul Delahaye

Le calcul du « cinquième castor affairé », est un exploit extraordinaire réalisé il y a quelques mois dans le cadre d'un travail de recherche collectif exemplaire. Il concerne les machines de Turing, ce concept abstrait de dispositif de calcul imaginé en 1936 par Alan Turing et qui aujourd'hui encore est un outil important pour parler de la complexité des algorithmes et de la « non-calculabilité ». Le record dont nous allons rendre compte comporte deux étapes principales. D’abord, il a fallu mener une recherche systématique, longue mais assez facile, consistant à exécuter une multitude de petits calculs pouvant être mené indépendamment et en parallèle les uns des autres, et dont il faut mémoriser certains résultats pour aboutir à une proposition plausible. Dans un second temps, bien plus délicat, il a fallu opérer un travail minutieux de démonstration du résultat suggéré. Les logiciels de validation de démonstrations, appelés « assistants de preuve », se sont révélés essentiels dans cette seconde étape, et on sait qu'ils le sont aujourd'hui aussi pour contrôler les travaux des systèmes d'intelligence artificielle. Remarquable aussi est le fait que cet exploit est le fruit d’un travail collaboratif entremêlant mathématiques et informatique, qui témoigne d’une nouvelle façon de pratiquer des recherches et où l'ordinateur est un acteur central.