Dans un sens, l’ordinateur et la conjecture de Collatz sont parfaitement compatibles. D’une part, comme le note Jeremy Avigad, logicien et professeur de philosophie à Carnegie Mellon, la notion d’algorithme itératif est à la base de l’informatique – et les séquences de Collatz sont un exemple d’algorithme itératif, procédant étape par étape selon à une règle déterministe. De même, montrer qu’un processus se termine est un problème courant en informatique. « Les informaticiens veulent généralement savoir que leurs algorithmes se terminent, c’est-à-dire qu’ils renvoient toujours une réponse », explique Avigad. Heule et ses collaborateurs tirent parti de cette technologie pour s’attaquer à la conjecture de Collatz, qui n’est en réalité qu’un problème de terminaison.
« La beauté de cette méthode automatisée est que vous pouvez allumer l’ordinateur et attendre. »
Jeffrey Lagarias
L’expertise de Heule réside dans un outil de calcul appelé « solveur SAT » ou un résolveur de « satisfiabilité », un programme informatique qui détermine s’il existe une solution pour une formule ou un problème étant donné un ensemble de contraintes. Bien qu’essentiellement, dans le cas d’un défi mathématique, un solveur SAT a d’abord besoin que le problème soit traduit, ou représenté, en des termes que l’ordinateur comprend. Et comme le dit Yolcu, doctorant chez Heule : « La représentation compte beaucoup.
Un long shot, mais ça vaut le coup d’essayer
Lorsque Heule a mentionné pour la première fois s’attaquer à Collatz avec un solveur SAT, Aaronson a pensé: « Il n’y a aucun moyen que cela fonctionne. » Mais il était facilement convaincu que cela valait la peine d’essayer, car Heule a vu des moyens subtils de transformer ce vieux problème qui pourrait le rendre malléable. Il avait remarqué qu’une communauté d’informaticiens utilisait des solveurs SAT pour trouver avec succès des preuves de terminaison pour une représentation abstraite du calcul appelée « système de réécriture ». C’était long, mais il a suggéré à Aaronson que transformer la conjecture de Collatz en un système de réécriture pourrait permettre d’obtenir une preuve de terminaison pour Collatz (Aaronson avait déjà aidé à transformer l’hypothèse de Riemann en un système de calcul, en l’encodant dans un petit machine). Ce soir-là, Aaronson a conçu le système. « C’était comme un devoir, un exercice amusant », dit-il.
« Dans un sens très littéral, je luttais contre un Terminator – au moins un prouveur de théorème de terminaison. »
Scott Aaronson
Le système d’Aaronson a capturé le problème de Collatz avec 11 règles. Si les chercheurs pouvaient obtenir une preuve de terminaison pour ce système analogue, en appliquant ces 11 règles dans n’importe quel ordre, cela prouverait que la conjecture de Collatz est vraie.
Heule a essayé avec des outils de pointe pour prouver l’arrêt des systèmes de réécriture, ce qui n’a pas fonctionné – c’était décevant, voire surprenant. « Ces outils sont optimisés pour les problèmes qui peuvent être résolus en une minute, alors que toute approche pour résoudre Collatz nécessite probablement des jours, voire des années de calcul », explique Heule. Cela les a motivés à affiner leur approche et à mettre en œuvre leurs propres outils pour transformer le problème de réécriture en un problème SAT.
MARIJN HEULE
Aaronson a pensé qu’il serait beaucoup plus facile de résoudre le système moins l’une des 11 règles – en laissant un système « de type Collatz », un test décisif pour l’objectif plus large. Il a lancé un défi humain contre ordinateur : le premier à résoudre tous les sous-systèmes avec 10 règles gagne. Aaronson a essayé à la main. Heule a essayé par le solveur SAT : il a codé le système en tant que problème de satisfiabilité – avec encore une autre couche de représentation intelligente, traduisant le système dans le jargon des variables de l’ordinateur qui peuvent être des 0 et des 1, puis a laissé son solveur SAT fonctionner sur les cœurs , à la recherche d’une preuve de résiliation.
MARIJN HEULE
Ils ont tous deux réussi à prouver que le système se termine avec les différents ensembles de 10 règles. Parfois, c’était une entreprise triviale, à la fois pour l’humain et pour le programme. L’approche automatisée de Heule a pris au plus 24 heures. L’approche d’Aaronson a nécessité un effort intellectuel important, prenant quelques heures ou même une journée – un ensemble de 10 règles qu’il n’a jamais réussi à prouver, bien qu’il pense fermement qu’il aurait pu le faire, avec plus d’efforts. « Dans un sens très littéral, je luttais contre un Terminator », dit Aaronson – « au moins un prouveur de théorème de terminaison. »
Yolcu a depuis affiné le solveur SAT, en calibrant l’outil pour mieux s’adapter à la nature du problème Collatz. Ces astuces ont fait toute la différence, en accélérant les preuves de terminaison pour les sous-systèmes à 10 règles et en réduisant les temps d’exécution à quelques secondes seulement.
« La principale question qui demeure », déclare Aaronson, « est : qu’en est-il de l’ensemble complet de 11 ? Vous essayez d’exécuter le système sur l’ensemble complet et il fonctionne pour toujours, ce qui ne devrait peut-être pas nous choquer, car c’est le problème de Collatz.
Selon Heule, la plupart des recherches sur le raisonnement automatisé ferment les yeux sur les problèmes qui nécessitent beaucoup de calculs. Mais sur la base de ses percées précédentes, il pense que ces problèmes peuvent être résolus. D’autres ont Collatz transformé comme un système de réécriture, mais c’est la stratégie consistant à utiliser un solveur SAT affiné à grande échelle avec une puissance de calcul formidable qui pourrait gagner du terrain vers une preuve.
Jusqu’à présent, Heule a mené l’enquête Collatz en utilisant environ 5 000 cœurs (les unités de traitement alimentant les ordinateurs ; les ordinateurs grand public ont quatre ou huit cœurs). En tant qu’Amazon Scholar, il a reçu une invitation ouverte d’Amazon Web Services pour accéder à des ressources « pratiquement illimitées », jusqu’à un million de cœurs. Mais il hésite à en utiliser beaucoup plus.
« Je veux une indication qu’il s’agit d’une tentative réaliste », dit-il. Sinon, Heule pense qu’il gaspillerait des ressources et de la confiance. « Je n’ai pas besoin de confiance à 100%, mais j’aimerais vraiment avoir des preuves qu’il y a une chance raisonnable que cela réussisse. »
Suralimenter une transformation
« La beauté de cette méthode automatisée est que vous pouvez allumer l’ordinateur et attendre », explique le mathématicien Jeffrey Lagarias, de l’Université du Michigan. Il a joué avec Collatz pendant une cinquantaine d’années et est devenu le gardien du savoir, en compilant des bibliographies annotées et en éditant un livre sur le sujet, « Le défi ultime.« Pour Lagarias, l’approche automatisée a fait penser à un 2013 papier par le mathématicien de Princeton John Horton Conway, qui a pensé que le problème de Collatz pourrait faire partie d’une classe insaisissable de problèmes qui sont vrais et « indécidables », mais à la fois pas prouvable indécidable. Comme Conway l’a noté : « … il se peut même que l’affirmation selon laquelle ils ne sont pas prouvables ne soit pas elle-même prouvable, et ainsi de suite.
« Si Conway a raison », dit Lagarias, « il n’y aura aucune preuve, automatisée ou non, et nous ne connaîtrons jamais la réponse. »
