Un nouveau pont relie l’étrange mathématique de l’infini à l’informatique

• Il a été mis en évidence que la théorie descriptive des ensembles, un domaine technique qui étudie la structure des ensembles infinis, peut être réinterprétée dans le langage des algorithmes
• Le mathématicien Anton Bernshteyn a démontré que des problèmes de graphes infinis peuvent être reformulés en problèmes de communication dans des réseaux informatiques
• Ce lien montre une correspondance entre la mesurabilité (measurability) et l’efficacité des algorithmes distribués
• Les chercheurs utilisent ce pont pour convertir dans les deux sens théorèmes et problèmes des deux domaines et en tirer de nouveaux résultats
• Une découverte qui redéfinit la frontière entre infini et calcul et élargit les possibilités de collaboration entre mathématiques et informatique

---

Introduction : la théorie des ensembles et le monde de l’infini

• Les fondements des mathématiques modernes reposent sur la théorie des ensembles, et la plupart des mathématiciens abordent leurs problèmes en la tenant pour acquise
• Mais les théoriciens descriptifs des ensembles (descriptive set theorists) forment un petit groupe de chercheurs qui continue d’explorer la nature des ensembles infinis
• En 2023, Anton Bernshteyn a découvert un lien profond entre la théorie descriptive des ensembles et l’informatique
  • Il a montré qu’il est possible de transformer certains problèmes sur des ensembles infinis en problèmes de communication dans des réseaux informatiques
• Ce résultat est considéré comme un pont entre des langages opposés : la logique et les algorithmes, l’infini et le fini

Contexte de la théorie descriptive des ensembles

• L’origine de la théorie des ensembles remonte aux travaux de Georg Cantor, qui ont démontré l’existence de différentes tailles d’infini
• Parmi les concepts qui décrivent la taille d’un ensemble figurent la cardinalité (cardinality) et la mesure (measure)
  • Exemple : l’ensemble des réels de l’intervalle 0~1 et celui de l’intervalle 0~10 ont la même cardinalité, mais leur mesure vaut respectivement 1 et 10
• La théorie descriptive des ensembles distingue les ensembles mesurables et non mesurables, puis les classe selon une hiérarchie de complexité (hierarchy)
• Cette hiérarchie sert de critère pour choisir les bons outils dans d’autres domaines des mathématiques (par ex. théorie des probabilités, systèmes dynamiques, théorie des groupes)

Graphes infinis et problème de coloration

• Bernshteyn étudiait les graphes infinis, en modélisant les nœuds et les arêtes de chaque graphe comme une structure connectée à l’infini
• Exemple : si l’on relie des points sur un cercle à intervalles réguliers, un intervalle rationnel produit une boucle fermée, tandis qu’un intervalle irrationnel engendre une structure connectée infinie
• Si l’on veut colorer les nœuds d’un graphe avec deux couleurs, c’est possible en utilisant l’axiome du choix (axiom of choice), mais on obtient alors un ensemble non mesurable
• En revanche, avec une méthode de coloration continue, trois couleurs sont nécessaires, mais on obtient un ensemble mesurable
• Cette différence joue un rôle clé pour déterminer la position dans la hiérarchie de complexité de la théorie des ensembles

Rencontre avec les algorithmes distribués

• En 2019, Bernshteyn a assisté à un exposé d’informatique sur les algorithmes distribués (distributed algorithms) et y a repéré une forte similarité
  • Exemple : le problème où des routeurs Wi‑Fi doivent choisir des fréquences (couleurs) différentes pour éviter les interférences
• Chaque nœud choisit sa couleur via un algorithme local (local algorithm), en ne communiquant qu’avec ses nœuds voisins
• Avec seulement deux couleurs, la solution est inefficace, mais en autorisant trois couleurs, on peut résoudre le problème efficacement
• Bernshteyn a compris que ce seuil (threshold) du nombre de couleurs était identique au seuil du problème de coloration mesurable en théorie descriptive des ensembles

Preuve de l’équivalence entre deux mondes

• Bernshteyn a démontré mathématiquement l’équivalence entre algorithme local efficace ↔ méthode de coloration mesurable
• Dans les graphes finis, on peut attribuer un numéro unique à chaque nœud, mais c’est impossible dans les graphes infinis non dénombrables
• Il a conçu une méthode d’étiquetage sans doublons entre nœuds adjacents, permettant d’étendre les algorithmes aux graphes infinis
• Il en résulte qu’« tout algorithme local correspond à une méthode de coloration mesurable en théorie descriptive des ensembles »
• Cela révèle un lien mathématique profond entre calculabilité et définissabilité (definability)

Extension des recherches et applications

• Václav Rozhoň et d’autres ont utilisé ce lien pour résoudre un problème de coloration de graphes en arbre (tree) et en tirer des outils pour l’étude des systèmes dynamiques
• À l’inverse, des travaux exploitent aussi les méthodes de la théorie des ensembles pour améliorer l’estimation de la difficulté des problèmes
• Ce pont va au-delà d’un simple outil de résolution : il contribue à refonder le système de classification de la théorie des ensembles
• Les théoriciens descriptifs des ensembles peuvent désormais s’appuyer sur les méthodes de classification systématique de l’informatique pour organiser des problèmes encore non classés
• Bernshteyn espère que ces recherches aideront à faire reconnaître le concept d’infini comme une composante concrète des mathématiques pratiques

[GN⁺]

Avis Hacker News

• Je me demande si ce genre de résultat pourrait être appliqué à des domaines concrets comme le calcul distribué, ou si cela n’existe que par pur intérêt mathématique

  • Ce n’est pas du tout une question idiote. Ce type de perspicacité technique pourrait mener à de nouveaux théorèmes d’impossibilité en algorithmique distribuée ou en théorie de la complexité computationnelle. Des applications comme le mesh networking seraient aussi intéressantes

• Dire que « toute la mathématique moderne est construite sur la théorie des ensembles » est trop catégorique. Des outils mathématiques modernes comme Lean ou Rocq se développent autour des mathématiques formalisées (formalized mathematics), qui reposent sur la théorie des types (type theory)

  • Je ne suis pas mathématicien, mais je pense que ZFC reste un système fondamental valable. Les types dépendants (dependent types) sont utiles pour la gestion des preuves, mais ils ne permettent pas de démontrer davantage de théorèmes. L’Isabelle/HOL de Lawrence Paulson n’est pas fondé sur les types, mais peut prouver la majeure partie des mathématiques
  • Mais les mathématiciens, en pratique, utilisent très peu les mathématiques formalisées. Même quand ils les connaissent, ils ne les emploient pas comme langage de base à cause de leur caractère peu pratique
  • Il ne faut pas confondre le langage des mathématiques et le langage formel dans lequel on prouve des choses à propos de ce langage. Le premier utilise presque entièrement les ensembles, le second recourt nécessairement aux types
  • Plus précisément, il serait plus juste de dire que la crise des fondements des mathématiques a été provisoirement réglée par la formalisation de la théorie des ensembles

• La formule humoristique « cons’es all the way down » est une satire des structures récursives

• Je suis ému par l’idée qu’on puisse enfin « calculer l’infini »

  • Le mois prochain, la tournée Calculating Infinity de The Dillinger Escape Plan passe dans la Bay Area. Lien vers le concert. Je partage ça parce qu’il y a probablement un chevauchement entre les fans de maths, de hacking et de mathcore
  • En réponse à « calculer l’infini », quelqu’un enchaîne la blague avec « Et au-delà ! »
  • En Haskell, on peut représenter une infinité dénombrable (countable infinity) avec une seule ligne : let x = x in x
  • Quelqu’un ajoute l’humour du mème : « Chuck Norris a compté de 1 à l’infini, deux fois »
  • Un autre ajoute une remarque sarcastique : « Ça a vraiment pris longtemps /s »

• Je ne suis pas d’accord avec l’idée que « l’informatique ne traite que du fini ». En réalité, l’informatique est profondément concernée par l’infini

  • C’est assez typique de la façon dont Quanta traite ce genre de sujets. Le récit adopte une vulgarisation scientifique centrée sur les personnes et tend à omettre les détails
  • Cela dit, l’informatique s’intéresse moins à l’infini non dénombrable (uncountable infinity). La théorie de la mesure (measure theory) s’occupe surtout de cela
  • Moi aussi, au départ, je pensais que « l’informatique approxime l’infini », mais en fait le mot-clé est bien approximation. Nous travaillons toujours à l’intérieur de bornes finies. Même si l’univers était infini, ce que nous pouvons observer reste limité par la vitesse de la lumière
  • Des phrases du type « l’informatique n’utilise pas la logique » sont d’une paresse affligeante. La logique booléenne en est la preuve directe

• J’ai étudié les mathématiques pendant longtemps, et j’en suis venu à croire que l’infini (infinity) n’existe pas. Les mathématiques seraient peut-être meilleures sans lui

  • Je n’ai étudié que les maths au niveau ingénieur, mais pour moi l’infini n’est pas un nombre, c’est un processus (process). Le « ... » de {1, 2, 3, ...} désigne un processus d’extension sans fin. Il n’existe pas de nième nombre premier infini ; il n’y a qu’une règle de génération selon laquelle il existe toujours un nombre premier plus grand
  • Mais si on supprime l’infini, les mathématiques deviennent atrocement compliquées. Si l’on n’étend pas les entiers naturels indéfiniment, les calculs deviennent très peu pratiques
  • Les mathématiques s’intéressent moins à l’existence qu’à l’utilité conceptuelle. Les cercles n’existent pas non plus dans le monde réel, mais ils sont utiles. Sans l’infini, on finirait par le réinventer sous la forme de « la limite quand x tend vers un nombre très, très grand »
  • Quelqu’un tourne en dérision l’inutilité supposée de l’infini avec la blague : « Il suffit de s’arrêter à 8 »
  • L’infini n’est qu’un nom pour désigner un processus sans fin. Certains processus croissent plus vite que d’autres, donc il existe des infinis plus grands. Personnellement, j’aime bien la conception de l’infini dans le modèle de la sphère de Riemann

• Blague disant que node_modules a relié les mathématiques de l’infini à mon système de fichiers, pour se moquer de l’explosion des dépendances

• En réponse à la phrase « toute la mathématique moderne est construite sur la théorie des ensembles », quelqu’un objecte qu’il existe aussi la théorie des types (Type Theory)

  • La Type Theory est un système axiomatique plus puissant que ZFC. Voir cette explication dans une réponse MathOverflow
  • Mais il n’existe pas encore d’ensemble d’axiomes en théorie des types aussi influent que ZF ou ZFC
  • Techniquement, la théorie descriptive des ensembles (descriptive set theory) est distincte de la théorie des ensembles fondationnelle. On peut facilement la reconstruire à l’aide des notions de types et d’espaces, et cela est souvent plus avantageux. Réinterpréter l’infini mathématique sous un angle computationnel n’est pas une tentative nouvelle
  • Décrire la théorie des ensembles comme « la discipline qui organise des collections d’objets abstraits » est une présentation trop simpliste. Il reste néanmoins vrai que la plupart des mathématiques sont encore définies à partir des axiomes des ensembles