Une équipe dirigée par le professeur Liu Yang, directeur exécutif de l’Institut de recherche en intelligence artificielle de l’Université Tsinghua (AIR), en collaboration avec l’Académie Qiu Zhen de l’Université Tsinghua, a récemment obtenu une avancée majeure en mathématiques grâce à une collaboration innovante avec un système d’IA nommé AIM (AI Mathematician). Ce projet, centré sur la théorie de l’uniformisation, a abouti à une preuve mathématique détaillée d’environ 17 pages, démontrant de manière systématique la faisabilité d’un partenariat humain-IA dans la recherche mathématique fondamentale. La théorie de l’uniformisation, qui relie les matériaux, la mécanique des fluides et les mathématiques, traite de l’effet des microstructures hétérogènes sur les comportements macroscopiques des matériaux. L’équipe s’est attaquée à un problème précis : la dérivation des équations limites d’un système couplé Stokes-Lamé lorsque l’échelle des inclusions fluides tend vers zéro (ε → 0), ainsi que la preuve rigoureuse d’une estimation d’erreur d’ordre α = 1/2. Ce défi, d’une complexité élevée, nécessitait une analyse fine et une démonstration structurée sur plusieurs étapes. Plutôt que d’utiliser l’IA comme un simple outil de calcul, l’équipe a mis en place un cadre de collaboration humain-IA structuré, basé sur cinq modes d’interaction clés. Premièrement, le prompting direct a permis d’orienter l’IA en fournissant des théorèmes, des définitions et des stratégies de preuve, réduisant ainsi les dérives logiques. Deuxièmement, le co-usage théorique a consisté à intégrer des blocs complets de théorie mathématique (comme la théorie de Schauder) dans les instructions, permettant à l’IA de mener des raisonnements complexes dans un cadre rigoureux. Troisièmement, le raffinement itératif interactif a permis d’affiner progressivement la preuve par cycles d’essai, d’analyse humaine et de correction, corrigant des failles logiques identifiées. Quatrièmement, l’évaluation des limites d’application a permis d’assigner aux humains les tâches trop délicates pour l’IA, comme la manipulation de variables à double échelle, évitant ainsi les erreurs de symbolisme. Enfin, la stratégie d’optimisation auxiliaire a consisté à sélectionner les meilleurs modèles selon les tâches (par exemple, o4-mini pour la structure, DeepSeek-R1 pour les détails) et à exploiter la variabilité des sorties pour explorer plusieurs chemins de preuve. Un cas emblématique concerne la preuve de la régularité du problème cellulaire. En fournissant à l’IA des lemmes clés issus de la théorie de Schauder, les chercheurs ont pu guider l’IA vers une déduction cohérente et rigoureuse, démontrant ainsi sa capacité à intégrer et à appliquer des connaissances théoriques complexes. Ce travail va au-delà de la résolution d’un problème spécifique. Il établit un modèle opérationnel pour l’IA en tant que partenaire de recherche, en montrant qu’elle peut contribuer de manière non triviale à des preuves mathématiques complexes, tout en restant soumise à une supervision humaine. L’IA excelle dans l’analyse, la recherche d’idées, l’optimisation de méthodes existantes, mais les percées conceptuelles — comme la création de nouveaux outils ou cadres théoriques — restent encore le domaine exclusif de l’intuition humaine. Les chercheurs prévoient deux axes futurs : améliorer la capacité des modèles à détecter leurs propres erreurs (réduction des hallucinations), et développer des systèmes capables de proposer des conjectures originales, en s’appuyant sur des données expérimentales. Ce travail ouvre une nouvelle voie vers une recherche mathématique hybride, où l’intelligence artificielle n’est plus un outil passif, mais un collaborateur actif, capable de repousser les frontières de la connaissance.