Anthropic : Claude formalise le théorème de Fermat en 11 jours
Le 4 septembre, Anthropic a publié les résultats d’un projet majeur : le modèle d’intelligence artificielle Claude a formalisé en onze jours la démonstration du théorème de Fermat via l’assistant Lean. Initiée par le chercheur Tianyi Peng, ancien élève de la classe Yao à l’université Tsinghua, cette initiative s’inscrit dans une démarche visant à auditer la fiabilité des raisonnements générés par les IA. Pour réussir cette entreprise, l’équipe a développé Prove2Me, une plateforme dédiée à la coopération multi-agents en mathématiques formelles. En séparant rigoureusement les énoncés des preuves et en cartographiant leurs dépendances, l’outil a permis à des dizaines d’agents Claude de traiter des sous-tâches parallèlement. Au total, le système a généré environ treize millions de lignes de code, validé plus de trente mille théorèmes intermédiaires et consommé six milliards de tokens. L’intelligence artificielle n’a pas inventé un nouveau raisonnement, mais a retranscrit avec précision la méthode historique d’Andrew Wiles, traduisant en vérifications binaires des concepts avancés comme les courbes de Frey et la modularité. La vérification de la preuve a fait l’objet d’une attention particulière. L’assistant Lean a contrôlé chaque étape logique, tandis qu’un comparateur a croisé le résultat avec la base de référence Mathlib. Un second noyau de vérification indépendant, développé en Rust, a validé l’intégrité du raisonnement, confirmant que le modèle s’appuyait exclusivement sur trois axiomes standards sans utiliser de raccourcis non prouvés. Cette réussite démontre que l’IA peut désormais endosser le rôle d’ingénieur en mathématiques formelles, capable de gérer des projets de grande envergure. Toutefois, Anthropic nuance l’enthousiasme : le code produit est cinq fois plus volumineux que les bibliothèques classiques, ce qui le rend difficile à lire et à réutiliser pour les humains. Les coûts informatiques restent élevés, et le gain en efficacité par rapport à un mathématicien expert n’est pas encore mesuré. En somme, ce projet ne remplace pas l’intuition humaine, mais il établit un nouveau standard pour la vérification assistée. Il ouvre la voie à des outils capables d’auditer automatiquement des raisonnements complexes, transformant progressivement la pratique de la recherche en garantissant une traçabilité et une rigueur jusque-là impossibles à atteindre manuscritement.
