Des chercheurs de prestigieuses universités (Cambridge, Oxford, Columbia, ETH Zurich) ont publié la Déclaration de Leiden, un texte de onze pages soulevant des enjeux cruciaux pour la fiabilité mathématique à l'ère de l'IA. Le problème central : les systèmes d'IA produisent des arguments qui ressemblent formellement à des preuves mathématiques, mais sans garantie de correction et sans possibilité de vérification indépendante fiable par les pairs.

Le cas d'AlphaProof illustre cette préoccupation. Google DeepMind a annoncé en juillet 2024 la résolution de trois problèmes de l'Olympiade Internationale de Mathématiques, mais la méthodologie détaillée n'a été publiée que le 12 novembre 2025, plus d'un an après. Pendant ce délai, la communauté mathématique n'avait pas accès aux informations nécessaires pour évaluer la méthode globalement. Les signataires dénoncent également que les modèles d'IA exploitent massivement les publications mathématiques sans consentement explicite et ne citent souvent pas leurs sources, ce qui viole un principe fondamental : en mathématiques, citer les résultats antérieurs est inhérent à la démonstration elle-même. Sans ces citations, aucune vérification indépendante n'est possible.

Les professeurs Baptiste Royer et Maxence Mayrand pilotent un projet de recherche d'envergure réunissant physiciens et mathématiciens autour d'un enjeu crucial pour le calcul quantique : la correction d'erreurs. Le projet s'appuie sur une analogie remarquable entre les codes bosoniques de GKP (utilisés pour encoder l'information dans des oscillateurs harmoniques) et les variétés abéliennes complexes, objets mathématiques étudiés depuis les travaux d'Abel et Jacobi au XIXe siècle.

Le coeur de l'étude repose sur une observation : les données nécessaires pour définir une variété abélienne sont identiques à celles requises pour établir un code de correction d'erreur quantique. Les chercheurs examineront si ce parallèle structural peut aider à classifier, caractériser et prédire le comportement des codes de GKP. Bien que cette connexion ait été signalée dans la littérature scientifique, aucune équipe n'avait jusqu'alors réuni l'expertise requise sur les deux domaines pour l'explorer en profondeur.

Financé par le Fonds Nouvelles frontières en recherche – Exploration 2025, ce projet interdisciplinaire à haut risque pourrait transformer l'approche de la correction d'erreurs quantiques en débloquant des techniques mathématiques avancées pour renforcer la fiabilité des ordinateurs quantiques.

Mattias Jonsson, mathématicien suédois en poste à l'université du Michigan depuis plus de vingt ans, a été nommé CNRS Fellow Ambassadeur pour la quatrième cohorte du programme. Docteur du KTH de Stockholm en 1997, il s'est distingué par plus de soixante publications et des travaux pionniers en dynamique complexe, particulièrement sur les méthodes non archimédiennes et les espaces de Berkovich. Il est membre de l'American Mathematical Society et a bénéficié d'une bourse Simons en 2023-2024.

En collaboration avec les chercheurs français Charles Favre et Sébastien Boucksom (tous deux directeurs de recherche au CNRS), Jonsson a contribué à des avancées majeures sur la conjecture de Yau-Tian-Donaldson, concernant les conditions de stabilité et les métriques canoniques sur les variétés complexes. Pour cette nomination, il passera au minimum trois mois annuels en France au cours des trois prochaines années, basé à l'Institut de Mathématiques de Jussieu-Paris Rive Gauche, tout en visitant les laboratoires de Toulouse et Bordeaux.

Ce programme vise à renforcer les échanges scientifiques entre la France et les États-Unis. Jonsson prévoit d'organiser des ateliers thématiques et de faciliter la mobilité des jeunes chercheurs entre les deux pays, consolidant ainsi les interactions internationales dans la communauté mathématique.

Le problème des distances distinctes, posé par le mathématicien hongrois Paul Erd"os au XX siècle, demandait : sur une feuille infinie, si l'on place des points selon une configuration quelconque, combien de segments de même longueur peut-on tracer entre eux ? Bien que simple à énoncer, cette question a résisté à des décennies de recherches, la dernière avancée significative remontant à plus de quarante ans.

Une intelligence artificielle d'OpenAI vient de le résoudre, ce qui représente un succès sans précédent. Tim Gowers de Cambridge précise qu'aucune preuve générée par une IA n'avait atteint un tel niveau de rigueur avant : il accepterait cette démonstration dans une revue prestigieuse. Misha Rudnev de Bristol qualifie le résultat d'« explosif ».

Cette percée marque un tournant dans la collaboration entre humains et machines pour la recherche mathématique, ouvrant la voie à une nouvelle approche des grandes énigmes scientifiques.

L'IA AxiomProver, créée par la startup Axiom, vient de démontrer quatre conjectures mathématiques majeures. Le cas le plus spectaculaire concerne le professeur Dawei Chen, bloqué pendant cinq ans sur une formule de géométrie ; l'IA a fourni une preuve complète en quelques heures. La clé de sa réussite réside dans la reformulation du problème selon un angle inédit, réduisant la démonstration à une identité mathématique connue.

Les trois autres résultats couvrent des domaines variés : les semi-groupes numériques (algèbre et théorie des nombres), la combinatoire (construction de suites infinies évitant certaines propriétés, avec un écart de 40 000 fois les prévisions probabilistes) et la théorie des nombres (démonstration que la quasi-totalité des nombres premiers satisfait une propriété liée au théorème de Vandiver). Tous les résultats sont vérifiés formellement en Lean, un langage informatique qui permet de vérifier chaque étape mécaniquement, et les démonstrations sont publiées en open-source sur GitHub pour reproduction complète.

Cette percée illustre une nouvelle approche de la validation scientifique : les machines explorent des chemins que l'esprit humain n'avait pas empruntés, ouvrant la voie à un « mathématicien artificiel » capable de naviguer autonomement dans l'espace mathématique.