Axiom formalise en Lean la preuve la plus longue

La jeune start-up d’IA Axiom a annoncé le 27 octobre avoir achevé, en 24 jours, la formalisation complète du théorème de classification des groupes simples finis (CFSG) dans le système Lean. Ses agents ont produit environ 43,1 millions de lignes de code, publiées en open source sur GitHub. Ce travail répond à un enjeu croissant: à mesure que des modèles, dont OpenAI, génèrent des preuves mathématiques, leur fiabilité devient un problème central. La formalisation traduit un raisonnement humain dans un langage vérifiable par une machine, chaque étape devant être contrôlée. Le CFSG, parfois nommé « théorème monstrueux », est la preuve humaine la plus longue: environ 15 000 pages, plus de 500 articles et près de 100 mathématiciens. Il dresse la liste des groupes simples finis, briques élémentaires de la symétrie, et inclut le groupe de Monster, aux 8×10^53 éléments. Les premières démonstrations, dispersées et parfois lacunaires, ont été complétées en 2004 puis 2008, tandis qu’une version modernisée reste inachevée. Axiom a donc formalisé la preuve initiale. En s’appuyant sur la bibliothèque Lean Mathlib et environ 1,2 million de lignes issues d’un projet lié à Shing-Tung Yau, l’équipe a découpé la démonstration en 108 jalons et 380 tâches confiées à des dizaines d’agents. Dès le 2 octobre, les systèmes ont commencé à coder sous supervision humaine. Des milliers de lignes ont été effacées après la découverte d’hypothèses non prouvées. Le 10 octobre, la preuve que le groupe de Monster est simple, pilier du classement, a été validée. Une pause brutale, due à des jalons trop larges, a forcé une replanification; un cache de vérification a ensuite accéléré les contrôles. Le 26 octobre, le noyau Lean a certifié toute la chaîne, des axiomes au résultat. Des experts doivent encore confirmer que l’énoncé traduit bien le théorème voulu. La démarche a aussi révélé des faiblesses dans les textes existants. Les ingénieurs rapportent des erreurs de frappe, des tableaux incorrects et des conditions manquantes, ainsi que 34 écarts sérieux par rapport à des publications. Le problème le plus délicat concernait le théorème des groupes déséquilibrés, utilisé pour exclure une famille entière de contre-exemples. Un raisonnement de John Walter de 1986 contenait une affirmation fausse; le théorème général n’est pas annulé, mais cette étape exigeait une nouvelle justification. Axiom a consulté Richard Lyons et Ronald Solomon, puis fait découvrir aux agents une démonstration de rechange, qui a produit un nouveau résultat de théorie des groupes publié sur Hexagon. Une route plus courte a ensuite été trouvée, et les deux sont conservées. Axiom a été fondée en mars 2025 par Carina Hong, mathématicienne formée au MIT et à Oxford, devenue entrepreneuse. Elle dirige une équipe où le théoricien Ken Ono est membre fondateur, après deux levées de fonds de 64 millions et 200 millions de dollars pour une valorisation supérieure à 1,6 milliard. Le projet répond aussi au débat ouvert par des mathématiciens de premier plan, dont Terence Tao, sur les preuves IA dont personne ne comprendrait l’enchaînement complet. La formalisation apporte une piste: même si l’énoncé et les choix d’organisation demandent une revue humaine, chaque dépendance devient inspectable et réutilisable. À l’heure où des preuves entières pourraient être écrites par des machines, elle offre un nouveau fondement à la confiance mathématique, libérant les chercheurs pour les questions et l’intuition que l’IA ne remplace pas encore.