En juillet 2024, Google DeepMind avait annoncé un exploit historique : son système d’intelligence artificielle, AlphaProof, avait obtenu une médaille d’argent à l’Olympiade internationale de mathématiques (IMO), devenant ainsi le premier modèle d’IA à atteindre un niveau de performance équivalent à celui des meilleurs mathématiciens adolescents du monde. Cette promesse de transparence a été tenue le 12 novembre, avec la publication d’un article complet dans la revue Nature, révélant en détail les mécanismes techniques derrière cette avancée majeure. L’IMO, qui réunit chaque année les plus brillants jeunes mathématiciens du globe, propose six problèmes extrêmement complexes, couvrant l’algèbre, la combinatoire, la théorie des nombres et la géométrie. En 2024, sur un total de 42 points, moins de 1 % des participants ont obtenu la note maximale. Le fait qu’AlphaProof, combiné à AlphaGeometry 2, ait résolu quatre des six épreuves pour atteindre 28 points – un score équivalent à une médaille d’argent – constitue une étape décisive dans l’évaluation des capacités de raisonnement mathématique des machines. En particulier, il a réussi à démontrer le problème n°6, considéré comme le plus difficile de l’édition, que seulement cinq participants humains ont résolu intégralement. Le succès d’AlphaProof repose sur une combinaison innovante de langage formel et d’apprentissage par renforcement. Contrairement aux grands modèles linguistiques classiques, qui peuvent générer des raisonnements plausibles mais erronés (des « hallucinations »), AlphaProof utilise Lean, un assistant de preuve interactif qui valide automatiquement chaque étape logique. Cette rigueur absolue élimine les erreurs et garantit la correction des preuves – une condition indispensable en mathématiques. Le principal défi était la rareté des données d’entraînement dans Lean. Pour y remédier, les chercheurs ont d’abord entraîné une version modifiée de Gemini pour convertir automatiquement les énoncés mathématiques en langage formel. Ce processus, appelé « formalisation automatique », a permis de générer huit millions de nouvelles déclarations formelles à partir d’un million de problèmes naturels. Ce vaste jeu de données a servi de base à l’entraînement d’un modèle transformer de 3 milliards de paramètres, inspiré de l’architecture d’AlphaZero. Ce modèle comprend deux composants clés : un réseau de stratégie, qui suggère la prochaine étape logique à suivre, et une fonction de valeur, qui évalue la pertinence d’un chemin de preuve. Ces deux éléments guident un algorithme de recherche arborescente optimisé, qui explore l’immense espace des preuves possibles. Une innovation majeure est l’introduction des « nœuds-produits », qui exigent que tous les sous-objectifs d’une preuve (comme les cas de récurrence) soient prouvés, permettant une meilleure gestion des ressources. L’approche la plus originale est l’« apprentissage par renforcement au moment du test » (Test-Time RL). Pour les problèmes particulièrement difficiles, AlphaProof génère une série de variantes plus simples, formant ainsi un « cours d’apprentissage » naturel. En résolvant progressivement ces versions plus accessibles, le système accumule des connaissances et des intuitions, avant de s’attaquer au problème original – une stratégie cruciale pour résoudre le problème n°6. La stratégie d’entraînement est également progressive : elle commence par des recherches limitées pour éviter les blocages, puis augmente progressivement la profondeur selon les performances. Bien que certains problèmes soient résolus en quelques minutes, d’autres nécessitent jusqu’à trois jours – une différence qui soulève des questions sur la rapidité, mais dont les chercheurs rappellent que l’objectif n’est pas la vitesse, mais la qualité du raisonnement. Des experts comme Timothy Gowers, lauréat de la médaille Fields, ont salué l’approche comme « impressionnante » et « une avancée significative ». Katie Collins, spécialiste d’IA et de mathématiques à Cambridge, souligne que la formalisation automatisée pourrait renforcer la confiance dans les résultats mathématiques et faciliter la collaboration scientifique. En parallèle, DeepMind a lancé en 2025 Gemini Deep Think, un système capable de raisonner directement en langage naturel et de remporter une médaille d’or à l’IMO en 4,5 heures – sans passer par Lean. Cette évolution montre une convergence vers des systèmes plus autonomes et plus naturels. AlphaProof ouvre la voie à une nouvelle génération d’outils mathématiques intelligents, où la rigueur formelle et la puissance d’inférence naturelle pourraient un jour se combiner. Comme le souligne Julian Schrittwieser, l’unique limite actuelle est la puissance de calcul disponible – une perspective prometteuse pour l’avenir de l’intelligence artificielle en mathématiques.