Publié le 12 novembre 2025 16h00:00. L’intelligence artificielle franchit une nouvelle étape en résolvant des problèmes mathématiques de niveau olympique, remettant en question la place de l’humain dans ce domaine autrefois considéré comme son apanage. Google DeepMind présente AlphaProof, un moteur de raisonnement capable de performances remarquables.
- AlphaProof, développé par Google DeepMind, a atteint un niveau de performance équivalent à une médaille d’argent aux Olympiades internationales de mathématiques (OMI) 2024.
- Contrairement aux grands modèles de langage (LLM), AlphaProof utilise une approche basée sur la « rigueur formelle », évitant ainsi les erreurs logiques et les « hallucinations ».
- Bien que prometteur, AlphaProof ne remplace pas les mathématiciens, mais constitue un outil puissant pour les assister dans leurs recherches.
Longtemps perçue comme un domaine exigeant créativité, raisonnement approfondi et logique implacable, les mathématiques étaient considérées comme l’une des dernières forteresses de l’intelligence humaine face aux machines. La perspective d’une IA capable de résoudre des problèmes mathématiques complexes, voire de faire des découvertes originales, relevait jusqu’à récemment de la science-fiction. Cette barrière est désormais en train de tomber.
Google DeepMind, la division de recherche en intelligence artificielle de Google, a une nouvelle fois fait sensation. L’équipe qui avait déjà impressionné le monde avec AlphaGo, vainqueur du champion du monde de go en 2016, et AlphaFold, capable de prédire la structure des protéines en quelques secondes (contre des années de recherche), vient de dévoiler AlphaProof.
Présenté dans la revue Nature, AlphaProof est un moteur de raisonnement révolutionnaire qui ne se contente pas de vérifier des théories mathématiques complexes, mais a démontré des capacités dignes d’une médaille d’argent aux Olympiades internationales de mathématiques (OMI) 2024. Un exploit sans précédent dans le domaine de l’IA.
Les OMI sont le concours de mathématiques préuniversitaires le plus prestigieux et le plus difficile au monde, réservé aux jeunes talents les plus brillants. Remporter une médaille à cette compétition est déjà un accomplissement majeur. Pour une IA, y parvenir en produisant des preuves vérifiables et correctes est, selon les auteurs de l’étude, un véritable « alunissage » dans le domaine de l’intelligence artificielle.
AlphaProof a résolu correctement trois des cinq problèmes non géométriques de l’OMI 2024, dont celui considéré comme le plus ardu de l’ensemble de la compétition. Si l’IA avait participé officiellement, elle aurait décroché une médaille d’argent. Jamais auparavant une intelligence artificielle n’avait atteint un tel niveau de performance.
Cependant, il convient de nuancer cet enthousiasme. Marta Macho-Stadler, du Département de mathématiques de l’Université du Pays basque, souligne que l’IA a nécessité une puissance de calcul considérable et plusieurs jours pour parvenir à ces résultats, alors qu’un participant humain aurait accompli la même tâche en un temps bien plus court. De plus, elle précise que, bien qu’AlphaProof excelle en algèbre et en théorie des nombres, il a rencontré des difficultés avec les problèmes combinatoires :
« Je comprends qu’il existe des problèmes mathématiques complexes qui nécessitent non seulement une « formation » (basée sur l’étude et les tests) pour être résolus, mais qui exigent également une grande dose de créativité. Et la créativité est une capacité intrinsèquement humaine. »
Marta Macho-Stadler, Département de mathématiques de l’Université du Pays basque
La clé du succès d’AlphaProof réside dans son architecture et, surtout, dans son adhésion à la « rigueur formelle ». Cette approche le distingue radicalement des grands modèles de langage (LLM) les plus connus. Si ces derniers ont montré un certain potentiel pour générer des textes ressemblant à des preuves mathématiques, ils opèrent sur un langage naturel (informel) et sont donc susceptibles de produire des « hallucinations » – des contenus plausibles mais logiquement incorrects, une erreur inacceptable en mathématiques.
Selon Carles Sierra, du Conseil supérieur de la recherche scientifique (CSIC), AlphaProof représente une avancée fondamentale car « il fournit des garanties formelles des preuves, il ne hallucine pas comme les LLM ». Son architecture garantit que chaque résultat est logiquement solide et vérifiable. Le système ne fonctionne pas sur le terrain glissant du langage naturel, mais dans un environnement logiciel formel appelé « Lean », un assistant de test interactif où une démonstration est exprimée dans un format que l’ordinateur peut vérifier automatiquement.
AlphaProof aborde la preuve mathématique comme un jeu de prise de décision, apprenant à trouver des preuves formelles grâce à l’apprentissage par renforcement (RL) et une formation massive. Pour les problèmes les plus complexes, il utilise une technique coûteuse en termes de calcul, le « Test-Time RL », qui lui permet de générer et d’apprendre à partir de millions de variantes du même problème, afin de s’adapter et de trouver la solution finale.
Ramón López de Mántaras, physicien et informaticien au CSIC et expert en intelligence artificielle, reconnaît qu’il s’agit d’un « excellent résultat » qui montre que les problèmes mathématiques formalisables par apprentissage par renforcement commencent à être accessibles à l’IA. Cependant, il tempère l’euphorie technologique :
« Les succès d’AlphaProof se sont produits principalement dans les mathématiques avancées du secondaire et du premier cycle, qui fonctionnent dans le cadre d’un ensemble de concepts connus et relativement fixes. »
Ramón López de Mántaras, CSIC
La véritable recherche mathématique avancée, qui implique la création de nouvelles théories et l’incorporation de nouveaux concepts, reste un défi majeur. L’extension des capacités d’AlphaProof à ce domaine semble encore lointaine.
AlphaProof est capable de démontrer et d’explorer dans un espace de solutions prédéfini, mais pas d’inventer. Il ne « comprend » pas les concepts mathématiques et ne peut pas créer de solutions à des problèmes complètement nouveaux. Il s’agit donc d’un outil précieux pour les mathématiciens, mais pas d’un substitut.
De plus, la puissance de calcul nécessaire pour atteindre ce niveau de performance soulève des questions sur la démocratisation de la science. La phase d’apprentissage d’AlphaProof nécessite une formation spécialisée et coûteuse, et la résolution des problèmes les plus difficiles peut prendre plusieurs jours d’inférence, ce qui est actuellement hors de portée de la plupart des chercheurs.
En conclusion, des systèmes comme AlphaProof, malgré leur nouveauté et leurs capacités, ne sont pas destinés à remplacer les mathématiciens, mais à les aider, tout comme un télescope aide les astronomes à faire de nouvelles découvertes. Google DeepMind a franchi une étape importante, mais la créativité humaine continuera, du moins pour l’instant, à guider la puissance logique des machines dans la recherche d’objectifs toujours plus ambitieux.