L'équipe de Xu Disheng, professeur à l'Université du Grand Baie et chercheur visiteur au Shanghai Artificial Intelligence Laboratory (Shanghai AI Laboratory), s'appuyant sur le grand modèle scientifique multimodal Intern-S2 (书生-S2) et sur la voie technologique de la « fusion du général et du spécialisé », a achevé par une collaboration humain-machine la preuve de la conjecture de Ghys en dimension trois. Les équipes du professeur Dong Bin et de l'académicien Liu Ruochuan de l'Université de Pékin ont réalisé la vérification formelle de cette preuve grâce au framework SHEAF qu'elles ont développé, confirmant ainsi la validité de ce travail. Des professionnels du secteur estiment que cela marque la première fois que des scientifiques chinois résolvent un problème mathématique de classe mondiale à l'aide d'un grand modèle chinois.
La « conjecture de Ghys » a été formulée en 1995 par le mathématicien français Étienne Ghys, qui conjecturait que tout système d'Anosov holomorphe sur une variété complexe compacte est biholomorphement conjugué à un automorphisme affine holomorphe d'une certaine variété complexe infra-nilpotente. Ce problème, alliant difficulté théorique et valeur emblématique pour la discipline, est reconnu par les experts en mathématiques du domaine des systèmes dynamiques comme l'une des questions ouvertes de long terme les plus importantes du domaine, une pierre de touche pour évaluer la capacité de raisonnement mathématique.
L'article de recherche correspondant a été publié sur la plateforme de prépublications (arXiv), et son code de formalisation a été rendu public sur la plateforme Github.
La conjecture de Ghys : à la recherche du « code sous-jacent » des systèmes chaotiques
En 1995, le mathématicien français Étienne Ghys a formulé la conjecture de Ghys, dont le cœur est : l'existence d'un comportement de système dynamique chaotique peut-elle déterminer une classification géométrique.
Il s'agit d'un problème majeur du domaine des systèmes dynamiques complexes. Si cette conjecture est vraie, le problème des trajectoires dynamiques chaotiques pourrait être « réduit » à des modèles algébriques standards, simples et réguliers.
Comment comprendre la conjecture de Ghys ? On peut imaginer un « monde » fermé et fini, sans bord, où chaque petite portion obéit aux règles de calcul des nombres complexes.
Pour les systèmes d'Anosov, on peut recourir à l'analogie du pétrissage : en appuyant, étirant et repliant une pâte, certaines directions sont étirées, d'autres comprimées. L'effet d'étirement fait que des points initialement voisins se séparent rapidement — de légères différences dans les conditions initiales conduisent à des évolutions radicalement différentes.
La conjecture de Ghys affirme que, dès qu'existe un tel mouvement « ressemblant à la fois au pétrissage de la pâte et parfaitement régulier », ce « monde » ne peut être qu'une forme constituée par la répétition de règles simples, hautement régulière comme un réseau cristallin. Par exemple, le tore complexe :
Sous un autre angle, ce mouvement n'est en essence qu'une simple translation, rotation ou homothétie de ce « monde ». Autrement dit, le caractère trop chaotique du mode de mouvement détermine en retour la seule forme que le monde peut prendre. Le professeur Xie Junyi, du Beijing International Center for Mathematical Research de l'Université de Pékin et conférencier de 45 minutes au Congrès international des mathématiciens de 2026, a commenté : « La difficulté de la conjecture de Ghys tient au fait que l'énoncé analogue dans sa version réelle (numérique) reste un célèbre problème complètement ouvert ; dans le cas complexe, le problème devient encore plus rigide, c'est une question importante dans l'étude des phénomènes de rigidité des systèmes dynamiques complexes, extrêmement difficile ».
Le professeur Xu Disheng, de l'Université du Grand Baie, s'est longuement consacré à la recherche sur cette conjecture ; il avait étudié le cas de dimension trois avec son directeur de thèse, le professeur Artur Avila, lauréat de la médaille Fields, sans parvenir à une stratégie de preuve efficace ; il avait ensuite obtenu, en collaboration avec son étudiant, le docteur Zhang Jiesong, des résultats partiels et faiblement liés à la conjecture de Ghys en dimension trois, publiés dans la revue mathématique de premier plan Journal of the European Mathematical Society (JEMS).
7 lots de déductions successives et 389 nœuds : la collaboration humain-machine réalise une percée clé
« La découverte scientifique est l'épreuve ultime de l'intelligence. » Zhou Bowen, directeur et scientifique en chef du Shanghai Artificial Intelligence Laboratory, a émis un jugement : plus un problème est ancien et fondamental, plus l'espace de gains d'efficacité offert par l'IA est grand — les anticorps monoclonaux auxquels l'IA a participé, le repliement des protéines, ainsi que le problème du millénaire toujours non résolu des équations de Navier-Stokes, tout y répond. La conjecture de Ghys en dimension trois est précisément l'un de ces problèmes fondamentaux.
En mars 2026, le professeur Xu Disheng est devenu chercheur visiteur au Shanghai AI Laboratory ; sa collaboration scientifique avec le Shanghai AI Laboratory est ainsi entrée dans une phase plus profonde et plus étroite : les deux parties ont formé une équipe conjointe et ont simultanément mis en place un système Harness adapté aux scénarios de recherche mathématique. Fort de son expérience en recherche mathématique, le professeur Xu Disheng a identifié avec précision les lacunes du modèle et du système, et, en s'appuyant sur des problèmes réels de recherche mathématique de pointe, a conduit le système à accomplir de multiples cycles d'itération et de perfectionnement.
En août, Intern-S2 et son système associé, dont l'itération interne avait pris forme, disposaient d'une capacité de raisonnement récursif à grande échelle ainsi que d'une grande flexibilité dans l'interaction humain-machine, réalisant un saut qualitatif dans le traitement de problèmes mathématiques complexes. Ainsi, dès son premier cycle de raisonnement sur la conjecture de Ghys en dimension trois, Intern-S2 a produit un rapport de dérivation de 400 pages.
Au niveau de la stratégie d'entraînement, l'équipe de recherche a maintenu la voie technologique de la « fusion du général et du spécialisé » : sur la base d'un pré-entraînement à grande échelle sur les connaissances scientifiques pour consolider le socle du modèle, elle a soigneusement construit des données de post-entraînement de niveau recherche, comprenant un grand nombre de problèmes issus d'articles mathématiques et des schémas de vérification fiables, afin d'améliorer la spécialisation, la rigueur et la normativité du modèle en mathématiques de niveau recherche.
Au niveau des algorithmes d'entraînement, l'équipe de recherche a réalisé des percées dans les méthodes d'entraînement par apprentissage par renforcement pour le raisonnement asynchrone à long terme, résolvant sous récompenses vérifiables une série de difficultés fondamentales telles que l'accumulation exponentielle des erreurs, le maintien des états à long terme et l'autocorrection ; l'équipe a également développé en parallèle un algorithme d'auto-évolution qui distille en retour dans le modèle les gains de capacité apportés par le Harness, obtenant continuellement des signaux de supervision efficaces sur de nombreux problèmes de haute difficulté dépassant les limites de la capacité d'inférence directe du modèle, et faisant progresser l'amélioration autonome des capacités du modèle.
Sur des benchmarks de mathématiques de compétition et de mathématiques supérieures mettant l'accent sur le raisonnement rigoureux à long terme, tels qu'IMO-Proof et AdvancedMathBench, Intern-S2 domine globalement les modèles open source existants et dépasse sur certains indicateurs des modèles propriétaires de pointe tels que Gemini 3.1 Pro, se hissant parmi les modèles open source aux capacités de raisonnement à long terme les plus puissantes au monde.
À ce stade, les capacités du modèle de base d'Intern-S2 atteignaient le niveau élémentaire nécessaire pour aider une équipe de recherche à attaquer des problèmes mathématiques de niveau recherche, mais pour véritablement résoudre un problème de classe mondiale, il fallait encore franchir un palier supplémentaire. L'équipe a estimé que la clé de la percée résidait dans une collaboration humain-machine plus étroite :
Intern-S2 et son système associé ont mis à profit leur avantage de déduction à grande échelle sur de longues chaînes, déployant plusieurs branches simultanées, décomposant des problèmes complexes, conjecturant différentes pistes, et prenant en charge le travail massif et fastidieux de dérivation, en fournissant à chaque cycle d'itération d'énormes quantités de résultats d'essais ; les chercheurs, quant à eux, étaient chargés de maîtriser l'orientation générale, de juger quelles pistes méritaient d'être approfondies, quelles voies étaient des impasses, et de donner quelques suggestions d'intuition servant d'instructions pour le cycle d'itération suivant du système. Les deux ne déduisaient pas indépendamment de façon unilatérale, mais collaboraient humain-machine, en itérant au fil d'interactions étroites par dialogues et retours multiples.
La figure illustre le processus d'interaction multi-cycles du système ainsi que la structure de résolution récursive de chaque cycle d'interaction. Les arêtes n'y indiquent que les relations de décomposition en sous-problèmes, non des relations de dépendance de contexte ; chaque nœud peut accéder à l'intégralité du contexte global antérieur dans le temps à ce nœud.
Sur la base de la première phase d'exploration produite par l'IA, les mathématiciens Xu Disheng et Zhang Jiesong ont saisi avec acuité la percée clé, continuant à fournir des retours au modèle et à calibrer la direction d'exploration, guidant le modèle vers des pistes prometteuses. Au cours de l'attaque du problème, Intern-S2 a successivement accompli 7 lots de déductions successives ; le graphe du problème est passé de 15 à 389 nœuds, la production totale a atteint plus de mille pages de dérivations rigoureuses, et des dizaines de stratégies d'argumentation entièrement nouvelles ont été générées, contribuant avec succès à la résolution de ce problème mathématique de classe mondiale, ce qui a valu au travail l'évaluation d'un chercheur international de pointe dans ce domaine : « une profondeur de réflexion bien au-delà des attentes ».
Fait intéressant, avant le dépôt de l'article sur le site de prépublications arXiv, le professeur Xie Junyi, expert en systèmes dynamiques mentionné plus haut, avait lui aussi tenté de relever ce problème avec GPT-6, sans trouver de schéma de preuve. « Cela non seulement confirme la valeur unique d'Intern-S2 dans cette exploration mathématique de pointe, mais transmet aussi un signal : les grands modèles chinois ont eux aussi la capacité de monter sur l'arène des mathématiques de pointe et de contribuer à la résolution de problèmes de classe mondiale. »
L'équipe de l'Université de Pékin fournit une vérification formelle professionnelle
Les résultats produits avec l'aide de l'IA résistent-ils à la vérification ?
L'équipe du professeur Dong Bin et de l'académicien Liu Ruochuan de l'Université de Pékin a réalisé la vérification formelle de la totalité des quatre théorèmes principaux du présent article ; les démonstrations ont été validées par Lean. Lean, en tant que système interactif de démonstration de théorèmes, permet de soumettre les démonstrations formelles à un contrôle logique rigoureux. Jiang Jiedong et Wu Bin, membres clés de l'équipe de l'Université de Pékin, ont indiqué que l'ensemble du processus n'a duré qu'environ 5 jours, avec une concurrence maximale atteignant 100 agents et une production d'environ 55 万 lignes de code Lean, illustrant une ampleur de parallélisme considérable et une vitesse de vérification extrêmement rapide. Des experts ont confirmé la cohérence sémantique des énoncés formels avec les théorèmes principaux de l'article, et la vérification par Lean garantit ainsi leur exactitude rigoureuse.
La difficulté de la formalisation provient d'abord des mathématiques elles-mêmes : une preuve en langue naturelle repose souvent sur les connaissances mathématiques du lecteur pour compléter les hypothèses et le raisonnement, tandis que la formalisation doit la concrétiser en une preuve complète vérifiable par ordinateur. Si un résultat cité par l'article ne figure pas dans la bibliothèque de théorèmes de base, il faut compléter une preuve formalisée ou trouver une voie alternative exploitant des résultats existants. En particulier, le domaine des systèmes dynamiques manquait d'infrastructure formelle ; ce travail a comblé une grande quantité d'infrastructure, couvrant les nombreux résultats bibliographiques dont dépend l'article. Pour les mathématiques de niveau recherche, ces travaux impliquent l'expression exacte des définitions, la décomposition de la structure des preuves et le choix des outils mathématiques ; lorsqu'un grand nombre d'agents opèrent en parallèle, il faut en outre garantir que les définitions, les énoncés et les dépendances des différentes parties s'articulent entre eux pour que les preuves locales forment une chaîne de preuve complète.
Pour organiser ce processus, l'équipe de l'Université de Pékin a utilisé le framework SHEAF développé en interne : plusieurs agents organisent les propositions, définitions et relations de dépendance de l'article en un graphe orienté acyclique s'étendant par niveaux du théorème objectif jusqu'à la bibliothèque de théorèmes de base ; sous ce framework, le modèle participe à la décomposition des propositions et à la construction des preuves formalisées, et l'équipe orchestre le travail autour de ce graphe, suivant pour chaque nœud l'état de l'énoncé, de la preuve et de l'élagage, décomposant ainsi la tâche de formalisation à grande échelle en étapes articulées et vérifiables.
Dès 2021, alors que les grands modèles n'existaient pas encore, l'équipe du professeur Dong Bin du Beijing International Center for Mathematical Research de l'Université de Pékin avait perçu avec acuité que l'intelligence artificielle allait remodeler le paradigme de la recherche mathématique. L'équipe de mathématiques de l'Université de Pékin est l'une des premières au monde à s'être positionnée sur la direction AI for Math, en construisant une chaîne technologique complète couvrant les ensembles d'évaluation de haute difficulté (FATE), la récupération de connaissances mathématiques à grande échelle (Matlas/LeanSearch), le raisonnement automatique et la vérification formelle (Rethlas/Archon/Danus/Iteris) ; son système d'IA a réussi à résoudre la conjecture d'Anderson, un problème mathématique ouvert, réalisant la première prouesse en Chine, et également la première au monde, d'une percée autonome dans une conjecture mathématique majeure par une équipe universitaire s'appuyant sur l'intelligence artificielle. Récemment, l'équipe a également achevé de façon indépendante la vérification formelle de la conjecture de Poincaré.
D'un casse-tête isolé résolu vers les infrastructures de recherche scientifique
La portée de cette recherche réside également dans la validation d'un nouveau paradigme de recherche scientifique. La recherche mathématique traditionnelle repose sur les longues explorations d'individus géniaux, tandis que cet effort a permis d'intégrer systématiquement l'intuition d'experts dans la boucle de résolution par la machine, formant ainsi une boucle fermée « exploration systématique — jugement d'expert — accumulation de résultats — correction par retour d'information ». Ce paradigme est reproductible et extensible à d'autres domaines de recherche fondamentale « à espace de recherche immense mais à experts rares », afin de réaliser davantage de percées d'innovation originale « de 0 à 1 ».
Ensuite, en s'appuyant sur la boucle complète de capacités éprouvée au cours de cette recherche, l'équipe l'intégrera davantage en tant que module de vérification mathématique réutilisable de la plateforme de découverte scientifique InternDuanyan (书生·端砚), afin qu'il puisse être directement appelé pour des recherches ultérieures sur des questions scientifiques. Parallèlement, en prenant comme point de départ la percée sur la conjecture de Ghys en dimension 3, le Shanghai AI Laboratory étendra les capacités de raisonnement accumulées à d'autres disciplines dont les structures mathématiques sont homologues ; après avoir obtenu de nouvelles percées, ces nouvelles capacités de raisonnement seront réintégrées dans la plateforme Duan'an pour être réutilisées et combinées avec davantage de disciplines afin de rechercher la prochaine vague de percées, formant ainsi une roue d'auto-évolution « percée — encapsulation — réutilisation — nouvelle percée ». Le média Lei Feng Wang (compte public : Lei Feng Wang) suivra également en continu les derniers développements dans ce domaine.
Article original de Lei Feng Wang (雷峰网), reproduction interdite sans autorisation. Pour plus de détails, voirConditions de republication。