Axiom affirme que des agents d’IA ont formalisé la classification des groupes simples finis en Lean

Axiom, une entreprise spécialisée en mathématiques et en IA, a annoncé sur X une formalisation automatique complète en Lean de la classification des groupes simples finis, un résultat qu’elle qualifie de « tableau périodique de la symétrie ». L’entreprise décrit la preuve originale comme comptant environ 15 000 pages, rédigées par plus de 100 mathématiciens au fil des générations, et la présente comme la plus grande preuve mathématique de l’histoire vérifiée par ordinateur.

Selon le dépôt open source d’Axiom, des essaims d’agents d’IA ont produit environ 43,1 millions de lignes de Lean en 24 jours, couvrant 715 articles et ouvrages, et ont signalé 34 écarts par rapport aux sources publiées. Une publication du compte d’actualités sur l’IA TestingCatalog ajoute que les agents se sont réparti le travail comme des équipes de développeurs et ont écrit du code plus vite que Lean ne pouvait le vérifier.

Ces chiffres proviennent du propre récit d’Axiom ; l’annonce ne fait état d’aucune évaluation indépendante de la formalisation. La publication avait reçu environ 6 200 mentions « J’aime » sur X au 28 octobre.