Axiom Math a annoncé le 26 octobre avoir achevé ce qu’elle décrit comme la première preuve complète de la classification des groupes simples finis vérifiée par ordinateur dans Lean.
Dans l’annonce d’Axiom Math, l’entreprise indique que le projet a formalisé la preuve CFSG de première génération et l’a réduite à des étapes que Lean pouvait vérifier mécaniquement. Axiom affirme aussi que l’effort a duré 24 jours, mobilisé des dizaines d’agents IA et généré environ 43.1 millions de lignes de code Lean.
La formalisation ne s’est pas limitée à reproduire la littérature. Axiom affirme qu’elle a mis au jour 34 écarts notables par rapport aux arguments publiés et signalé un problème dans une approche publiée du théorème des groupes non équilibrés. L’entreprise prévoit de publier une liste d’errata plus détaillée à destination des mathématiciens.
Pour les builders, l’intérêt se situe moins dans le théorème mis en avant que dans le modèle opérationnel : décomposer un problème riche en dépendances en sous-problèmes suivis, puis maintenir un vérificateur dans la boucle afin qu’une sortie plausible ne soit pas prise pour un résultat finalisé. Ce modèle est pertinent partout où les agents doivent démontrer l’exhaustivité et la correction, et pas seulement produire un texte qui semble complet.