Une conjecture vieille de trente ans, un modèle chinois et une preuve vérifiée par machine

Une conjecture vieille de trente ans, un modèle chinois et une preuve vérifiée par machine

Le 15 octobre, Shanghai AI Laboratory (上海人工智能实验室) a annoncé qu'une équipe de recherche avait démontré le cas tridimensionnel de la conjecture de Ghys, un problème ouvert en systèmes dynamiques posé depuis 1995. Les travaux ont été menés avec Intern-S2, le modèle propre au laboratoire, et la preuve finale a été formellement vérifiée dans Lean par une équipe de Peking University (北京大学).

L'intérêt ne tient pas seulement à la chute d'un problème difficile. Il tient à ce que l'annonce était structurée autour d'un processus plutôt que d'un chiffre : un modèle qui produit des dérivations, des chercheurs qui choisissent sur quelles pistes concentrer leur attention, et un assistant de preuve qui certifie chaque étape. C'est exactement la combinaison que le secteur promet depuis deux ans, et la voici, avec un article à la clé.

Ce que demande la conjecture

Étienne Ghys a posé le problème en 1995. En gros, il demande si le comportement des systèmes dynamiques chaotiques peut déterminer leur classification géométrique, c'est-à-dire si le mouvement renseigne sur la forme de l'espace où il se produit.

Ce n'est pas la question générale qui a été résolue. L'équipe a démontré le cas de codimension un, c'est-à-dire le cadre tridimensionnel, resté ouvert pendant trois décennies. Cette distinction compte pour lire l'affirmation honnêtement : la conjecture complète demeure plus large, mais le cas précis qui avait résisté à tout le monde est désormais tranché.

La première passe a produit quatre cents pages

La mécanique de la collaboration est plus intéressante que le résultat, car elle montre à quoi ressemble concrètement la recherche humain-IA, minute par minute.

La première exploration du problème par Intern-S2 a produit un rapport de dérivation d'environ 400 pages. Ce n'est pas une réponse. C'est un empilement de raisonnements candidats, dont une partie est utile et une autre non, exactement la forme de sortie que l'on obtient lorsqu'on demande à un modèle de réfléchir à quelque chose de réellement non résolu plutôt que de se remémorer quelque chose de connu.

À partir de là, le travail a suivi sept tours de raisonnement continu. Le graphe du problème, une carte des sous-affirmations et de leurs dépendances mutuelles, est passé de 15 à 389 nœuds. La production accumulée a atteint environ un millier de pages et incluait des dizaines d'approches distinctes. À chaque étape, les mathématiciens ont fait ce que le modèle ne peut pas faire seul : ils ont examiné les propositions, jugé quelles ouvertures étaient prometteuses et orienté le tour suivant.

Xu Disheng, chercheur invité au laboratoire et professeur à la Greater Bay University, et Zhang Jiesong, chercheur postdoctoral qui suit la conjecture depuis ses études doctorales, ont apporté ce jugement. L'article de Zhang, mis sur arXiv le 29 septembre et révisé le 13 octobre, est un travail à auteur unique assorti d'une déclaration d'usage de l'IA : le modèle a aidé à développer les idées et les arguments par de multiples tours de dialogue, et il a vérifié les mathématiques de façon indépendante.

Ce qui en fait plus qu'une histoire

Les affirmations selon lesquelles l'IA résout les mathématiques ne coûtent rien. Ce qui donne du poids à celle-ci, c'est que la preuve a été formalisée.

L'équipe de Peking University, dirigée par Bin Dong et Ruochuan Liu, a utilisé son propre cadre SHEAF pour formaliser les quatre théorèmes principaux, ainsi que les résultats auxiliaires de Ghys dont dépendent les arguments. Formaliser signifie traduire les définitions, les hypothèses et le raisonnement dans un langage qu'un ordinateur peut vérifier, où chaque étape de l'argument doit être écrite explicitement au lieu d'être laissée au lecteur averti.

Le travail a pris environ cinq jours, avec jusqu'à 100 agents en parallèle, et a produit près de 550 000 lignes de code Lean. Lean est un assistant de preuve interactif. Il ne se soucie pas du degré de confiance de quiconque. Il vérifie la logique, et il accepte la preuve ou il ne l'accepte pas.

SHEAF a organisé la tâche sous forme de graphe orienté de définitions, de propositions et de dépendances, de sorte que des agents distincts pouvaient travailler sur des pièces connectées pendant que l'équipe suivait quelles affirmations avaient une preuve et lesquelles en avaient encore besoin. C'est un type de division du travail réellement nouveau, et le cadre a aussi dû combler des lacunes dans la bibliothèque formelle existante pour les systèmes dynamiques, car l'outillage requis par cette preuve n'existait tout simplement pas encore.

Humains et modèle, des tâches différentes

La division du travail décrite par le laboratoire mérite d'être prise au pied de la lettre, car ce n'est la version flatteuse pour aucune des deux parties.

Le modèle a passé la littérature au peigne fin, découpé la proposition en morceaux, exploré des branches de preuve en parallèle, vérifié les étapes logiques et testé un grand nombre d'idées rapidement. Les humains ont fixé la direction, jugé quelles approches valaient la peine d'être poursuivies et pris les décisions qui déterminaient où investir l'effort du tour suivant.

Aucune des deux moitiés ne ressemble à l'autre. La contribution du modèle, c'est l'échelle et l'endurance : il peut garder en tête des dizaines d'impasses sans se décourager. La contribution des humains, c'est le goût, c'est-à-dire la capacité de regarder cent pages de raisonnement plausible et de savoir quels trois paragraphes comptent.

Une anecdote y est rattachée, dont la presse chinoise a fait grand cas. Un expert en systèmes dynamiques aurait soumis le même problème à GPT-6 par curiosité, après avoir entendu qu'un modèle national l'avait résolu, et il n'y est pas parvenu. Lu étroitement, c'est une comparaison entre deux systèmes sur un problème, ce qui prouve très peu. Lu comme un signal sur la dynamique concurrentielle, c'est le genre de détail qui oriente les investissements.

Pourquoi la vérification formelle change les enjeux

Pendant la majeure partie des deux dernières années, le goulot d'étranglement des mathématiques assistées par IA n'a pas été la génération d'arguments candidats. Les modèles sont doués pour produire du raisonnement plausible. Le goulot a été de savoir ce qui, dans tout cela, est correct, car vérifier une preuve est lent, exige un expert et se parallélise mal.

Lean inverse cela. Une fois qu'un énoncé est formalisé, la vérification est bon marché et rapide, et elle est fiable parce qu'elle est mécanique plutôt que sociale. Les 550 000 lignes sont la partie coûteuse, et le fait qu'une équipe plus une centaine d'agents aient pu les produire en cinq jours constitue la véritable avancée ici. Cela suggère que le goulot de la vérification pourrait se desserrer, tout comme celui de la génération était déjà desserré.

Le laboratoire indique qu'il packagera ce flux de travail comme module réutilisable de vérification mathématique sur sa plateforme de découverte scientifique, reliant le modèle, les agents, les données et les équipements expérimentaux. Il cite aussi un résultat antérieur, dans lequel une équipe de Wuhan University (武汉大学) a utilisé la plateforme pour réduire le cycle de développement d'une synthèse électrochimique de cinq à dix ans à un à deux.

Ce qu'il faut en retenir

Le résumé honnête est qu'il s'agit d'un vrai résultat, avec une vraie preuve, produit par un flux de travail encore très gourmand en main-d'œuvre humaine. Sept tours de pilotage par des experts, ce n'est pas un modèle qui tourne seul. Un article à auteur unique avec déclaration d'usage de l'IA, ce n'est pas un modèle qui réclame le mérite.

Ce qui a changé, c'est que la boucle se referme désormais. Un modèle peut produire assez de raisonnement pour compter sur un problème que personne n'a résolu, les humains peuvent le diriger, et un assistant de preuve peut certifier le résultat sans que personne ait à faire confiance à un résumé. C'est un pipeline, pas une démonstration, et ce sont les pipelines qui transforment une capacité en pratique.

La question suivante est de savoir si cela se généralise au-delà des cas où la formalisation est seulement possible. La géométrie et la dynamique ont une structure qui se prête à la vérification par machine. Une grande partie du reste de la science n'en a pas, et c'est dans ce territoire plus désordonné, en biologie, en science des matériaux et en médecine, que la promesse de l'IA comme assistante de recherche sera réellement mise à l'épreuve. Le résultat de Ghys dit que l'outil peut fonctionner. Il ne dit pas encore à quelle fréquence.