7 mois pour dépasser le travail de 15 mathématiciens en 6 ans : L'IA écrit des millions de lignes de code pour relever le défi de la vérification à grande échelle de la preuve du théorème de classification des groupes finis simples
La classification des groupes finis simples (CFSG) représente l'une des preuves mathématiques les plus vastes, fruit de décennies de travail par des centaines de mathématiciens, dispersée dans des milliers de pages. Pour relever le défi de sa vérification, le projet FormaTheoria, une initiative impliquant des chercheurs de l'Université Tsinghua et de l'Université de Warwick, propose un flux de travail assisté par IA. Ce système utilise l'intelligence artificielle pour analyser la littérature mathématique, reconstituer les dépendances, traduire les énoncés en code formel et les faire vérifier par l'assistant de preuve Lean.
En sept mois, FormaTheoria a formalisé en Lean quatre théorèmes clés de la CFSG (Feit-Thompson, Glauberman Z*, Brauer-Suzuki, Bender–Suzuki), produisant un réseau de preuves de plus de 994 000 lignes de code, 850 fichiers et 30 298 déclarations mathématiques interconnectées. Ce travail, qui aurait pris environ six ans à une quinzaine de mathématiciens, démontre la capacité de l'IA à gérer des projets mathématiques de longue haleine.
Le processus a révélé et corrigé des incohérences, des omissions ou des erreurs dans les sources originales, offrant une vérification granulaire. FormaTheoria vise à établir une nouvelle voie de collaboration homme-machine pour construire et maintenir des connaissances mathématiques massives, vérifiables et réutilisables, ouvrant la porte à la validation complète de la CFSG et au-delà.
marsbitIl y a 18 mins
