Une équipe de l’Université de Pékin a développé un système d’intelligence artificielle capable de résoudre la conjecture d’Anderson, un problème d’algèbre commutative formulé en 2014 et resté sans solution depuis. Le cadre d’IA à double agent a synthétisé des décennies de littérature mathématique pour établir une preuve formelle en 80 heures de calcul, marquant une étape significative dans l’automatisation de la recherche mathématique.
La conjecture d’Anderson, énoncée en 2014 par le professeur Dan Anderson de l’Université de l’Iowa et demeurée sans réponse depuis, vient de trouver sa solution grâce à un système d’intelligence artificielle développé par des chercheurs chinois. L’avancée technique ouvre ici de nouvelles perspectives sur l’automatisation de la recherche fondamentale en mathématiques.
Un cadre d’IA à double agent
Sous la direction du mathématicien Dong Bin, l’équipe de l’Université de Pékin a conçu une architecture informatique originale baptisée « cadre d’IA à double agent ». Ce système synthétise des décennies de littérature mathématique pour combler l’écart entre le raisonnement en langage naturel et la vérification formelle par machine. « Grâce à ce cadre, nous avons réussi à résoudre un problème ouvert en algèbre commutative et à formaliser automatiquement la preuve sans pratiquement aucune intervention humaine », expliquent les chercheurs dans leur article.
Le mécanisme repose sur un module de raisonnement nommé Rethlas, qui s’appuie sur un moteur de recherche de théorèmes mathématiques connu sous le nom de Matlas. La combinaison permet d’explorer des stratégies de résolution de problèmes selon un processus similaire à celui qu’emploient les mathématiciens humains, mais avec une capacité de traitement et d’analyse considérablement accrue.
80 heures de calcul pour une démonstration complète
Le système a complété la démonstration en 80 heures de calcul, accomplissant des tâches qui nécessiteraient normalement la collaboration d’experts issus de différents domaines des mathématiques. « Aucun jugement mathématique n’a été requis de la part de l’opérateur humain », note l’équipe, tout en reconnaissant que l’implication d’un mathématicien pourrait accélérer le processus.
La performance technique soulève toutefois des questions fondamentales sur l’évolution des pratiques de recherche. L’article, qui n’a pas encore été soumis à l’évaluation par les pairs, présente ce résultat comme une illustration tangible des progrès réalisés dans l’automatisation de la recherche mathématique grâce à l’intelligence artificielle.
Une vague d’avancées en mathématiques assistées par IA
La percée de l’Université de Pékin s’inscrit dans une tendance plus large où les systèmes d’intelligence artificielle s’attaquent à des problèmes mathématiques de longue date. Plus tôt cette année, le GPT-5.4 d’OpenAI a résolu un problème du benchmark FrontierMath qui avait résisté aux chercheurs depuis 2019. Parallèlement, une startup spécialisée en intelligence artificielle nommée Axiom a annoncé avoir résolu quatre problèmes jusqu’alors insolubles en février.
Ce rythme de progression suscite des réactions contrastées au sein de la communauté mathématique. D’un côté, l’enthousiasme domine face à la possibilité de résoudre des conjectures qui résistaient depuis des années, voire des décennies. De l’autre, une certaine inquiétude émerge quant à l’évolution du rôle des mathématiciens dans un domaine où l’intelligence artificielle occupe une place de plus en plus centrale.
Les implications de ces développements techniques dépassent le cadre strict des mathématiques pures. Elles interrogent la nature même de la découverte scientifique et la place de l’intuition humaine dans un processus de recherche de plus en plus automatisé. Si l’intelligence artificielle démontre sa capacité à résoudre des problèmes complexes, elle soulève également des questions sur la créativité mathématique et la manière dont les nouvelles idées émergent dans ce domaine.
La résolution de la conjecture d’Anderson par un système d’intelligence artificielle marque ainsi un tournant dans l’histoire des mathématiques. Elle montre comment les outils computationnels peuvent non seulement assister les chercheurs, mais aussi mener de manière autonome des démonstrations complètes.
