Ce Que Claude a Réellement Fait
Anthropic a annoncé le 4 septembre que Claude avait produit la première démonstration complète et vérifiée par ordinateur du dernier théorème de Fermat, en travaillant avec l'assistant de preuve Lean 4 pendant 11 jours, avec seulement des indications générales d'un chercheur humain. Le système a généré 13 millions de lignes de code Lean et démontré plus de 30 000 théorèmes auxiliaires, dont 29 500 ont été intégrés à la démonstration finale vérifiée, en utilisant un modèle de recherche interne qui a consommé environ six milliards de jetons de sortie via des dizaines d'agents fonctionnant en parallèle sur la plateforme Prove2Me.
Les mathématiques sous-jacentes ne sont pas nouvelles. Andrew Wiles a démontré le dernier théorème de Fermat en 1995, et Claude a formalisé une simplification ultérieure de cette démonstration due à Darmon, Diamond et Taylor, transformant un argument de 129 pages qu'il avait fallu des mois à la communauté mathématique pour vérifier à la main en une forme qu'un ordinateur peut vérifier ligne par ligne. Le mathématicien Kevin Buzzard, qui a examiné le résultat, a déclaré à Anthropic qu'il s'agissait d'un grand pas vers la formalisation automatique de la littérature mathématique moderne, obtenu en bien moins de temps qu'il ne l'attendait.
Pourquoi C'est une Histoire de Coût, Pas de Mathématiques
Le chiffre qui compte ici n'est pas les 13 millions de lignes, ce sont les 11 jours. La vérification formelle, cette pratique qui consiste à démontrer qu'un morceau de mathématiques ou de logiciel est correct plutôt que de le tester en espérant qu'il le soit, a toujours été lente et coûteuse à faire à la main, et formaliser un résultat de cette ampleur demandait auparavant des années de travail à des équipes spécialisées. Ce coût explique précisément pourquoi si peu de logiciels critiques pour la sécurité dans le monde portent une preuve formelle de correction, et un système automatisé capable d'un travail comparable en moins de deux semaines change le calcul pour toute entreprise d'ingénierie européenne qui certifie des systèmes selon des normes comme l'ISO 26262 pour l'automobile ou la DO-178C pour l'aviation, où les méthodes formelles sont déjà utilisées mais rationnées en raison de leur coût.
Le compte rendu d'Anthropic est franc sur le taux d'échec derrière ce chiffre marquant: environ 7 pour cent du code non répétitif provenait de tentatives infructueuses, abandonnées en chemin vers la démonstration finale. C'est une part normale de la manière dont la vérification formelle a toujours progressé, machine ou humain, mais cela mérite d'être dit clairement, car un succès de 13 millions de lignes donne l'impression inverse.
La Limite Que Personne Ne Devrait Franchir
Claude a formalisé une démonstration existante, il n'en a pas découvert une nouvelle, et cette différence compte plus que la performance elle-même dès que quelqu'un essaie d'y appuyer un poids d'ingénierie. Le dernier théorème de Fermat a fonctionné comme démonstration précisément parce que les mathématiciens s'accordaient déjà, depuis trois décennies, sur ce à quoi ressemblait la démonstration correcte, ce qui signifiait que la tâche de Claude était de traduire un argument connu dans un langage qu'une machine peut vérifier, pas de décider si l'argument était juste au départ.
Un dossier de sécurité pour un système de freinage ou un protocole cryptographique commence par une question plus difficile: que signifie correct ici, et quelqu'un l'a-t-il spécifié avec assez de précision pour qu'une méthode formelle puisse le vérifier. La formalisation automatisée peut désormais réduire drastiquement la seconde moitié de ce problème. Elle ne change rien à la première moitié, et toute organisation qui lit ce résultat comme une autorisation à sauter le travail de spécification plutôt que celui de vérification l'a mal compris.
À lire ensuite: 87 ans tombés devant une réponse que chacun peut vérifier | Anthropic loge vos journaux dans votre propre cloud
