La classification des groupes finis simples (CFSG) est considérée comme l'une des plus vastes entreprises de preuve des mathématiques modernes.
Cette preuve, réalisée par une centaine de mathématiciens sur plusieurs décennies de travail collaboratif, est dispersée dans des centaines d'articles et de monographies, totalisant près de 20 000 pages, un volume qui dépasse de loin la capacité de vérification complète d'une seule personne ou même d'une seule équipe.
Dans ce contexte, l'introduction de l'IA pour assister la vérification formelle à grande échelle est devenue une nouvelle voie qu'il faut nécessairement explorer.
Pour promouvoir le développement de l'IA pour les Mathématiques, sous l'impulsion de Shing-Tung Yau, une équipe de recherche composée d'élèves du programme « Leading Class » du Qiuzhen College de l'Université Tsinghua, ainsi que de chercheurs du Yau Mathematical Sciences Center, de l'Institute for AI Industry Research (AIR) de Tsinghua et de l'Université de Warwick, a proposé FormaTheoria — un flux de travail assisté par l'IA pour la recherche mathématique : permettre à l'IA de partir des publications mathématiques originales, d'analyser automatiquement les relations de dépendance, d'intégrer les systèmes de connaissances et de construire des preuves formelles, pour enfin les soumettre à l'assistant de preuve Lean pour une vérification étape par étape.
Fin août 2026, FormaTheoria a déjà complété la formalisation Lean de quatre théorèmes clés, produisant plus de 994 000 lignes de code interconnecté représentant la théorie mathématique. Bien qu'il reste encore un long chemin pour vérifier entièrement la classification des groupes finis simples, ce résultat constitue déjà une étape importante vers cet objectif final.
La CFSG fournit un système de base à de nombreux résultats mathématiques importants
« Classification des groupes finis simples » semble très abstrait. Pour le dire simplement, c'est comme une « liste de pièces élémentaires » concernant la symétrie finie : toute structure symétrique finie complexe peut être décomposée couche par couche pour aboutir à un ensemble d'unités fondamentales impossibles à diviser davantage ; et le rôle de la CFSG est d'indiquer aux mathématiciens quelles sont exactement ces unités fondamentales.
Typiquement, la recherche mathématique commence par décomposer un problème complexe en ces unités fondamentales, puis traite chaque classe en se basant sur la liste complète fournie par la CFSG. Ainsi, la CFSG devient une infrastructure que d'autres preuves peuvent invoquer à tout moment. Si cette « infrastructure » contient des failles cachées, alors de nombreux résultats ultérieurs construits sur ses conclusions connexes pourraient être affectés.
Certaines synthèses professionnelles fournissent des preuves quantifiées de l'application de la CFSG. En 2018, l'American Mathematical Society a publié une monographie de Stephen D. Smith intitulée « Applying the Classification of Finite Simple Groups: A User’s Guide », un livre de 231 pages, en 10 chapitres, passant en revue les scénarios d'application de la CFSG. Les deux derniers chapitres de la table des matières publique listent 14 sujets d'application numérotés, incluant les graphes distance-transitifs, la conjecture de Frobenius, les algorithmes de groupes de permutations, la croissance des sous-groupes dans les groupes de type fini, les extensions de corps, les revêtements de surfaces de Riemann, le problème de Waring en théorie des groupes, les graphes expanseurs et les groupes approximatifs, etc.
La valeur applicative de la CFSG a également reçu la reconnaissance des plus hautes instances de la communauté mathématique internationale. En 2014, le Congrès International des Mathématiciens a invité Robert Guralnick, lauréat du prix Cole en algèbre 2018 de l'AMS, à donner une conférence plénière intitulée « Applications of the Classification of Finite Simple Groups ».
Ces applications incluent des résultats majeurs d'une grande influence académique. La CFSG est un maillon clé dans la chaîne de preuve complète du problème de Burnside restreint ; Efim Zelmanov a reçu la médaille Fields en 1994 pour avoir résolu ce problème. La monographie de Smith classe également le problème de Waring sur les groupes simples finis et les graphes expanseurs comme des directions d'application importantes de la CFSG, les articles représentatifs correspondants étant publiés dans les « Annals of Mathematics » (Problème de Waring ; diamètre des groupes simples finis et ses applications). Ces exemples montrent que la CFSG soutient déjà une série de travaux importants ayant remporté des prix académiques prestigieux et paru dans des revues mathématiques de premier plan.
En ce sens, la CFSG est devenue un système sous-jacent réutilisé de nombreuses fois. À mesure que les résultats en aval s'accumulent, vérifier sa justesse et sa vérifiabilité devient de plus en plus critique. Effectuer une vérification machine, traçable et reproductible, de la CFSG prend une signification qui dépasse la théorie des groupes elle-même.
Cependant, la difficulté réside dans le fait que les preuves de ce système sous-jacent proviennent d'époques, d'auteurs et de publications différentes, utilisant des notations, des définitions et des conditions par défaut souvent incohérentes ; une simple référence peut même pointer vers toute une autre littérature. Historiquement, une lacune importante dans la preuve de classification n'a été comblée que plus de vingt ans plus tard par une monographie en deux volumes totalisant 1 220 pages. FormaTheoria doit non seulement vérifier étape par étape chaque raisonnement, mais aussi vérifier que les définitions, conditions et références entre des centaines de publications peuvent être intégralement reliées, pour finalement former une chaîne de preuve sans rupture.
Comment l'IA fait progresser un projet de preuve à très grande échelle
De nombreux systèmes d'IA mathématique font face à un problème déjà préparé, avec l'énoncé, les définitions et les outils tous prêts ; l'IA se contente de trouver la preuve. Mais FormaTheoria est différent : il doit d'abord reconstruire les fondements mathématiques derrière le problème à partir d'une littérature éparse, puis achever la preuve. Ce travail présente quatre difficultés principales :
Premièrement, le système ne sait pas à l'avance combien de documents il devra consulter.
Une référence peut mener à un autre article, qui lui-même en évoque d'autres antérieurs. Le projet n'avait initialement que 3 sources principales, mais 12 sources supplémentaires ont été découvertes lors du processus de preuve ; les documents ajoutés ultérieurement représentent environ 65,6 % du nombre total de pages consultées. La méthode de FormaTheoria est la suivante : dès qu'un théorème prérequis manquant est détecté, il suspend la preuve en cours, recherche et formalise cet élément de dépendance, puis reprend la tâche initiale. Les résultats déjà vérifiés sont stockés dans une base de connaissances unifiée, accessible pour les preuves ultérieures.
Deuxièmement, il est difficile d'assembler directement différentes publications.
Différents auteurs utilisent différentes définitions, notations et conditions par défaut. Deux définitions peuvent être mathématiquement équivalentes, mais une fois écrites en code Lean, elles peuvent être incompatibles. FormaTheoria compare constamment les textes originaux et le code existant pour établir les relations de conversion nécessaires. Parallèlement, le système protège les énoncés mathématiques déjà vérifiés et vérifie si chaque correction affecte les preuves ultérieures. Ainsi, plusieurs ouvrages et articles indépendants peuvent progressivement s'intégrer dans un même cadre théorique.
Troisièmement, le code peut passer la vérification tout en interprétant mal le texte original.
Lean vérifie seulement si la logique de la preuve est cohérente, si la conclusion découle des prémisses, mais il ne peut juger si cette conclusion est fidèle au texte original. L'IA peut facilement omettre une condition, confondre « pour tout » et « il existe », ou même modifier incorrectement la conclusion. Pour cela, FormaTheoria a spécifiquement établi une étape de révision indépendante : un composant de traduction rédige d'abord l'énoncé Lean, puis un composant de révision le compare point par point avec le texte original. Parmi les 14 sections de littérature analysées dans l'article, les traductions initiales de 11 sections ont été renvoyées pour modification. Ce mécanisme de révision indépendant constitue ainsi une deuxième « assurance » en plus de la vérification machine.
Quatrièmement, la littérature originale peut elle-même contenir des problèmes.
Des erreurs de typographie, des conditions manquantes ou des formulations ambiguës peuvent apparaître dans les anciennes publications. FormaTheoria conserve les pages originales, et lorsque des contradictions surviennent dans les preuves ultérieures, il remonte les traces. Si la littérature permet une correction, le système ajoute la condition ou établit une relation de compatibilité ; si les preuves sont insuffisantes, le système enregistre le problème et le soumet à un mathématicien professionnel.
De plus, ce projet exige que l'IA maintienne un rythme sur une longue période. Une seule conversation ne peut contenir la tâche complète. Pour cela, FormaTheoria utilise une « carte des preuves » mise à jour en continu pour gérer la progression : les objectifs plus ardus sont décomposés en lemmes auxiliaires plus petits, les résultats réussis sont agrégés couche par couche vers le théorème principal, et les chemins d'échec sont également enregistrés pour éviter que le système ne retombe plusieurs fois dans la même impasse.
La stratégie de parallélisation est également conçue de manière particulière. Les tâches indépendantes peuvent progresser simultanément ; lorsque plusieurs tâches nécessitent le même résultat préliminaire, le système ne l'effectue qu'une seule fois et permet aux autres tâches de le réutiliser. En revanche, les contenus mathématiques publics susceptibles d'avoir un impact en cascade sont modifiés séquentiellement pour éviter les conflits. Les expériences contrôlées de l'article montrent que cette approche parallèle prenant en compte les dépendances a permis une accélération de 4,2 fois sur les tâches testées.
Ainsi, FormaTheoria forme une chaîne de travail complète : recherche de littérature, complément des dépendances, traduction du texte original, construction des preuves, vérification machine, révision indépendante, résolution des conflits, et transmission des questions incertaines aux professionnels mathématiques. Chaque étape est clairement attribuée et traçable. C'est précisément pour répondre aux difficultés pratiques rencontrées dans les projets de preuve à très grande échelle que cette conception a été faite, permettant à l'IA de connecter progressivement la littérature mathématique dispersée en un système théorique vérifiable, traçable et extensible.
△
Sept mois, quatre théorèmes clés, près d'un million de lignes de code vérifiable
Le 22 janvier 2026, FormaTheoria a soumis son premier code. Au 2 août 2026, le projet avait établi une chaîne théorique clé s'étendant jusqu'au théorème de Bender–Suzuki, ayant au préalable successivement prouvé les théorèmes de Feit–Thompson (sur les groupes d'ordre impair), de Glauberman Z*, et de Brauer–Suzuki.
Ces quatre théorèmes ne sont pas isolés ; ils constituent une voie importante et interconnectée au sein de la classification des groupes finis simples, la preuve de chacun s'appuyant souvent sur les vastes fondations mathématiques établies par les précédents.
L'instantané du projet après achèvement de ces preuves comprend :
- Plus de 994 000 lignes de code Lean ;
- Plus de 850 fichiers de code ;
- Le système a consulté 15 livres et articles, totalisant 1037 pages, dont environ les deux tiers ont été découverts progressivement lors de l'avancement des preuves.
Bien sûr, le nombre de lignes de code ne donne qu'un aperçu du volume du projet. Si l'on retrace à partir du théorème de Bender–Suzuki, le projet a formé un réseau de preuves contenant 30 298 déclarations mathématiques et 186 187 relations de dépendance, la chaîne de dépendance la plus longue atteignant 458 niveaux. Si l'on inclut les contenus pertinents de la bibliothèque de base de Lean, ce réseau s'étendrait à 74 922 déclarations et plus de 1,44 million de relations de dépendance. On peut dire qu'à l'arrière-plan de ce million de lignes de code se trouve un réseau de preuves inextricablement lié. Cette étude montre que des agents d'IA peuvent désormais, sous l'effet combiné de la vérification machine et d'une révision hiérarchique, continuer à faire progresser des projets mathématiques de grande envergure et à très longue portée.
Le processus d'exécution réel du projet possède également cette caractéristique de très longue portée. L'exécution d'agent la plus longue enregistrée dans l'article a duré 9,17 jours, période durant laquelle le système a effectué 606 compressions et réorganisations des informations accumulées, tout en conservant constamment l'objectif de preuve actuel, les résultats déjà accomplis et les problèmes encore en suspens. Ces données indiquent que le projet gère un réseau de preuves de très longue portée en constante évolution, qu'une simple génération ou une seule conversation ne peut couvrir un processus aussi complexe.
Auparavant, la formalisation mathématique à grande échelle dépendait fortement d'un investissement humain important, nécessitant généralement la collaboration soutenue de plusieurs chercheurs pendant des années. Un point de référence historique : la version formalisée en Coq du théorème de Feit–Thompson, réalisée précédemment par un projet manuel, a nécessité environ 15 personnes travaillant pendant six ans. En revanche, FormaTheoria a complété tout le contenu de ce projet manuel en sept mois, et a en outre étendu le travail à la formalisation d'autres théorèmes clés. Sept mois reste une période d'exécution extrêmement longue pour une tâche d'agent IA, mais comparé à la formalisation manuelle traditionnelle, l'intervention de l'IA réduit significativement l'échelle temporelle du projet.
△
La formalisation fait émerger un à un les problèmes cachés dans la littérature
La littérature mathématique s'adresse généralement à des chercheurs familiers du domaine. Ainsi, les auteurs omettent souvent des conditions déjà mentionnées précédemment, ou supposent que le lecteur peut reconnaître l'équivalence entre différentes définitions. De petites erreurs de typographie ou de notation sont souvent naturellement ignorées ou corrigées lors d'une lecture humaine. Mais FormaTheoria agit différemment : en traduisant la littérature ligne par ligne en code Lean, chaque définition, chaque condition et chaque étape de raisonnement doivent être écrits de manière claire et sans ambiguïté. C'est cette exigence de vérification ligne par ligne qui rend évidents les problèmes autrement invisibles dans la littérature originale.
L'article documente en détail divers problèmes découverts dans la littérature, notamment des définitions incohérentes pour un même concept dans différentes sources, des énoncés de théorèmes omettant des conditions nécessaires, des conditions de divisibilité mal placées, et même des erreurs d'indice dans des preuves. Certains de ces problèmes peuvent être corrigés automatiquement en fonction du contexte de la littérature ; ceux pour lesquels les preuves sont insuffisantes sont soumis à l'appréciation d'un mathématicien.
Un cas typique provient de deux documents sur le théorème des groupes d'ordre impair. Les deux documents définissent le « sous-groupe maximal de type I », mais la différence est que l'un exige qu'une propriété soit vérifiée pour « chaque complément », tandis que l'autre exige seulement « l'existence d'un complément » satisfaisant cette propriété. Formellement, la première est clairement plus forte que la seconde, rendant les deux définitions directement incompatibles. FormaTheoria a identifié cette différence lors de la formalisation, puis, en s'appuyant sur le théorème de Schur–Zassenhaus, a prouvé que les deux définitions sont en réalité équivalentes dans ce contexte, réussissant ainsi à établir un pont entre les deux documents.
Un autre cas provient d'un lemme de Peterfalvi. L'énoncé formel de ce lemme omettait la condition préalable que « l'ordre d'un certain groupe est impair », bien que la preuve ultérieure en dépende réellement. Même si, lors de l'application du lemme plus loin, le contexte antérieur garantissait cette condition, et que l'argument global n'était pas interrompu, Lean ne complète pas automatiquement cette information contextuelle. Après avoir retracé le chemin de preuve et les utilisations de ce lemme, FormaTheoria a automatiquement ajouté la condition manquante à l'énoncé du théorème, rendant toute la chaîne de formalisation plus complète et fiable.
△
Le projet a également découvert des erreurs plus directes dans la littérature. Une définition écrivait M à la place de H, objet qui aurait dû apparaître, et deux ouvrages de référence conservaient la même erreur. Un théorème de Huppert plaçait le facteur d dans une condition de divisibilité erronée ; le système, après avoir trouvé un contre-exemple, a arrêté la preuve et soumis le problème à un mathématicien. La condition correcte a été confirmée manuellement. Une preuve de Higman écrivait également les indices d'un ensemble de vecteurs de base de u0 à um, alors que la plage correcte devait aller jusqu'à um−1 ; cette erreur d'indice a été automatiquement identifiée et corrigée par le système durant le processus de preuve.
Ces cas reflètent une autre valeur importante de la vérification machine pour les grands projets mathématiques. FormaTheoria, en construisant des preuves formelles, effectue également un examen granulaire de la littérature originale : il enregistre où apparaissent les problèmes, quelles conditions nécessitent les preuves ultérieures, sur quels documents reposent les corrections, et si ces corrections affectent d'autres résultats. Pour la CFSG, constituée de centaines de documents interconnectés, ce mécanisme d'examen traçable peut transformer des détails qui dépendaient auparavant de l'expérience du lecteur pour être complétés, en justifications mathématiques pouvant être explicitement vérifiées.
Perspectives futures
FormaTheoria n'a pas encore achevé la formalisation complète de la classification des groupes finis simples ; il reste un long chemin vers l'objectif final. Le projet progresse à un rythme accéléré, continuant d'avancer vers la formalisation intégrale de l'une des entreprises de preuve les plus vastes des mathématiques modernes. Les résultats actuels indiquent que l'IA est déjà capable, en quelques mois, de maintenir et d'étendre un environnement mathématique à grande échelle, de suivre des relations de dépendance complexes à travers de multiples publications, et de construire, sous vérification stricte, un système théorique interconnecté et de volume substantiel. Les limites des capacités de l'IA commencent ainsi à s'étendre, passant de la résolution de problèmes mathématiques isolés à la participation à la construction systématique de connaissances mathématiques.
Ce travail formera également une infrastructure mathématique extensible de manière durable et réutilisable. La littérature traditionnelle indique seulement « où la preuve est écrite » ; le code formalisé enregistre en outre « de quoi dépend chaque conclusion », « comment différentes sources s'articulent », « quels problèmes ont été corrigés », et organise les définitions, lemmes et preuves déjà vérifiés en modules de connaissances directement exploitables pour les recherches futures. Une fois doté d'outils d'explication, de recherche et de visualisation, ce réseau de connaissances pourra aider les chercheurs à comprendre plus rapidement la structure globale de la CFSG, à réutiliser les résultats existants, et même fournir un soutien puissant aux mathématiciens humains pour explorer de nouvelles connexions et découvrir de nouveaux théorèmes.
L'équipe du projet FormaTheoria espère explorer un mode de collaboration humain-machine adapté à l'ère de l'IA : les humains sont responsables d'identifier les problèmes de recherche pertinents et de porter des jugements clés, l'IA assume les tâches de recherche et de déduction à grande échelle, et le système formel garantit que chaque étape acceptée peut être réexaminée. Lorsqu'une preuve devient si vaste qu'aucun individu ne peut la vérifier entièrement, cette combinaison des trois pourrait devenir une voie entièrement nouvelle pour l'humanité afin de gérer les connaissances mathématiques à très grande échelle.
Note : L'état du projet et les résultats quantitatifs dans cet article proviennent de l'instantané du projet à son achèvement en août 2026, tel que décrit dans l'article.
Article : https://arxiv.org/abs/2608.10894
Code : https://github.com/Qiuzhen-CFSG/CFSG
Cet article provient du compte WeChat « Quantum Bits », auteur : Équipe FormaTheoria
