"Les IA commencent à résoudre la plupart des problèmes en mathématiques et des problèmes de preuves en mathématiques", cadre le mathématicien Amaury Hayat, professeur à l'École nationale française des Ponts et chaussées et qui étudie depuis plusieurs années la possibilité d'utiliser des modèles d'IA pour résoudre des problèmes de maths avancés. "Il y a environ un an, face à un théorème existant, les modèles étaient capables de déterminer s'il était possible de généraliser ce théorème, c'est-à-dire l'appliquer à des cas ou de le modifier pour traiter de nouveaux cas. C'est toujours sur cet aspect que ces IA sont les meilleures. Elles étaient aussi capables de faire des liens. En effet, à partir du moment où un large modèle de langage (LLM) comprend un peu les mathématiques et peut lire tous les articles de maths de l'histoire, il arrivait à repérer lorsqu'il manquait un argument, parce que celui-ci était déjà présent dans un autre article mais qui appartenait à un autre domaine. Argument dont les mathématiciens du premier domaine n'avaient souvent pas connaissance… Mais aujourd'hui, les modèles vont au-delà. Ils arrivent à résoudre des problèmes significativement plus durs, en particulier certaines anciennes conjectures restées non résolues bien que les mathématiciens cherchaient à les démontrer depuis très longtemps."

Cette avancée, dont la rapidité surprend jusqu'aux experts eux-mêmes, s'explique par deux progrès techniques au sein des grandes entreprises d'intelligence artificielle. La première est la technique d'entraînement des IA. L'adoption de la méthode par essai-erreur a créé une rupture entre les modèles "classiques" de type ChatGPT 4, et les "modèles de raisonnement" comme ChatGPT 5, Claude Opus ou Magistral de Mistral. "On n'a plus seulement entraîné un modèle de langage à prédire le mot suivant, reprend Amaury Hayat. On a aussi fait un "post-entraînement" où on l'entraîne à résoudre des problèmes. Et là, la seule chose qui compte est de voir s'il a ou pas la bonne réponse, et de favoriser ces dernières. On a ainsi fait naître une capacité du LMM à se poser des questions et à produire de longues réponses, en fonction desquelles il génère une réponse finale. Cette capacité de raisonnement a permis de stopper les hallucinations flagrantes du début." Ces modèles ont en outre été entraînés dès le départ sur les mathématiques, car ils nécessitaient de pouvoir vérifier la réponse finale. Pas étonnant donc qu'ils soient de très bons "matheux"…

Ce qui rend aussi ces LLM particulièrement "compétitifs" face à l'être humain, c'est leur échelle. "L'argent dépensé pour résoudre Navier-Stokes doit correspondre à peu près à 200 années d'un chercheur au CNRS, plaisante Amaury Hayat. C'est aussi compliqué de faire travailler 150 humains sur le même problème en même temps. On ne peut pas non plus les accélérer en mettant plus de puces informatiques. Une IA, oui !"

Concrètement, à ce stade, l'IA, même si elle s'appuie comme tout chercheur sur des découvertes humaines préalables, est bien capable d'une œuvre originale : elle peut "générer des idées brillantes que les humains n'avaient pas encore générées jusqu'ici". Mais pour démontrer un théorème, elle est – pour le moment ! – toujours meilleure associée aux humains que toute seule, selon Amaury Hayat.

Dans un futur immédiat, que peut-on encore attendre de ces larges modèles de langage ? "Ce n'est pas exclu qu'il y ait un deuxième problème du Millénaire résolu d'ici à la fin d'année, ou même plusieurs l'an prochain." Les IA s'améliorent en outre grandement – et vont encore s'améliorer à l'avenir – dans ce qu'on appelle l'autoformalisation. Concrètement, l'IA traduit automatiquement un problème mathématique écrit en langage humain (comme le français ou l'anglais) en un code logique rigoureux que les ordinateurs peuvent vérifier et prouver sans erreur.

En outre, si tous les manuels composant la "bibliothèque des mathématiques" étaient traduits en langage formel, cela "changerait la donne". En effet, cette masse constituerait des données d'entraînement idéales pour des IA. "Cela ouvre à des méthodes d'entraînement jusqu'ici un peu inaccessibles, comme celles où elles s'entraînent contre elles-mêmes. En 2018, AlphaZero a de cette façon mis trois jours à être meilleure aux échecs que tous les humains ! Avec une grande quantité de données formelles, on pourrait combiner cette méthode à celle de l'essai-erreur. Les IA pourraient donc atteindre un autre niveau de capacité. Je serais surpris qu'il y ait un plateau à très court terme, sauf si les grosses entreprises d'IA s'en désintéressent, ce qui est possible." Pour l'instant, les maths servent en effet à une entreprise de l'IA de "test de performance", et "à montrer que son modèle est meilleur que celui du voisin".