Je suis fasciné par l'énergie qui a été investie dans ce problème, la passion qu'il a déchaînée, et le fait que la résolution fasse la une de Quanta Magazine et le tour des réseaux sociaux (en tous cas tous mes contacts habituels sur Mastodon et Bluesky).
Pourquoi ? Parce que les valeurs exactes de la fonction castor affairé me paraissent parfaitement inintéressantes :D Notamment parce qu'elles dépendent fortement de choix purement techniques sur la forme des machines de Turing, qui n'ont généralement aucune importance parce toutes les variantes des machines de Turing sont interconvertibles, mais qui influencent le nombre exact d'états et donc la fonction castor affairé : le nombre de symboles de l'alphabet (un alphabet binaire est le plus courant, mais on permet généralement des alphabets plus gros, et on s'en sert même parfois vraiment, cf. space speedup theorem en complexité), le nombre de bandes (une seule dans la variante la plus simple, mais parfois deux avec une bande d'entrée/sortie et une bande de travail, et en complexité toujours trois, entrée + travail + sortie, car c'est ce qui permet de mesurer l'espace pris par un algorithme sans compter l'entrée ni la sortie), et aussi la manière de gérer les blancs (est-ce que la machine a le droit de se déplacer à l'intérieur des blancs après l'entrée en les laissant écrits ?), etc., etc.
Cela dit, c'est vrai que formaliser ça en Coq est assez impressionnant.
# L'œil amusé d'un théoricien
Posté par jeanas (site web personnel, Mastodon) . En réponse au lien Des mathématiciens amateurs établissent une preuve du cinquième castor affairé. Évalué à 5.
Je suis fasciné par l'énergie qui a été investie dans ce problème, la passion qu'il a déchaînée, et le fait que la résolution fasse la une de Quanta Magazine et le tour des réseaux sociaux (en tous cas tous mes contacts habituels sur Mastodon et Bluesky).
Pourquoi ? Parce que les valeurs exactes de la fonction castor affairé me paraissent parfaitement inintéressantes :D Notamment parce qu'elles dépendent fortement de choix purement techniques sur la forme des machines de Turing, qui n'ont généralement aucune importance parce toutes les variantes des machines de Turing sont interconvertibles, mais qui influencent le nombre exact d'états et donc la fonction castor affairé : le nombre de symboles de l'alphabet (un alphabet binaire est le plus courant, mais on permet généralement des alphabets plus gros, et on s'en sert même parfois vraiment, cf. space speedup theorem en complexité), le nombre de bandes (une seule dans la variante la plus simple, mais parfois deux avec une bande d'entrée/sortie et une bande de travail, et en complexité toujours trois, entrée + travail + sortie, car c'est ce qui permet de mesurer l'espace pris par un algorithme sans compter l'entrée ni la sortie), et aussi la manière de gérer les blancs (est-ce que la machine a le droit de se déplacer à l'intérieur des blancs après l'entrée en les laissant écrits ?), etc., etc.
Cela dit, c'est vrai que formaliser ça en Coq est assez impressionnant.