Séminaire - Tristan Stérin : Le cinquième nombre Busy Beaver
Description
Thimothy Gowers
Chaire Combinatoire
Collège de France
Année 2025-2026
La philosophie de la pratique des mathématiques
Séminaire - Tristan Stérin : Le cinquième nombre Busy Beaver
Résumé
Nous calculons la cinquième valeur d'une fonction… non calculable. Cette fonction, appelée Busy Beaver et proposée par Tibor Radó en 1962, mesure le nombre maximal d'opérations qu'un programme peut effectuer avant de s'arrêter, en fonction de sa taille. Pour la première fois depuis plus de quarante ans, une nouvelle valeur, BusyBeaver(5) = 47 176 870, a été déterminée.
C'est un ordinateur qui a vérifié formellement les 181 385 789 cas particuliers à l'aide de l'assistant de preuve Coq, dans le cadre d'un effort de recherche massivement collaboratif ayant mobilisé une centaine de personnes sur Internet pendant deux ans (bbchallenge.org).
Tristan Stérin
PRGM DEV
United States
