OpenAI a annoncé le 10 juillet que son modèle GPT-5.6 Sol Ultra avait généré une preuve complète de la Cycle Double Cover Conjecture, un problème de théorie des graphes non résolu depuis les années 1970. La preuve a été produite en moins d’une heure, par 64 sous-agents travaillant en parallèle. Elle a été vérifiée par machine.
Un problème posé dans les années 1970
La Cycle Double Cover Conjecture pose une question fondamentale sur les réseaux de noeuds et d’arêtes : existe-t-il toujours, pour tout graphe sans pont, une collection de cycles telle que chaque arête est traversée exactement deux fois ? Le problème avait été formulé indépendamment par plusieurs mathématiciens à partir des années 1970, notamment par Paul Seymour en 1979. Des solutions partielles pour des cas spéciaux existaient depuis, mais aucune preuve générale n’avait jamais été acceptée par la communauté.
OpenAI a publié le texte complet de la preuve en ligne. Thomas Bloom, mathématicien à l’Université de Manchester, qui a lu l’intégralité du document, la décrit comme « une très belle preuve » : courte, élémentaire, avec des outils mathématiques connus depuis les années 1980.
Pourquoi les humains ne l’avaient pas trouvée
Bloom identifie une raison précise. La preuve repose sur une petite torsion contre-intuitive dans le raisonnement. Un mathématicien humain essaie naturellement l’approche la plus directe. Quand elle échoue, il passe à autre chose. L’IA, elle, ne se décourage pas et continue d’explorer de petites variations autour de la même idée jusqu’à ce qu’une fonctionne.
« On peut imaginer essayer le marquage naturel en premier, vérifier l’algèbre linéaire, et quand cela échoue hausser les épaules en pensant ‘oh, je m’y attendais, je suppose que ce n’est pas si simple’ – alors que l’IA ne se décourage pas et continue d’essayer de petites variations », écrit Bloom sur X.
C’est ce que Bloom appelle « montrer ce que les humains auraient pu résoudre avec plus de patience ». Le problème n’était pas hors de portée humaine. Il demandait simplement une ténacité que les chercheurs n’ont pas le luxe de s’offrir sur une seule idée parmi des milliers.
La méthode : 64 agents en parallèle
GPT-5.6 Sol Ultra n’a pas travaillé seul. OpenAI précise que la preuve a été produite par 64 sous-agents opérant en parallèle. Chacun explore une direction ou vérifie un sous-problème. La coordination entre agents permettrait d’éviter que tous convergent vers la même impasse.
Cette architecture multi-agents représente une évolution notable par rapport à un seul modèle qui raisonne de manière séquentielle. Elle se rapproche de ce que font les équipes de mathématiciens humains : diviser les problèmes en parties travaillées simultanément, puis recombiner les résultats.
Des réserves subsistent
Bloom formule une critique nette : la preuve d’OpenAI ne cite aucun des travaux antérieurs dont elle s’inspire, notamment un article de 1983 de Bermond, Jackson et Jaeger sur lequel reposent les idées centrales. Pour Bloom, cela laisse croire que l’IA aurait inventé la stratégie de preuve de toutes pièces, ce qui est trompeur.
La vérification complète par la communauté mathématique est aussi encore en cours. Une vérification par machine confirme la validité formelle du raisonnement, mais le regard des experts humains reste nécessaire pour statuer définitivement sur l’importance et l’originalité réelle de l’approche.
GPT-5.6 Sol Ultra avait déjà montré des capacités remarquables en mathématiques depuis son lancement début juillet. Cet épisode est le premier où un modèle est crédité d’une preuve complète et vérifiée d’un problème ouvert de ce niveau.
