Un modèle d’IA chinois contribue à démontrer la conjecture de Ghys en dimension trois, les mathématiques étant vérifiées avec Lean

Un problème de mathématiques posé en 1995 franchit une nouvelle étape

Une conjecture mathématique formulée en 1995 a fait l’objet d’une démonstration couvrant la dimension complexe trois, grâce à une collaboration entre des mathématiciens et le modèle Intern-S2 du laboratoire d’IA de Shanghai. Une équipe de l’université de Pékin a ensuite traduit les quatre principaux théorèmes de l’article en preuves vérifiées par Lean, un système informatique conçu pour contrôler le raisonnement mathématique.

Le laboratoire d’IA de Shanghai a annoncé cette avancée le 15 octobre 2026, en l’attribuant à une équipe dirigée par Disheng Xu, professeur à la Great Bay University et chercheur invité au laboratoire. L’article de recherche, intitulé Codimension-one holomorphic Anosov diffeomorphisms, indique Jiesong Zhang, de l’Institut royal de technologie KTH de Suède, comme unique auteur.

Le résultat résout le cas de codimension un de la conjecture du mathématicien français Étienne Ghys, y compris en dimension complexe trois. Il porte sur un lien remarquable entre mouvement et forme : un espace qui permet un certain type de mouvement chaotique doit-il nécessairement présenter lui-même une structure mathématique très ordonnée ?

Intern-S2 a contribué à élaborer des idées et des arguments au fil d’échanges répétés avec les chercheurs. Dans sa déclaration sur l’usage de l’IA, Zhang indique avoir vérifié seul l’ensemble des mathématiques. La collaboration a combiné exploration par machine, jugement humain et processus indépendant de vérification formelle.

Le laboratoire présente cette avancée comme la première fois qu’un modèle d’IA chinois contribue à résoudre un problème mathématique de cette envergure. Le résultat concret est un théorème de classification, accompagné d’une prépublication accessible au public et du code de formalisation rendu public.

Ce que la démonstration révèle sur le mouvement et la forme

La conjecture de Ghys relève des systèmes dynamiques complexes, qui étudient l’évolution de systèmes mathématiques lorsque leurs coordonnées obéissent aux règles des nombres complexes. Un nombre complexe possède deux composantes réelles ; la dimension complexe trois correspond donc localement à six dimensions réelles. Le cadre est plus abstrait que celui d’un objet ordinaire se déplaçant dans une pièce.

Un système d’Anosov associe de façon précise étirement et contraction. Au fil des mouvements répétés, certaines directions se contractent tandis que d’autres s’étendent. Des points de départ proches peuvent rapidement s’éloigner, produisant un comportement chaotique alors même que la règle régissant chaque étape est exacte.

On peut se représenter le phénomène comme un processus répétitif qui étire et replie une forme. Le système mathématique étudié ici est bien plus contraint : étirement et contraction doivent respecter des conditions uniformes, et le mouvement doit préserver la structure définie par les coordonnées complexes.

Ghys a conjecturé que de tels systèmes sur des variétés complexes compactes devraient admettre une description algébrique standard. Une variété est un espace qui paraît simple à petite échelle, même si sa forme globale est complexe. Dans ce contexte, la compacité est une propriété mathématique qui empêche l’espace de s’étendre à l’infini.

Le théorème de Zhang affirme que tout difféomorphisme holomorphe d’Anosov de codimension un sur une variété complexe compacte et connexe est biholomorphiquement conjugué à un automorphisme hyperbolique d’un tore complexe. En termes plus simples, un changement réversible de coordonnées qui respecte la structure complexe transforme le mouvement en une transformation algébrique standard sur un espace très régulier.

Un tore complexe peut être construit en identifiant les points d’un espace complexe qui diffèrent d’un élément d’un réseau périodique. L’apport essentiel est que cette dynamique complexe impose cette description géométrique ordonnée.

Pourquoi la portée exacte du résultat compte

L’article porte sur le cas de codimension un. Pour ces systèmes, cela signifie que l’une des composantes contractantes ou dilatantes est de dimension complexe un. Le théorème couvre cette famille restreinte de manière générale et résout la conjecture en dimension complexe trois.

La conjecture plus générale de Ghys concerne les systèmes d’Anosov holomorphes sur un éventail plus large de variétés complexes et les décrit à l’aide de modèles algébriques standard sur des espaces appelés infra-nilvariétés complexes. Le résultat de Zhang apporte une réponse particulièrement rigide pour le cas étudié : un tore complexe et un automorphisme hyperbolique.

Pour les mathématiciens qui travaillent sur ce cas, le théorème remplace la recherche d’un espace et d’un mouvement inconnus par l’étude d’un modèle standard. Un changement de coordonnées relie le système d’origine à ce modèle tout en préservant la géométrie complexe.

Xu étudiait le problème depuis des années. Avec son ancien directeur de thèse, le lauréat de la médaille Fields Artur Avila, il s’était auparavant penché sur le cas de la dimension trois. Xu et Zhang ont ensuite obtenu des résultats partiels connexes, publiés dans le Journal of the European Mathematical Society. Le nouveau travail s’inscrit dans la continuité de leurs recherches sur cette même question mathématique.

Des olympiades à un partenariat de recherche

Le rôle d’Intern-S2 fait suite à un résultat antérieur d’Intern-S1 aux Olympiades mathématiques chinoises de 2025. Cette année-là, le comité de la Société mathématique chinoise chargé des concours de mathématiques du secondaire a organisé un test d’IA, en invitant trois modèles chinois à résoudre des problèmes dans le même temps imparti qu’aux candidats humains.

Selon les mêmes critères de notation, Intern-S1 a obtenu 102 points, se classant premier parmi les trois modèles participants. Le seuil de la médaille d’or était fixé à 78 points : le modèle l’a dépassé de 24 points, soit environ 31 %.

Xu a entrevu le potentiel de cette famille de modèles pour la recherche en mathématiques, tandis que le laboratoire d’IA de Shanghai souhaitait passer des problèmes de concours aux questions non résolues. Leur collaboration a débuté au début de 2026 et a notamment donné lieu à la création d’un système logiciel, appelé Harness, destiné à organiser le travail du modèle et ses échanges avec les chercheurs.

Les principales étapes ont été les suivantes :

• 1995 : Étienne Ghys formule la conjecture.
• 2025 : Intern-S1 obtient 102 points au test d’IA des Olympiades mathématiques chinoises.
• Début 2026 : Xu et le laboratoire d’IA de Shanghai lancent leur collaboration sur l’entraînement du modèle.
• Mars 2026 : Xu devient chercheur invité au laboratoire.
• Août 2026 : une version d’Intern-S2 développée en interne et son système d’assistance atteignent le stade utilisé pour une exploration mathématique intensive.
• 29 septembre : l’article de Zhang est publié sur arXiv, puis révisé le 13 octobre.
• 15 octobre 2026 : l’avancée est annoncée publiquement.

Comment les mathématiciens ont guidé l’IA

La première exploration du problème par Intern-S2 a produit un rapport de démonstration d’environ 400 pages. Xu a invité Zhang, son ancien étudiant et chercheur postdoctoral au KTH, à rejoindre le projet comme chercheur invité. Zhang suivait la conjecture de Ghys depuis ses études doctorales.

Xu et Zhang ont examiné les propositions du modèle, repéré les pistes prometteuses et formulé des retours pour orienter les explorations suivantes. La machine a suivi différentes voies de raisonnement et produit des arguments ; les mathématiciens ont choisi celles qui méritaient d’être approfondies et contribué à assembler la démonstration finale.

Le laboratoire fait état de sept séries de raisonnements successives. Au cours du processus, le graphe du problème élaboré par le modèle est passé de 15 à 389 nœuds, tandis que le volume cumulé des résultats a atteint environ un millier de pages et comprend des dizaines de pistes proposées.

Un graphe de problème représente les sous-tâches mathématiques et leurs liens. Un nœud peut correspondre à une affirmation intermédiaire, un autre à un résultat nécessaire pour l’établir. La croissance rapportée illustre l’ampleur du découpage et de l’exploration du problème par le système.

Dans sa déclaration sur l’usage de l’IA, Zhang précise directement qui est responsable des mathématiques finales : une version interne d’Intern-S2 a contribué à élaborer les idées et les arguments au fil de plusieurs échanges, et il a vérifié les mathématiques de manière indépendante. Dans son article, il remercie également Xu pour leurs discussions suivies.

L’apport des logiciels d’assistance

Le laboratoire d’IA de Shanghai a associé le modèle à un logiciel conçu pour gérer de longues chaînes de raisonnement et des retours humains répétés. Le système pouvait décomposer une question difficile en tâches plus petites, explorer plusieurs pistes et soumettre ses résultats à l’évaluation des chercheurs.

L’approche d’entraînement associait des connaissances scientifiques générales à des contenus visant la recherche en mathématiques, notamment des problèmes difficiles tirés d’articles et des méthodes de vérification des solutions proposées. Le laboratoire décrit également un apprentissage par renforcement fondé sur des récompenses vérifiables : un raisonnement correct et vérifiable pouvait ainsi fournir un signal d’entraînement.

Les chercheurs se sont ensuite appuyés sur l’expérience acquise avec le système d’assistance pour améliorer le modèle lui-même. L’objectif pratique était de maintenir des progrès utiles au long d’une recherche approfondie, en suivant les résultats intermédiaires et en corrigeant les erreurs à mesure que de nouveaux arguments étaient élaborés.

Le laboratoire a également cité des résultats obtenus sur IMO-Proof et AdvancedMathBench, des évaluations portant sur le raisonnement mathématique. Pour le projet consacré à la conjecture de Ghys, les éléments les plus détaillés sur le fonctionnement du système sont la succession de démonstrations approfondies, les retours d’experts, l’article achevé et sa vérification formelle ultérieure.

Comment l’université de Pékin a vérifié la démonstration

L’équipe de l’université de Pékin, dirigée par Bin Dong et Ruochuan Liu, a utilisé son cadre SHEAF pour formaliser les quatre principaux théorèmes de l’article de Zhang. Le travail a également couvert des résultats de Ghys dont dépendent les arguments.

La formalisation consiste à traduire des définitions, des hypothèses et des raisonnements mathématiques dans un langage vérifiable par un ordinateur. Un article classique peut compter sur un lecteur formé pour compléter les étapes familières. Avec Lean, ces étapes doivent être exprimées au moyen d’énoncés précis et d’opérations logiques autorisées.

Les membres de l’équipe Jiedong Jiang et Bin Wu ont indiqué que le travail avait duré environ cinq jours, avec jusqu’à 100 agents d’IA fonctionnant en parallèle. Il a produit environ 550 000 lignes de code Lean. Des experts ont également vérifié que les énoncés formels correspondaient au sens mathématique des principaux théorèmes de l’article.

SHEAF a organisé la tâche sous la forme d’un graphe orienté de définitions, de propositions et de dépendances. Plusieurs agents ont ainsi pu travailler sur des éléments connexes, tandis que l’équipe suivait les énoncés déjà démontrés et ceux qui restaient à traiter.

La formalisation ne consistait pas seulement à traduire les arguments finaux. Certains résultats auxiliaires en dynamique manquaient dans les bibliothèques de mathématiques formelles existantes. L’équipe a dû établir ces bases ou trouver des voies reposant sur des résultats déjà disponibles, puis relier les différents éléments pour former une chaîne complète.

L’article est disponible sous forme de prépublication sur arXiv, et le code de formalisation a été publié sur GitHub. L’annonce ne précise ni publication dans une revue ni décision d’évaluation par les pairs.

Pourquoi ces deux étapes sont complémentaires

Intern-S2 et SHEAF ont joué des rôles différents. Le premier a contribué à rechercher des idées et des arguments mathématiques. Le second a aidé à construire des preuves formelles vérifiables par Lean. Des mathématiciens ont guidé l’exploration, vérifié les résultats obtenus et évalué si les énoncés formels correspondaient bien aux théorèmes visés.

L’ampleur du travail rend cette répartition concrète. Environ un millier de pages de résultats exploratoires ont alimenté un article de recherche ; le processus de vérification a ensuite produit quelque 550 000 lignes de code formel. Chaque étape a donné au travail une forme adaptée à une tâche différente.

Pour les chercheurs qui travailleront sur le sujet, l’article public expose l’argument mathématique, tandis que le code public consigne la structure de la preuve formelle. Les définitions et résultats auxiliaires ajoutés pendant la formalisation pourront aussi servir de point de départ à de futurs travaux dans le même domaine.

La prochaine étape : un module de vérification réutilisable

Le laboratoire d’IA de Shanghai prévoit de transformer ce processus en module de vérification mathématique pour sa plateforme de découverte scientifique Intern Duanyan. L’objectif est de permettre aux projets ultérieurs de réutiliser la combinaison entre exploration par un modèle, retours d’experts et vérification formelle.

Le laboratoire compte également appliquer à d’autres disciplines présentant des structures mathématiques apparentées les capacités de raisonnement développées dans le cadre de ce projet. Le cycle envisagé consiste à résoudre un problème de recherche, à transformer les méthodes utiles en logiciels réutilisables, puis à les appliquer à une autre étude.

Pour Xu, ce résultat prolonge un intérêt de recherche de longue date grâce à la collaboration entre la Great Bay University, le laboratoire d’IA de Shanghai, le KTH et l’université de Pékin. Pour l’ensemble de la communauté mathématique, il apporte à la fois un nouveau résultat de classification et un exemple détaillé de participation de l’IA à la recherche sous la direction d’humains.

Points clés

• La nouvelle démonstration résout le cas de codimension un de la conjecture de Ghys, y compris en dimension complexe trois.
• Jiesong Zhang est l’unique auteur de l’article et affirme avoir vérifié de manière indépendante l’ensemble des mathématiques.
• Disheng Xu et Zhang ont guidé Intern-S2 au fil d’explorations et de retours répétés.
• Le graphe du problème élaboré par le modèle est passé de 15 à 389 nœuds, et les démonstrations produites représentent environ un millier de pages.
• Le cadre SHEAF de l’université de Pékin a contribué à formaliser dans Lean les quatre principaux théorèmes et des résultats auxiliaires.
• La vérification aurait duré environ cinq jours et généré près de 550 000 lignes de code.
• Le laboratoire prévoit de transformer ce processus en module de vérification mathématique réutilisable.