OpenAI a annoncé des centaines de résultats mathématiques produits par un modèle interne de pointe, parmi lesquels des preuves formalisées en Lean et des travaux originaux portant sur des questions de recherche ouvertes. La nouveauté tient à deux éléments : le nombre de résultats proposés et le recours à la formalisation par un assistant de preuve interactif, qui produit des éléments vérifiables plutôt que de simples arguments en langage naturel. Cette combinaison — raisonnement génératif et résultats vérifiables par machine — se distingue par le chemin qu’elle ouvre entre une idée initiale du modèle et un résultat validable mécaniquement, ce qui permet une reproduction indépendante plus rapide que pour des affirmations uniquement textuelles.

Jusqu’ici, les modèles de pointe étaient surtout évalués sur leurs capacités de programmation et leurs performances en traitement du langage. Produire du contenu mathématique original les fait entrer dans le domaine de la création et de la recherche scientifique. La découverte mathématique suppose de proposer de nouvelles conjectures, de construire des raisonnements non triviaux et de synthétiser des résultats existants pour faire progresser les connaissances. Lorsque les modèles font émerger de nouveaux lemmes ou comblent des lacunes dans des preuves complexes, leur rôle se rapproche davantage de celui d’un assistant de recherche que d’un outil de développement. Cette évolution change à la fois les bénéficiaires de leurs résultats et la façon de les intégrer : il ne s’agit plus seulement d’aider les programmeurs à accélérer la mise en œuvre, mais aussi d’aider les chercheurs à formuler des hypothèses et à construire des preuves.

La formalisation en Lean réduit les ambiguïtés, mais ne supprime pas le travail de vérification. Traduire une suggestion informelle du modèle en une preuve Lean entièrement spécifiée exige souvent un travail d’ingénierie humaine : il faut choisir les définitions, encoder les lemmes et ajuster les scripts de preuve. Par ailleurs, la formalisation en Lean met au jour les chaînes de dépendances et les hypothèses implicites, mais peut aussi introduire ses propres erreurs. Un processus robuste doit donc associer la vérification automatique des preuves, des dépôts reproductibles précisant les versions exactes de l’environnement et de la chaîne d’outils, ainsi qu’une reproduction indépendante par des experts afin de confirmer que l’affirmation du modèle tient au-delà de l’artefact initial.

Les résultats mathématiques générés par l’IA obligent les institutions à revoir leurs conventions de paternité et d’attribution du mérite. Lorsqu’un théorème est découvert avec l’aide importante d’un modèle, faut-il mentionner le chercheur principal, le concepteur du modèle, les deux ou aucun des deux ? Les registres de provenance sont tout aussi essentiels : les scripts de preuve versionnés, les points de contrôle du modèle, les invites initiales et les modifications humaines doivent être consignés pour que les évaluateurs puissent retracer l’évolution d’une idée. Les revues et les conférences doivent mettre à jour leurs politiques de soumission afin d’exiger une déclaration explicite de l’intervention d’un modèle et de définir comment attribuer ou écarter les résultats issus de l’IA lorsque leur provenance est incomplète.

Les équipes devraient adopter des pratiques concrètes : (1) traiter les résultats des modèles comme des ébauches à formaliser et à vérifier de manière indépendante ; (2) gérer les scripts de preuve avec un système de contrôle de versions et consigner le modèle exact ainsi que l’invite utilisée ; (3) mettre en place des processus d’évaluation pluridisciplinaires associant spécialistes du domaine et ingénieurs en vérification ; et (4) investir dans des outils qui automatisent la capture de l’environnement et la réexécution des preuves. Les bailleurs de fonds devraient privilégier les projets qui réduisent l’écart en matière de vérification et soutiennent des infrastructures communautaires permettant de produire des travaux mathématiques assistés par machine et reproductibles, plutôt que de se concentrer uniquement sur la taille des modèles ou les performances aux bancs d’essai.